translation to structures now okay for pattern matching constructs

The locations in simpl, unfold, and the like are also better taken into account


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

3 files changed, 146 insertions, 81 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 456b00ea9..1a23883ae 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -30,7 +30,7 @@ and ct_BOOL =
 and ct_CASE =
     CT_case of string
 and ct_CLAUSE =
-    CT_clause of ct_HYP_LOCATION_LIST_OPT * ct_BOOL
+    CT_clause of ct_HYP_LOCATION_LIST_OR_STAR * ct_STAR_OPT
 and ct_COERCION_OPT =
     CT_coerce_NONE_to_COERCION_OPT of ct_NONE
   | CT_coercion_atm
@@ -115,7 +115,7 @@ and ct_COMMAND =
   | CT_rec_ml_add_path of ct_STRING
   | CT_rec_tactic_definition of ct_REC_TACTIC_FUN_LIST
   | CT_recaddpath of ct_STRING
-  | CT_record of ct_COERCION_OPT * ct_ID * ct_BINDER_LIST * ct_SORT_TYPE * ct_ID_OPT * ct_RECCONSTR_LIST
+  | CT_record of ct_COERCION_OPT * ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_ID_OPT * ct_RECCONSTR_LIST
   | CT_remove_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_require of ct_IMPEXP * ct_SPEC_OPT * ct_ID * ct_STRING_OPT
   | CT_reset of ct_ID
@@ -231,7 +231,7 @@ and ct_FORMULA =
   | CT_appc of ct_FORMULA * ct_FORMULA_NE_LIST
   | CT_arrowc of ct_FORMULA * ct_FORMULA
   | CT_bang of ct_INT_OPT * ct_FORMULA
-  | CT_cases of ct_FORMULA_OPT * ct_FORMULA_NE_LIST * ct_EQN_LIST
+  | CT_cases of ct_MATCHED_FORMULA_NE_LIST * ct_FORMULA_OPT * ct_EQN_LIST
   | CT_cofixc of ct_ID * ct_COFIX_REC_LIST
   | CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST
   | CT_existvarc
@@ -263,13 +263,12 @@ and ct_HINT_EXPRESSION =
   | CT_resolve of ct_FORMULA
   | CT_unfold_hint of ct_ID
 and ct_HYP_LOCATION =
-    CT_coerce_ID_to_HYP_LOCATION of ct_ID
-  | CT_intype of ct_ID
-  | CT_invalue of ct_ID
-and ct_HYP_LOCATION_LIST =
-    CT_hyp_location_list of ct_HYP_LOCATION list
-and ct_HYP_LOCATION_LIST_OPT =
-    CT_hyp_location_list_opt of ct_HYP_LOCATION_LIST option
+    CT_coerce_UNFOLD_to_HYP_LOCATION of ct_UNFOLD
+  | CT_intype of ct_ID * ct_INT_LIST
+  | CT_invalue of ct_ID * ct_INT_LIST
+and ct_HYP_LOCATION_LIST_OR_STAR =
+    CT_coerce_STAR_to_HYP_LOCATION_LIST_OR_STAR of ct_STAR
+  | CT_hyp_location_list of ct_HYP_LOCATION list
 and ct_ID =
     CT_ident of string
   | CT_metac of ct_INT
@@ -285,7 +284,7 @@ and ct_ID_NE_LIST =
     CT_id_ne_list of ct_ID * ct_ID list
 and ct_ID_NE_LIST_OR_STAR =
     CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR of ct_ID_NE_LIST
-  | CT_star
+  | CT_coerce_STAR_to_ID_NE_LIST_OR_STAR of ct_STAR
 and ct_ID_OPT =
     CT_coerce_ID_to_ID_OPT of ct_ID
   | CT_coerce_NONE_to_ID_OPT of ct_NONE
@@ -354,6 +353,13 @@ and ct_LOCAL_OPT =
   | CT_local
 and ct_LOCN =
     CT_locn of string
+and ct_MATCHED_FORMULA =
+    CT_coerce_FORMULA_to_MATCHED_FORMULA of ct_FORMULA
+  | CT_formula_as of ct_FORMULA * ct_ID_OPT
+  | CT_formula_as_in of ct_FORMULA * ct_ID_OPT * ct_FORMULA
+  | CT_formula_in of ct_FORMULA * ct_FORMULA
+and ct_MATCHED_FORMULA_NE_LIST =
+    CT_matched_formula_ne_list of ct_MATCHED_FORMULA * ct_MATCHED_FORMULA list
 and ct_MATCH_PATTERN =
     CT_coerce_ID_OPT_to_MATCH_PATTERN of ct_ID_OPT
   | CT_pattern_app of ct_MATCH_PATTERN * ct_MATCH_PATTERN_NE_LIST
@@ -402,8 +408,8 @@ and ct_PREMISE_PATTERN =
 and ct_PROOF_SCRIPT =
     CT_proof_script of ct_COMMAND list
 and ct_RECCONSTR =
-    CT_coerce_CONSTR_to_RECCONSTR of ct_ID_OPT * ct_FORMULA
-  | CT_constr_coercion of ct_ID_OPT * ct_FORMULA
+    CT_constr_coercion of ct_ID_OPT * ct_FORMULA
+  | CT_recconstr of ct_ID_OPT * ct_FORMULA
 and ct_RECCONSTR_LIST =
     CT_recconstr_list of ct_RECCONSTR list
 and ct_REC_TACTIC_FUN =
@@ -449,6 +455,11 @@ and ct_SPEC_LIST =
 and ct_SPEC_OPT =
     CT_coerce_NONE_to_SPEC_OPT of ct_NONE
   | CT_spec
+and ct_STAR =
+    CT_star
+and ct_STAR_OPT =
+    CT_coerce_NONE_to_STAR_OPT of ct_NONE
+  | CT_coerce_STAR_to_STAR_OPT of ct_STAR
 and ct_STRING =
     CT_string of string
 and ct_STRING_NE_LIST =
@@ -606,7 +617,8 @@ and ct_THM_OPT =
 and ct_TYPED_FORMULA =
     CT_typed_formula of ct_FORMULA * ct_FORMULA
 and ct_UNFOLD =
-    CT_unfold_occ of ct_INT_LIST * ct_ID
+    CT_coerce_ID_to_UNFOLD of ct_ID
+  | CT_unfold_occ of ct_ID * ct_INT_NE_LIST
 and ct_UNFOLD_LIST =
     CT_unfold_list of ct_UNFOLD list
 and ct_UNFOLD_NE_LIST =
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 9f8ece9b2..31134653c 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -70,14 +70,14 @@ and fBOOL = function
 and fCASE = function
 | CT_case x -> fATOM "case";
    (f_atom_string x);
-   print_string "\n"and fCOERCION_OPT = function
+   print_string "\n"and fCLAUSE = function
+| CT_clause(x1, x2) ->
+   fHYP_LOCATION_LIST_OR_STAR x1;
+   fSTAR_OPT x2;
+   fNODE "clause" 2
+and fCOERCION_OPT = function
 | CT_coerce_NONE_to_COERCION_OPT x -> fNONE x
 | CT_coercion_atm -> fNODE "coercion_atm" 0
-and fCLAUSE = function
-| CT_clause(x1,x2) ->
-   fHYP_LOCATION_LIST_OPT x1;
-   fBOOL x2;
-   fNODE "clause" 2
 and fCOFIXTAC = function
 | CT_cofixtac(x1, x2) ->
    fID x1;
@@ -320,7 +320,7 @@ and fCOMMAND = function
    fCOERCION_OPT x1;
    fID x2;
    fBINDER_LIST x3;
-   fSORT_TYPE x4;
+   fFORMULA x4;
    fID_OPT x5;
    fRECCONSTR_LIST x6;
    fNODE "record" 6
@@ -588,8 +588,8 @@ and fFORMULA = function
    fFORMULA x2;
    fNODE "bang" 2
 | CT_cases(x1, x2, x3) ->
-   fFORMULA_OPT x1;
-   fFORMULA_NE_LIST x2;
+   fMATCHED_FORMULA_NE_LIST x1;
+   fFORMULA_OPT x2;
    fEQN_LIST x3;
    fNODE "cases" 3
 | CT_cofixc(x1, x2) ->
@@ -677,23 +677,20 @@ and fHINT_EXPRESSION = function
    fID x1;
    fNODE "unfold_hint" 1
 and fHYP_LOCATION = function
-| CT_coerce_ID_to_HYP_LOCATION x -> fID x
-| CT_intype(x1) ->
+| CT_coerce_UNFOLD_to_HYP_LOCATION x -> fUNFOLD x
+| CT_intype(x1, x2) ->
    fID x1;
-   fNODE "intype" 1
-| CT_invalue(x1) ->
+   fINT_LIST x2;
+   fNODE "intype" 2
+| CT_invalue(x1, x2) ->
    fID x1;
-   fNODE "invalue" 1
-and fHYP_LOCATION_LIST = function
+   fINT_LIST x2;
+   fNODE "invalue" 2
+and fHYP_LOCATION_LIST_OR_STAR = function
+| CT_coerce_STAR_to_HYP_LOCATION_LIST_OR_STAR x -> fSTAR x
 | CT_hyp_location_list l ->
    (List.iter fHYP_LOCATION l);
    fNODE "hyp_location_list" (List.length l)
-and fHYP_LOCATION_LIST_OPT = function
-| CT_hyp_location_list_opt (Some l) ->
-   fHYP_LOCATION_LIST l;
-   fNODE "hyp_location_list_opt_some" 1
-| CT_hyp_location_list_opt None ->
-   fNODE "hyp_location_list_opt_none" 0
 and fID = function
 | CT_ident x -> fATOM "ident";
    (f_atom_string x);
@@ -720,7 +717,7 @@ and fID_NE_LIST = function
    fNODE "id_ne_list" (1 + (List.length l))
 and fID_NE_LIST_OR_STAR = function
 | CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR x -> fID_NE_LIST x
-| CT_star -> fNODE "star" 0
+| CT_coerce_STAR_to_ID_NE_LIST_OR_STAR x -> fSTAR x
 and fID_OPT = function
 | CT_coerce_ID_to_ID_OPT x -> fID x
 | CT_coerce_NONE_to_ID_OPT x -> fNONE x
@@ -826,7 +823,27 @@ and fLOCAL_OPT = function
 and fLOCN = function
 | CT_locn x -> fATOM "locn";
    (f_atom_string x);
-   print_string "\n"and fMATCH_PATTERN = function
+   print_string "\n"and fMATCHED_FORMULA = function
+| CT_coerce_FORMULA_to_MATCHED_FORMULA x -> fFORMULA x
+| CT_formula_as(x1, x2) ->
+   fFORMULA x1;
+   fID_OPT x2;
+   fNODE "formula_as" 2
+| CT_formula_as_in(x1, x2, x3) ->
+   fFORMULA x1;
+   fID_OPT x2;
+   fFORMULA x3;
+   fNODE "formula_as_in" 3
+| CT_formula_in(x1, x2) ->
+   fFORMULA x1;
+   fFORMULA x2;
+   fNODE "formula_in" 2
+and fMATCHED_FORMULA_NE_LIST = function
+| CT_matched_formula_ne_list(x,l) ->
+   fMATCHED_FORMULA x;
+   (List.iter fMATCHED_FORMULA l);
+   fNODE "matched_formula_ne_list" (1 + (List.length l))
+and fMATCH_PATTERN = function
 | CT_coerce_ID_OPT_to_MATCH_PATTERN x -> fID_OPT x
 | CT_pattern_app(x1, x2) ->
    fMATCH_PATTERN x1;
@@ -910,14 +927,14 @@ and fPROOF_SCRIPT = function
    (List.iter fCOMMAND l);
    fNODE "proof_script" (List.length l)
 and fRECCONSTR = function
-| CT_coerce_CONSTR_to_RECCONSTR (x1,x2) ->
-   fID_OPT x1;
-   fFORMULA x2;
-   fNODE "CONSTR_to_RECCONSTR" 2
 | CT_constr_coercion(x1, x2) ->
    fID_OPT x1;
    fFORMULA x2;
    fNODE "constr_coercion" 2
+| CT_recconstr(x1, x2) ->
+   fID_OPT x1;
+   fFORMULA x2;
+   fNODE "recconstr" 2
 and fRECCONSTR_LIST = function
 | CT_recconstr_list l ->
    (List.iter fRECCONSTR l);
@@ -1010,6 +1027,11 @@ and fSORT_TYPE = function
 and fSPEC_OPT = function
 | CT_coerce_NONE_to_SPEC_OPT x -> fNONE x
 | CT_spec -> fNODE "spec" 0
+and fSTAR = function
+| CT_star -> fNODE "star" 0
+and fSTAR_OPT = function
+| CT_coerce_NONE_to_STAR_OPT x -> fNONE x
+| CT_coerce_STAR_to_STAR_OPT x -> fSTAR x
 and fSTRING = function
 | CT_string x -> fATOM "string";
    (f_atom_string x);
@@ -1465,9 +1487,10 @@ and fTYPED_FORMULA = function
    fFORMULA x2;
    fNODE "typed_formula" 2
 and fUNFOLD = function
+| CT_coerce_ID_to_UNFOLD x -> fID x
 | CT_unfold_occ(x1, x2) ->
-   fINT_LIST x1;
-   fID x2;
+   fID x1;
+   fINT_NE_LIST x2;
    fNODE "unfold_occ" 2
 and fUNFOLD_LIST = function
 | CT_unfold_list l ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index d0617bd6e..265975dc0 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -113,6 +113,13 @@ let ident_tac s = CT_user_tac (xlate_ident s, CT_targ_list []);;
 
 let ident_vernac s = CT_user_vernac (CT_ident s, CT_varg_list []);;
 
+let nums_to_int_list_aux l = List.map (fun x -> CT_int x) l;;
+
+let nums_to_int_list l =  CT_int_list(nums_to_int_list_aux l);;
+
+let nums_to_int_ne_list n l =
+  CT_int_ne_list(CT_int n, nums_to_int_list_aux l);;
+
 type iTARG =   Targ_command of ct_FORMULA
              | Targ_intropatt of ct_INTRO_PATT_LIST
              | Targ_id_list of ct_ID_LIST
@@ -261,11 +268,12 @@ let rec xlate_match_pattern =
     | CPatNotation _ -> xlate_error "CPatNotation";;
 
 
+let xlate_id_opt_aux = function
+    Name id -> ctf_ID_OPT_SOME(CT_ident (string_of_id id))
+  | Anonymous -> ctv_ID_OPT_NONE;;
 
 
-let xlate_id_opt = function
-  | (_,Name id) -> ctf_ID_OPT_SOME(CT_ident (string_of_id id))
-  | (_,Anonymous) -> ctv_ID_OPT_NONE;;
+let xlate_id_opt (_, v) = xlate_id_opt_aux v;;
 
 let xlate_id_opt_ne_list = function
     [] -> assert false
@@ -318,16 +326,18 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
    | CLetIn(_, v, a, b) -> 
        CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
-   | CAppExpl(_, (_,r), l) -> (* TODO: proj notation *)
+   | CAppExpl(_, (_, r), l) -> (* TODO: proj notation *)
        CT_appc(CT_bang(xlate_int_opt None, varc (xlate_reference r)),
 	       xlate_formula_ne_list l)
    | CApp(_, (_,f), l) -> (* TODO: proj notation *)
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
-   | CCases (_,(po,None),tml,eqns)-> CT_cases(xlate_formula_opt po, 
-                         xlate_formula_ne_list (List.map fst tml),
-                         CT_eqn_list (List.map 
-         (fun x -> translate_one_equation x)
-			   eqns))
+   | CCases (_, _, [], _) -> assert false
+   | CCases (_, (Some _, _), _, _) -> xlate_error "TODO: Cases with Some"
+   | CCases (_,(None, None), tm::tml, eqns)->
+       CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
+					   List.map xlate_matched_formula tml),
+		ctv_FORMULA_OPT_NONE,
+                CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns))
    | CCases (_,(po,Some _),tml,eqns)-> xlate_error "TODO"
    | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> 
 		   CT_if(xlate_formula_opt po,
@@ -386,6 +396,15 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		       lmi)) 
    | CCoFix _ -> assert false
    | CFix _ -> assert false
+and xlate_matched_formula = function
+    (f, (Some x, Some y)) ->
+      CT_formula_as_in(xlate_formula f, xlate_id_opt_aux x, xlate_formula y)
+  | (f, (None, Some y)) ->
+      CT_formula_in(xlate_formula f, xlate_formula y)
+  | (f, (Some x, None)) ->
+      CT_formula_as(xlate_formula f, xlate_id_opt_aux x)
+  | (f, (None, None)) -> 
+      CT_coerce_FORMULA_to_MATCHED_FORMULA(xlate_formula f)
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
   | (a, Some (_,ExplByPos i)) -> 
@@ -410,21 +429,27 @@ let xlate_hyp = function
 
 let xlate_hyp_location =
  function
-  | AI (_,id), _, (InHypTypeOnly,_) -> CT_intype(xlate_ident id)
+  | AI (_,id), nums, (InHypTypeOnly,_) ->
+      CT_intype(xlate_ident id, nums_to_int_list nums)
   | AI (_,id), _, (InHyp,_) when !Options.v7 ->
-      CT_coerce_ID_to_HYP_LOCATION (xlate_ident id)
+      CT_coerce_UNFOLD_to_HYP_LOCATION 
+	(CT_coerce_ID_to_UNFOLD (xlate_ident id))
   | AI (_,id), _, ((InHypValueOnly|InHyp),_) ->
       xlate_error "TODO in v8: InHyp now means InHyp if variable but InHypValueOnly if a local definition"
   | MetaId _, _,_ -> 
       xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
 
 let xlate_clause cls =
+  let hyps_info =
+    match cls.onhyps with
+    	None -> CT_coerce_STAR_to_HYP_LOCATION_LIST_OR_STAR CT_star
+      | Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in
   CT_clause
-    (CT_hyp_location_list_opt
-      (option_app
-        (fun l -> CT_hyp_location_list(List.map xlate_hyp_location l))
-        cls.onhyps),
-      if cls.onconcl then CT_true else CT_false)
+    (hyps_info, 
+     if cls.onconcl then 
+       CT_coerce_STAR_to_STAR_OPT CT_star
+     else
+       CT_coerce_NONE_to_STAR_OPT CT_none)
 
 (** Tactics
    *)
@@ -585,23 +610,26 @@ let xlate_using = function
   | Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);;
 
 let xlate_one_unfold_block = function
-    (nums,qid) -> 
-      CT_unfold_occ (CT_int_list (List.map (fun x -> CT_int x) nums),
-		     tac_qualid_to_ct_ID qid);;
+    ([],qid) -> CT_coerce_ID_to_UNFOLD(tac_qualid_to_ct_ID qid)
+  | (n::nums, qid) ->
+      CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_to_int_ne_list n nums);;
 
 let xlate_lettac_clauses = function
     (opt_l, l') ->
       let res = 
 	(List.map 
-	   (fun (id, l) -> 
-	      CT_unfold_occ(CT_int_list (List.map (fun x -> CT_int x) l),
-			    xlate_ident_or_metaid id)) l') in
+	   (function
+		(id, []) -> 
+		  CT_coerce_ID_to_UNFOLD(xlate_ident_or_metaid id)
+	      | (id, n::nums) ->
+	      CT_unfold_occ(xlate_ident_or_metaid id, nums_to_int_ne_list n nums)) l') in
 	match opt_l with
-	    Some l ->
+	    Some (n::nums) ->
 	      CT_unfold_list
 	      	((CT_unfold_occ
-		    (CT_int_list (List.map (fun x -> CT_int x) l),
-		     CT_ident "Goal"))::res)
+		    (CT_ident "Goal", nums_to_int_ne_list n nums))::res)
+	  | Some [] ->
+	      CT_unfold_list((CT_coerce_ID_to_UNFOLD(CT_ident "Goal"))::res)
 	  | None -> CT_unfold_list res;;
 
 let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
@@ -919,7 +947,9 @@ and xlate_tac =
         (if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none))
     | TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt)
     | TacAuto (nopt, Some []) -> CT_auto (xlate_int_opt nopt)
-    | TacAuto (nopt, None) -> CT_auto_with (xlate_int_opt nopt, CT_star)
+    | TacAuto (nopt, None) ->
+ 	CT_auto_with (xlate_int_opt nopt,
+		      CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
     | TacAuto (nopt, Some (id1::idl)) ->
 	CT_auto_with(xlate_int_opt nopt,
              CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
@@ -937,7 +967,9 @@ and xlate_tac =
 	    | None -> none_in_id_or_int_opt in
 	let idl = out_gen Eauto.rawwit_hintbases idl in
           (match idl with
-	    None -> CT_eauto_with(first_n, second_n, CT_star)
+	    None -> CT_eauto_with(first_n,
+				  second_n,
+				  CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
 	  | Some [] -> CT_eauto(first_n, second_n)
 	  | Some (a::l) -> 
 	      CT_eauto_with(first_n, second_n,
@@ -955,7 +987,8 @@ and xlate_tac =
      let c = xlate_formula c and bindl = xlate_bindings bindl in
      CT_eapply (c, bindl)
     | TacTrivial (Some []) -> CT_trivial
-    | TacTrivial None -> CT_trivial_with(CT_star)
+    | TacTrivial None -> 
+	CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
     | TacTrivial (Some (id1::idl)) ->
 	 CT_trivial_with(CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
             (CT_id_ne_list(CT_ident id1,List.map (fun x -> CT_ident x) idl))))
@@ -1262,8 +1295,7 @@ let build_record_field_list l =
   | AssumExpr (id,c) ->
       if coe then CT_constr_coercion (xlate_id_opt id, xlate_formula c)
       else
-	CT_coerce_CONSTR_to_RECCONSTR
-	  (xlate_id_opt id, xlate_formula c)
+	CT_recconstr(xlate_id_opt id, xlate_formula c)
   | DefExpr (id,c,topt) ->
       xlate_error "TODO: manifest fields in Record" in
  CT_recconstr_list (List.map build_record_field l);;
@@ -1455,10 +1487,9 @@ let xlate_vernac =
   | VernacShow (ShowIntros _|ShowGoalImplicitly _|ShowExistentials|ShowScript)
       -> xlate_error "TODO: Show Intro/Intros/Implicits/Existentials/Script"
   | VernacGo arg -> CT_go (xlate_locn arg)
-  | VernacShow ExplainProof l ->
-      CT_explain_proof (CT_int_list (List.map (fun x -> CT_int x) l))
+  | VernacShow ExplainProof l -> CT_explain_proof (nums_to_int_list l)
   | VernacShow ExplainTree l ->
-      CT_explain_prooftree (CT_int_list (List.map (fun x -> CT_int x) l))
+      CT_explain_prooftree (nums_to_int_list l)
   | VernacCheckGuard -> CT_guarded
   | VernacPrint p ->
       (match p with
@@ -1527,18 +1558,17 @@ let xlate_vernac =
 
   | (*Record from tactics/Record.v *)
     VernacRecord 
-      (_, (add_coercion, (_,s)), binders, CSort (_,c1), rec_constructor_or_none, field_list) ->
+      (_, (add_coercion, (_,s)), binders, c1,
+       rec_constructor_or_none, field_list) ->
       let record_constructor =
         xlate_ident_opt (option_app snd rec_constructor_or_none) in
       CT_record
        ((if add_coercion then CT_coercion_atm else
           CT_coerce_NONE_to_COERCION_OPT(CT_none)),
         xlate_ident s, xlate_binder_list binders, 
-	xlate_sort c1, record_constructor,
+	xlate_formula c1, record_constructor,
          build_record_field_list field_list)
 
-  |    VernacRecord _ -> xlate_error "TODO: Record in a defined sort"
-
 (* TODO
      | (*Inversions from tactics/Inv.v *)
        "MakeSemiInversionLemmaFromHyp",
@@ -1694,7 +1724,7 @@ let xlate_vernac =
 	(reference_to_ct_ID id,
 	 match opt_positions with
 	     None -> CT_int_list[]
-	   | Some l ->
+	   | Some l -> 
 	       CT_int_list
 	       (List.map (function ExplByPos x -> CT_int x | ExplByName _ ->
 		 xlate_error "TODO: explicit argument by name") l))