Optimized extraction

Coq/f.v

@@ -965,9 +965,24 @@ rewrite form_to_type_substt.
 reflexivity.
 Qed.
 
-Extract Inductive unit => "unit" [ "()" ].
+Extraction Inline id.
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive list => "list" [ "[]" "(::)" ].
+Extract Inlined Constant List.map => "List.map".
+Extract Inlined Constant List.nth => "(fun n l d -> match List.nth_opt l n with Some a -> a | None -> d)".
+Extract Inlined Constant List.fold_right => "(fun f a l -> List.fold_right f l a)".
 Extract Inductive prod => "(*)"  [ "(,)" ].
+Extract Inlined Constant fst => "fst".
+Extract Inlined Constant snd => "snd".
+Extract Inductive sigT => "(*)" ["(,)"].
+Extract Inlined Constant projT1 => "fst".
+Extract Inlined Constant projT2 => "snd".
 Extract Inductive option => "option"  [ "Some" "None" ].
-Extraction "f.ml" term_equal bound term1 term2.
+Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
+Extract Inlined Constant pred => "pred".
+Extract Inlined Constant Init.Nat.sub => "(fun m n -> m - n)".
+Extract Inlined Constant Nat.eqb => "(fun m n -> m = n)".
+Extract Inlined Constant Nat.leb => "(fun m n -> m <= n)".
+Extract Inlined Constant Nat.ltb => "(fun m n -> m < n)".
+Extract Inlined Constant Nat.compare => "(fun m n -> if m < n then Lt else if m > n then Gt else Eq)".
+Extraction "f.ml" term_equal bound type1 term1 type2 term2.