makes sure the following examples are well-treated:

Export X.
 conditional trivial rewrite nat_le_correct in H.
firstorder.
Definition error := @None.
Proof with trivial.
Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l
 with minus := Rminus div := Rdiv.
Ltac ElimPcompare c1 c2 :=
  let x := fresh H in
             intro x.
simplify_eq H.
Extraction Inline list_length_induction.
Extraction
 NoInline code insert isort map frequency_list huffman encode decode.

ajoute une modification dans le traitement de let_tuple


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5363 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 164 insertions, 54 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index ae7b71c1c9..18f2cc9349 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -46,6 +46,7 @@ and ct_COMMAND =
   | CT_coerce_THEOREM_GOAL_to_COMMAND of ct_THEOREM_GOAL
   | CT_abort of ct_ID_OPT_OR_ALL
   | CT_abstraction of ct_ID * ct_FORMULA * ct_INT_LIST
+  | CT_add_field of ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_BINDING_LIST
   | CT_add_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_addpath of ct_STRING * ct_ID_OPT
   | CT_arguments_scope of ct_ID * ct_ID_OPT_LIST
@@ -84,6 +85,7 @@ and ct_COMMAND =
   | CT_import_id of ct_ID_NE_LIST
   | CT_ind_scheme of ct_SCHEME_SPEC_LIST
   | CT_infix of ct_STRING * ct_ID * ct_MODIFIER_LIST * ct_ID_OPT
+  | CT_inline of ct_ID_NE_LIST
   | CT_inspect of ct_INT
   | CT_kill_node of ct_INT
   | CT_load of ct_VERBOSE_OPT * ct_ID_OR_STRING
@@ -108,6 +110,7 @@ and ct_COMMAND =
   | CT_ml_print_path
   | CT_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR
   | CT_module_type_decl of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_OPT
+  | CT_no_inline of ct_ID_NE_LIST
   | CT_omega_flag of ct_OMEGA_MODE * ct_OMEGA_FEATURE
   | CT_opaque of ct_ID_NE_LIST
   | CT_open_scope of ct_ID
@@ -140,6 +143,7 @@ and ct_COMMAND =
   | CT_print_visibility of ct_ID_OPT
   | CT_proof of ct_FORMULA
   | CT_proof_no_op
+  | CT_proof_with of ct_TACTIC_COM
   | CT_pwd
   | CT_quit
   | CT_read_module of ct_ID
@@ -290,11 +294,11 @@ and ct_FORMULA =
   | CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST
   | CT_existvarc
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
-  | CT_if of ct_FORMULA * ct_ID_OPT_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
+  | CT_if of ct_FORMULA * ct_RETURN_INFO * ct_FORMULA * ct_FORMULA
   | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
   | CT_labelled_arg of ct_ID * ct_FORMULA
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
-  | CT_let_tuple of ct_ID_OPT_NE_LIST * ct_ID_OPT_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
+  | CT_let_tuple of ct_ID_OPT_NE_LIST * ct_RETURN_INFO * ct_FORMULA * ct_FORMULA
   | CT_letin of ct_DEF * ct_FORMULA
   | CT_notation of ct_STRING * ct_FORMULA_LIST
   | CT_num_encapsulator of ct_NUM_TYPE * ct_FORMULA
@@ -351,10 +355,6 @@ and ct_ID_OPT_NE_LIST =
 and ct_ID_OPT_OR_ALL =
     CT_coerce_ID_OPT_to_ID_OPT_OR_ALL of ct_ID_OPT
   | CT_all
-and ct_ID_OPT_OPT =
-    CT_coerce_ID_to_ID_OPT_OPT of ct_ID
-  | CT_coerce_ANONYMOUS_to_ID_OPT_OPT of ct_NONE
-  | CT_coerce_NONE_to_ID_OPT_OPT of ct_NONE
 and ct_ID_OR_INT =
     CT_coerce_ID_to_ID_OR_INT of ct_ID
   | CT_coerce_INT_to_ID_OR_INT of ct_INT
@@ -530,6 +530,10 @@ and ct_RED_COM =
   | CT_red
   | CT_simpl of ct_PATTERN_OPT
   | CT_unfold of ct_UNFOLD_NE_LIST
+and ct_RETURN_INFO =
+    CT_coerce_NONE_to_RETURN_INFO of ct_NONE
+  | CT_as_and_return of ct_ID_OPT * ct_FORMULA
+  | CT_return of ct_FORMULA
 and ct_RULE =
     CT_rule of ct_PREMISES_LIST * ct_FORMULA
 and ct_RULE_LIST =
@@ -634,8 +638,12 @@ and ct_TACTIC_COM =
   | CT_exists of ct_SPEC_LIST
   | CT_fail of ct_INT * ct_STRING_OPT
   | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list
+  | CT_firstorder of ct_TACTIC_OPT
+  | CT_firstorder_using of ct_TACTIC_OPT * ct_ID_NE_LIST
+  | CT_firstorder_with of ct_TACTIC_OPT * ct_ID_NE_LIST
   | CT_fixtactic of ct_ID_OPT * ct_INT * ct_FIX_TAC_LIST
   | CT_formula_marker of ct_FORMULA
+  | CT_fresh of ct_STRING_OPT
   | CT_generalize of ct_FORMULA_NE_LIST
   | CT_generalize_dependent of ct_FORMULA
   | CT_idtac of ct_STRING_OPT
@@ -675,7 +683,7 @@ and ct_TACTIC_COM =
   | CT_right of ct_SPEC_LIST
   | CT_ring of ct_FORMULA_LIST
   | CT_simple_user_tac of ct_ID * ct_TACTIC_ARG_LIST
-  | CT_simplify_eq of ct_ID_OPT
+  | CT_simplify_eq of ct_ID_OR_INT_OPT
   | CT_specialize of ct_INT_OPT * ct_FORMULA * ct_SPEC_LIST
   | CT_split of ct_SPEC_LIST
   | CT_subst of ct_ID_LIST
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index d758113865..3801e1a043 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -111,6 +111,19 @@ and fCOMMAND = function
    fFORMULA x2;
    fINT_LIST x3;
    fNODE "abstraction" 3
+| CT_add_field(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) ->
+   fFORMULA x1;
+   fFORMULA x2;
+   fFORMULA x3;
+   fFORMULA x4;
+   fFORMULA x5;
+   fFORMULA x6;
+   fFORMULA x7;
+   fFORMULA x8;
+   fFORMULA x9;
+   fFORMULA x10;
+   fBINDING_LIST x11;
+   fNODE "add_field" 11
 | CT_add_natural_feature(x1, x2) ->
    fNATURAL_FEATURE x1;
    fID x2;
@@ -273,6 +286,9 @@ and fCOMMAND = function
    fMODIFIER_LIST x3;
    fID_OPT x4;
    fNODE "infix" 4
+| CT_inline(x1) ->
+   fID_NE_LIST x1;
+   fNODE "inline" 1
 | CT_inspect(x1) ->
    fINT x1;
    fNODE "inspect" 1
@@ -367,6 +383,9 @@ and fCOMMAND = function
    fMODULE_BINDER_LIST x2;
    fMODULE_TYPE_OPT x3;
    fNODE "module_type_decl" 3
+| CT_no_inline(x1) ->
+   fID_NE_LIST x1;
+   fNODE "no_inline" 1
 | CT_omega_flag(x1, x2) ->
    fOMEGA_MODE x1;
    fOMEGA_FEATURE x2;
@@ -443,6 +462,9 @@ and fCOMMAND = function
    fFORMULA x1;
    fNODE "proof" 1
 | CT_proof_no_op -> fNODE "proof_no_op" 0
+| CT_proof_with(x1) ->
+   fTACTIC_COM x1;
+   fNODE "proof_with" 1
 | CT_pwd -> fNODE "pwd" 0
 | CT_quit -> fNODE "quit" 0
 | CT_read_module(x1) ->
@@ -800,13 +822,12 @@ and fFORMULA = function
    fID x1;
    fFIX_BINDER_LIST x2;
    fNODE "fixc" 2
-| CT_if(x1, x2, x3, x4, x5) ->
+| CT_if(x1, x2, x3, x4) ->
    fFORMULA x1;
-   fID_OPT_OPT x2;
-   fFORMULA_OPT x3;
+   fRETURN_INFO x2;
+   fFORMULA x3;
    fFORMULA x4;
-   fFORMULA x5;
-   fNODE "if" 5
+   fNODE "if" 4
 | CT_inductive_let(x1, x2, x3, x4) ->
    fFORMULA_OPT x1;
    fID_OPT_NE_LIST x2;
@@ -821,13 +842,12 @@ and fFORMULA = function
    fBINDER_NE_LIST x1;
    fFORMULA x2;
    fNODE "lambdac" 2
-| CT_let_tuple(x1, x2, x3, x4, x5) ->
+| CT_let_tuple(x1, x2, x3, x4) ->
    fID_OPT_NE_LIST x1;
-   fID_OPT_OPT x2;
-   fFORMULA_OPT x3;
+   fRETURN_INFO x2;
+   fFORMULA x3;
    fFORMULA x4;
-   fFORMULA x5;
-   fNODE "let_tuple" 5
+   fNODE "let_tuple" 4
 | CT_letin(x1, x2) ->
    fDEF x1;
    fFORMULA x2;
@@ -925,12 +945,6 @@ and fID_OPT_NE_LIST = function
    fID_OPT x;
    (List.iter fID_OPT l);
    fNODE "id_opt_ne_list" (1 + (List.length l))
-and fID_OPT_OPT = function
-| CT_coerce_ID_to_ID_OPT_OPT x -> fID x
-| CT_coerce_ANONYMOUS_to_ID_OPT_OPT x ->
-    fNONE x;
-    fNODE "anonymous" 1
-| CT_coerce_NONE_to_ID_OPT_OPT x -> fNONE x
 and fID_OPT_OR_ALL = function
 | CT_coerce_ID_OPT_to_ID_OPT_OR_ALL x -> fID_OPT x
 | CT_all -> fNODE "all" 0
@@ -1268,6 +1282,15 @@ and fRED_COM = function
 | CT_unfold(x1) ->
    fUNFOLD_NE_LIST x1;
    fNODE "unfold" 1
+and fRETURN_INFO = function
+| CT_coerce_NONE_to_RETURN_INFO x -> fNONE x
+| CT_as_and_return(x1, x2) ->
+   fID_OPT x1;
+   fFORMULA x2;
+   fNODE "as_and_return" 2
+| CT_return(x1) ->
+   fFORMULA x1;
+   fNODE "return" 1
 and fRULE = function
 | CT_rule(x1, x2) ->
    fPREMISES_LIST x1;
@@ -1528,6 +1551,17 @@ and fTACTIC_COM = function
    fTACTIC_COM x;
    (List.iter fTACTIC_COM l);
    fNODE "first" (1 + (List.length l))
+| CT_firstorder(x1) ->
+   fTACTIC_OPT x1;
+   fNODE "firstorder" 1
+| CT_firstorder_using(x1, x2) ->
+   fTACTIC_OPT x1;
+   fID_NE_LIST x2;
+   fNODE "firstorder_using" 2
+| CT_firstorder_with(x1, x2) ->
+   fTACTIC_OPT x1;
+   fID_NE_LIST x2;
+   fNODE "firstorder_with" 2
 | CT_fixtactic(x1, x2, x3) ->
    fID_OPT x1;
    fINT x2;
@@ -1536,6 +1570,9 @@ and fTACTIC_COM = function
 | CT_formula_marker(x1) ->
    fFORMULA x1;
    fNODE "formula_marker" 1
+| CT_fresh(x1) ->
+   fSTRING_OPT x1;
+   fNODE "fresh" 1
 | CT_generalize(x1) ->
    fFORMULA_NE_LIST x1;
    fNODE "generalize" 1
@@ -1680,7 +1717,7 @@ and fTACTIC_COM = function
    fTACTIC_ARG_LIST x2;
    fNODE "simple_user_tac" 2
 | CT_simplify_eq(x1) ->
-   fID_OPT x1;
+   fID_OR_INT_OPT x1;
    fNODE "simplify_eq" 1
 | CT_specialize(x1, x2, x3) ->
    fINT_OPT x1;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 4ddcd21503..5359c69ade 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -76,7 +76,7 @@ let ctf_STRING_OPT_SOME s = CT_coerce_STRING_to_STRING_OPT s;;
 
 let ctf_STRING_OPT = function
   | None -> ctf_STRING_OPT_NONE
-  | Some s -> ctf_STRING_OPT_SOME s
+  | Some s -> ctf_STRING_OPT_SOME (CT_string s)
 
 let ctv_ID_OPT_NONE = CT_coerce_NONE_to_ID_OPT CT_none;;
 
@@ -272,11 +272,6 @@ let rec xlate_match_pattern =
 ;;
 
 
-let xlate_id_opt_opt = function
-    Some (Name id) -> CT_coerce_ID_to_ID_OPT_OPT(CT_ident (string_of_id id))
-  | Some Anonymous -> CT_coerce_ANONYMOUS_to_ID_OPT_OPT CT_none
-  | None -> CT_coerce_NONE_to_ID_OPT_OPT CT_none
-
 let xlate_id_opt_aux = function
     Name id -> ctf_ID_OPT_SOME(CT_ident (string_of_id id))
   | Anonymous -> ctv_ID_OPT_NONE;;
@@ -313,6 +308,11 @@ let rec make_fix_struct b = function
 
 let rec xlate_binder = function
     (l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
+and xlate_return_info = function
+  (None, None) -> CT_coerce_NONE_to_RETURN_INFO CT_none
+| (None, Some t) -> CT_return(xlate_formula t)
+| (Some x, Some t) -> CT_as_and_return(xlate_id_opt_aux x, xlate_formula t)
+| (Some _, None) -> assert false
 and xlate_formula_opt =
   function
     | None -> ctv_FORMULA_OPT_NONE
@@ -362,6 +362,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		 CT_formula_ne_list
 		   (CT_bang(varc (xlate_reference r)),
 		    List.map xlate_formula l'))
+   | CAppExpl(_, (None, r), []) -> CT_bang(varc(xlate_reference r))
    | CAppExpl(_, (None, r), l) -> 
        CT_appc(CT_bang(varc (xlate_reference r)),
 	       xlate_formula_ne_list l)
@@ -381,17 +382,16 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
                 CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns))
    | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> 
        xlate_error "No more COrderedCase"
-   | CLetTuple (_,a::l, (na,po), c, b) -> 
+   | CLetTuple (_,a::l, ret_info, c, b) -> 
       CT_let_tuple(CT_id_opt_ne_list(xlate_id_opt_aux a,
 				     List.map xlate_id_opt_aux l),
-		   xlate_id_opt_opt na,
-		   xlate_formula_opt po,
+		   xlate_return_info ret_info,
 		   xlate_formula c,
 		   xlate_formula b)
    | CLetTuple (_, [], _, _, _) -> xlate_error "NOT parsed: Let with ()"
-   | CIf (_,c, (na, p), b1, b2) -> 
+   | CIf (_,c, ret_info, b1, b2) -> 
        CT_if
-	 (xlate_formula c, xlate_id_opt_opt na, xlate_formula_opt p,
+	 (xlate_formula c, xlate_return_info ret_info,
 	  xlate_formula b1, xlate_formula b2)
 
    | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
@@ -739,6 +739,7 @@ and (xlate_call_or_tacarg:raw_tactic_arg -> ct_TACTIC_COM) =
     | Reference (Ident (_,s)) -> ident_tac s
     | ConstrMayEval(ConstrTerm a) ->
 	CT_formula_marker(xlate_formula a)
+    | TacFreshId s -> CT_fresh(ctf_STRING_OPT s)
     | t -> xlate_error "TODO LATER: result other than tactic or constr"
 
 and xlate_red_tactic =
@@ -880,9 +881,31 @@ and xlate_tactic =
 
 and xlate_tac =
   function
+    | TacExtend (_, "firstorder", tac_opt::l) ->
+       let t1 = match out_gen (wit_opt rawwit_tactic) tac_opt with
+	 | None -> CT_coerce_NONE_to_TACTIC_OPT CT_none
+	 | Some t2 -> CT_coerce_TACTIC_COM_to_TACTIC_OPT (xlate_tactic t2) in
+	 (match l with
+	      [] -> CT_firstorder t1
+	    | [l1] -> 
+		(match genarg_tag l1 with
+		     List1ArgType PreIdentArgType -> 
+		       let l2 = List.map 
+				  (fun x -> CT_ident x)
+				  (out_gen (wit_list1 rawwit_pre_ident) l1) in
+		       let fst,l3 = 
+			 match l2 with fst::l3 -> fst,l3 | [] -> assert false in
+		      	 CT_firstorder_using(t1, CT_id_ne_list(fst, l3))
+		   | List1ArgType RefArgType ->
+		       let l2 = List.map reference_to_ct_ID 
+				  (out_gen (wit_list1 rawwit_ref) l1) in
+		       let fst,l3 =
+			 match  l2 with fst::l3 -> fst, l3 | [] -> assert false in
+			 CT_firstorder_with(t1, CT_id_ne_list(fst, l3))
+		   | _ -> assert false)
+	    | _ -> assert false)
     | TacExtend (_, "refine", [c]) ->
-       CT_refine
-	 (xlate_formula (out_gen rawwit_casted_open_constr c))
+       CT_refine (xlate_formula (out_gen rawwit_casted_open_constr c))
     | TacExtend (_,"absurd",[c]) ->
        CT_absurd (xlate_formula (out_gen rawwit_constr c))
     | TacExtend (_,"contradiction",[opt_c]) ->
@@ -907,9 +930,15 @@ and xlate_tac =
      CT_discriminate_eq
          (xlate_quantified_hypothesis_opt
 	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
-    | TacExtend (_,"DEq", [idopt]) ->
-     CT_simplify_eq
-         (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt))
+    | TacExtend (_,"deq", [idopt]) ->
+	let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in
+	let idopt2 = match idopt1 with
+	    None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT
+		(CT_coerce_NONE_to_ID_OPT CT_none)
+	  | Some v ->
+	      CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
+	      	(xlate_quantified_hypothesis v) in
+	  CT_simplify_eq idopt2
     | TacExtend (_,"injection", [idopt]) ->
      CT_injection_eq
          (xlate_quantified_hypothesis_opt
@@ -966,14 +995,14 @@ and xlate_tac =
      let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
      if b then CT_rewrite_lr (c, bindl, id)
      else CT_rewrite_rl (c, bindl, id)
-    | TacExtend (_,"ConditionalRewrite", [t; b; cbindl]) ->
+    | TacExtend (_,"conditionalrewrite", [t; b; cbindl]) ->
      let t = out_gen rawwit_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_formula c and bindl = xlate_bindings bindl in
      if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
      else CT_condrewrite_rl (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
-    | TacExtend (_,"ConditionalRewriteIn", [t; b; cbindl; id]) ->
+    | TacExtend (_,"conditionalrewritein", [t; b; cbindl; id]) ->
      let t = out_gen rawwit_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
@@ -1151,8 +1180,7 @@ and xlate_tac =
 		     but the structures are different *)
 		  xlate_clause cl)
     | TacForward (true, name, c) -> 
-(* TODO LATER : avoid adding a location that will be ignored *)
-               CT_pose(xlate_id_opt ((0,0), name), xlate_formula c)
+               CT_pose(xlate_id_opt_aux name, xlate_formula c)
     | TacForward (false, name, c) -> 
                CT_assert(xlate_id_opt ((0,0),name), xlate_formula c)
     | TacTrueCut (na, c) -> 
@@ -1541,8 +1569,7 @@ let rec xlate_vernac =
       let red = xlate_red_tactic red in
       CT_coerce_EVAL_CMD_to_COMMAND
        (CT_eval (xlate_int_opt numopt, red, xlate_formula f))
-    | VernacChdir (Some str) -> CT_cd (ctf_STRING_OPT_SOME (CT_string str))
-    | VernacChdir None -> CT_cd ctf_STRING_OPT_NONE
+    |VernacChdir opt_s -> CT_cd (ctf_STRING_OPT opt_s)
     | VernacAddLoadPath (false,str,None) ->
  	CT_addpath (CT_string str, ctv_ID_OPT_NONE)
     | VernacAddLoadPath (false,str,Some x) ->
@@ -1583,6 +1610,39 @@ let rec xlate_vernac =
 	 CT_extract_to_file(CT_string file, 
 		       CT_id_ne_list(loc_qualid_to_ct_ID fst,
 				     List.map loc_qualid_to_ct_ID l2))
+    | VernacExtend("ExtractionInline", [l]) ->
+	let l1 = out_gen (wit_list1 rawwit_ref) l in
+	let fst, l2 = match l1 with [] -> assert false | fst ::l2 -> fst, l2 in
+	CT_inline(CT_id_ne_list(loc_qualid_to_ct_ID fst,
+				List.map loc_qualid_to_ct_ID l2))
+    | VernacExtend("ExtractionNoInline", [l]) ->
+	let l1 = out_gen (wit_list1 rawwit_ref) l in
+	let fst, l2 = match l1 with [] -> assert false | fst ::l2 -> fst, l2 in
+	CT_no_inline(CT_id_ne_list(loc_qualid_to_ct_ID fst,
+				List.map loc_qualid_to_ct_ID l2))
+    | VernacExtend("Field", 
+		   [a;aplus;amult;aone;azero;aopp;aeq;ainv;fth;ainvl;minusdiv]) ->
+	(match List.map (fun v -> xlate_formula(out_gen rawwit_constr v))
+                   [a;aplus;amult;aone;azero;aopp;aeq;ainv;fth;ainvl]
+ 	 with
+             [a1;aplus1;amult1;aone1;azero1;aopp1;aeq1;ainv1;fth1;ainvl1] ->
+	       let bind =
+		 match out_gen Field.rawwit_minus_div_arg minusdiv with
+		     None, None ->
+		       CT_binding_list[]
+		   | Some m, None ->
+		       CT_binding_list[
+			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "minus"), xlate_formula m)]
+		   | None, Some d ->
+		       CT_binding_list[
+			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "div"), xlate_formula d)]
+		   | Some m, Some d ->
+		       CT_binding_list[
+			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "minus"), xlate_formula m);
+			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "div"), xlate_formula d)] in
+		 CT_add_field(a1, aplus1, amult1, aone1, azero1, aopp1, aeq1,
+			      ainv1, fth1, ainvl1, bind)
+	   |_ -> assert false)
   | VernacExtend (("HintRewriteV7"|"HintRewriteV8") as key, largs) ->
       let in_v8 = (key = "HintRewriteV8") in
       let orient = out_gen Extraargs.rawwit_orient (List.nth largs 0) in
@@ -1727,9 +1787,7 @@ let rec xlate_vernac =
 	| PrintCoercionPaths (id1, id2) -> 
 	    CT_print_path (xlate_class id1, xlate_class id2)
 	| PrintInspect n -> CT_inspect (CT_int n)
-        | PrintUniverses None -> CT_print_universes ctf_STRING_OPT_NONE
-	| PrintUniverses (Some s) ->
-	    CT_print_universes (ctf_STRING_OPT_SOME (CT_string s))
+	| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
 	| PrintLocalContext -> CT_print
 	| PrintTables -> CT_print_tables
         | PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a)
@@ -2043,13 +2101,20 @@ let rec xlate_vernac =
 	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
 	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
 	CT_set_option_value2(table1, CT_id_or_string_ne_list(fst, values1))
+  | VernacImport(true, a::l) ->
+      CT_export_id(CT_id_ne_list(reference_to_ct_ID a,
+				 List.map reference_to_ct_ID l))
+  | VernacImport(false, a::l) ->
+      CT_import_id(CT_id_ne_list(reference_to_ct_ID a,
+				 List.map reference_to_ct_ID l))
+  | VernacImport(_, []) -> assert false
+  | VernacProof t -> CT_proof_with(xlate_tactic t)
+  | VernacVar _ -> xlate_error "Grammar vernac obsolete"
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)
-  |
-     VernacBack _|VernacRestoreState _|
-     VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
-     VernacImport (_, _)|VernacDistfix _|
-     VernacTacticGrammar _|VernacVar _|VernacProof _)
+  | VernacBack _|VernacRestoreState _| VernacWriteState _|
+    VernacSolveExistential (_, _)|VernacCanonical _ | VernacDistfix _|
+     VernacTacticGrammar _)
     -> xlate_error "TODO: vernac";;
 
 let rec xlate_vernac_list =