Add translations for many tactics but a dozen are still remaining

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

3 files changed, 163 insertions, 46 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index a72963293..d9641bd34 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -194,6 +194,9 @@ and ct_DEFN_OR_THM =
 and ct_DEF_BODY =
     CT_coerce_CONTEXT_PATTERN_to_DEF_BODY of ct_CONTEXT_PATTERN
   | CT_coerce_EVAL_CMD_to_DEF_BODY of ct_EVAL_CMD
+and ct_DEF_BODY_OPT =
+    CT_coerce_DEF_BODY_to_DEF_BODY_OPT of ct_DEF_BODY
+  | CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT of ct_FORMULA_OPT
 and ct_DEP =
     CT_dep of string
 and ct_DESTRUCTING =
@@ -278,6 +281,11 @@ and ct_ID_OPT_OR_ALL =
 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
+and ct_ID_OR_INTYPE =
+    CT_coerce_ID_to_ID_OR_INTYPE of ct_ID
+  | CT_intype of ct_ID
+and ct_ID_OR_INTYPE_LIST =
+    CT_id_or_intype_list of ct_ID_OR_INTYPE list
 and ct_ID_OR_INT_OPT =
     CT_coerce_ID_OPT_to_ID_OR_INT_OPT of ct_ID_OPT
   | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT of ct_ID_OR_INT
@@ -324,7 +332,7 @@ and ct_IN_OR_OUT_MODULES =
   | CT_in_modules of ct_ID_NE_LIST
   | CT_out_modules of ct_ID_NE_LIST
 and ct_LET_CLAUSE =
-    CT_let_clause of ct_ID * ct_LET_VALUE
+    CT_let_clause of ct_ID * ct_DEF_BODY_OPT * ct_LET_VALUE
 and ct_LET_CLAUSES =
     CT_let_clauses of ct_LET_CLAUSE * ct_LET_CLAUSE list
 and ct_LET_VALUE =
@@ -369,6 +377,9 @@ and ct_PATTERN =
     CT_pattern_occ of ct_INT_LIST * ct_FORMULA
 and ct_PATTERN_NE_LIST =
     CT_pattern_ne_list of ct_PATTERN * ct_PATTERN list
+and ct_PATTERN_OPT =
+    CT_coerce_NONE_to_PATTERN_OPT of ct_NONE
+  | CT_coerce_PATTERN_to_PATTERN_OPT of ct_PATTERN
 and ct_PREMISE =
     CT_coerce_TYPED_FORMULA_to_PREMISE of ct_TYPED_FORMULA
   | CT_eval_result of ct_FORMULA * ct_FORMULA * ct_FORMULA
@@ -395,7 +406,7 @@ and ct_RED_COM =
   | CT_lazy of ct_CONVERSION_FLAG_LIST * ct_CONV_SET
   | CT_pattern of ct_PATTERN_NE_LIST
   | CT_red
-  | CT_simpl
+  | CT_simpl of ct_PATTERN_OPT
   | CT_unfold of ct_UNFOLD_NE_LIST
 and ct_RULE =
     CT_rule of ct_PREMISES_LIST * ct_FORMULA
@@ -435,9 +446,11 @@ and ct_STRING_OPT =
     CT_coerce_NONE_to_STRING_OPT of ct_NONE
   | CT_coerce_STRING_to_STRING_OPT of ct_STRING
 and ct_TACTIC_ARG =
-    CT_coerce_FORMULA_to_TACTIC_ARG of ct_FORMULA
+    CT_coerce_EVAL_CMD_to_TACTIC_ARG of ct_EVAL_CMD
+  | CT_coerce_FORMULA_to_TACTIC_ARG of ct_FORMULA
   | CT_coerce_ID_OR_INT_to_TACTIC_ARG of ct_ID_OR_INT
   | CT_coerce_TACTIC_COM_to_TACTIC_ARG of ct_TACTIC_COM
+  | CT_coerce_TERM_CHANGE_to_TACTIC_ARG of ct_TERM_CHANGE
   | CT_void
 and ct_TACTIC_ARG_LIST =
     CT_tactic_arg_list of ct_TACTIC_ARG * ct_TACTIC_ARG list
@@ -454,7 +467,8 @@ and ct_TACTIC_COM =
   | CT_case_type of ct_FORMULA
   | CT_casetac of ct_FORMULA * ct_SPEC_LIST
   | CT_cdhyp of ct_ID
-  | CT_change of ct_FORMULA * ct_ID_LIST
+  | CT_change of ct_FORMULA * ct_ID_OR_INTYPE_LIST
+  | CT_change_local of ct_PATTERN * ct_FORMULA * ct_ID_OR_INTYPE_LIST
   | CT_clear of ct_ID_NE_LIST
   | CT_cofixtactic of ct_ID_OPT * ct_COFIX_TAC_LIST
   | CT_condrewrite_lr of ct_TACTIC_COM * ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
@@ -466,6 +480,8 @@ and ct_TACTIC_COM =
   | CT_cutrewrite_rl of ct_FORMULA * ct_ID_OPT
   | CT_dconcl
   | CT_decompose_list of ct_ID_NE_LIST * ct_FORMULA
+  | CT_decompose_record of ct_FORMULA
+  | CT_decompose_sum of ct_FORMULA
   | CT_depinversion of ct_INV_TYPE * ct_ID_OR_INT * ct_FORMULA_OPT
   | CT_deprewrite_lr of ct_ID
   | CT_deprewrite_rl of ct_ID
@@ -492,11 +508,12 @@ and ct_TACTIC_COM =
   | CT_intro of ct_ID_OPT
   | CT_intro_after of ct_ID_OPT * ct_ID
   | CT_intros of ct_INTRO_PATT_LIST
-  | CT_intros_until of ct_ID
+  | CT_intros_until of ct_ID_OR_INT
   | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_ID_LIST
   | CT_left of ct_SPEC_LIST
   | CT_lettac of ct_LET_CLAUSES * ct_LET_VALUE
   | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
+  | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_tac of ct_LET_VALUE * ct_MATCH_TAC_RULES
   | CT_move_after of ct_ID * ct_ID
   | CT_omega
@@ -506,8 +523,9 @@ and ct_TACTIC_COM =
   | CT_progress of ct_TACTIC_COM
   | CT_prolog of ct_FORMULA_LIST * ct_INT
   | CT_rec_tactic_in of ct_REC_TACTIC_FUN_LIST * ct_TACTIC_COM
-  | CT_reduce of ct_RED_COM * ct_ID_LIST
+  | CT_reduce of ct_RED_COM * ct_ID_OR_INTYPE_LIST
   | CT_reflexivity
+  | CT_rename of ct_ID * ct_ID
   | CT_repeat of ct_TACTIC_COM
   | CT_replace_with of ct_FORMULA * ct_FORMULA
   | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
@@ -549,6 +567,9 @@ and ct_TARG =
   | CT_coerce_UNFOLD_NE_LIST_to_TARG of ct_UNFOLD_NE_LIST
 and ct_TARG_LIST =
     CT_targ_list of ct_TARG list
+and ct_TERM_CHANGE =
+    CT_check_term of ct_FORMULA
+  | CT_inst_term of ct_ID * ct_FORMULA
 and ct_TEXT =
     CT_coerce_ID_to_TEXT of ct_ID
   | CT_text_formula of ct_FORMULA
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 3e7cfd82a..34cb2a816 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -506,6 +506,9 @@ and fDEFN = function
 and fDEF_BODY = function
 | CT_coerce_CONTEXT_PATTERN_to_DEF_BODY x -> fCONTEXT_PATTERN x
 | CT_coerce_EVAL_CMD_to_DEF_BODY x -> fEVAL_CMD x
+and fDEF_BODY_OPT = function
+| CT_coerce_DEF_BODY_to_DEF_BODY_OPT x -> fDEF_BODY x
+| CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT x -> fFORMULA_OPT x
 and fDEP = function
 | CT_dep x -> fATOM "dep";
    (f_atom_string x);
@@ -700,6 +703,15 @@ and fID_OPT_OR_ALL = function
 and fID_OR_INT = function
 | CT_coerce_ID_to_ID_OR_INT x -> fID x
 | CT_coerce_INT_to_ID_OR_INT x -> fINT x
+and fID_OR_INTYPE = function
+| CT_coerce_ID_to_ID_OR_INTYPE x -> fID x
+| CT_intype(x1) ->
+   fID x1;
+   fNODE "intype" 1
+and fID_OR_INTYPE_LIST = function
+| CT_id_or_intype_list l ->
+   (List.iter fID_OR_INTYPE l);
+   fNODE "id_or_intype_list" (List.length l)
 and fID_OR_INT_OPT = function
 | CT_coerce_ID_OPT_to_ID_OR_INT_OPT x -> fID_OPT x
 | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT x -> fID_OR_INT x
@@ -772,10 +784,11 @@ and fIN_OR_OUT_MODULES = function
    fID_NE_LIST x1;
    fNODE "out_modules" 1
 and fLET_CLAUSE = function
-| CT_let_clause(x1, x2) ->
+| CT_let_clause(x1, x2, x3) ->
    fID x1;
-   fLET_VALUE x2;
-   fNODE "let_clause" 2
+   fDEF_BODY_OPT x2;
+   fLET_VALUE x3;
+   fNODE "let_clause" 3
 and fLET_CLAUSES = function
 | CT_let_clauses(x,l) ->
    fLET_CLAUSE x;
@@ -846,6 +859,9 @@ and fPATTERN_NE_LIST = function
    fPATTERN x;
    (List.iter fPATTERN l);
    fNODE "pattern_ne_list" (1 + (List.length l))
+and fPATTERN_OPT = function
+| CT_coerce_NONE_to_PATTERN_OPT x -> fNONE x
+| CT_coerce_PATTERN_to_PATTERN_OPT x -> fPATTERN x
 and fPREMISE = function
 | CT_coerce_TYPED_FORMULA_to_PREMISE x -> fTYPED_FORMULA x
 | CT_eval_result(x1, x2, x3) ->
@@ -908,7 +924,9 @@ and fRED_COM = function
    fPATTERN_NE_LIST x1;
    fNODE "pattern" 1
 | CT_red -> fNODE "red" 0
-| CT_simpl -> fNODE "simpl" 0
+| CT_simpl(x1) ->
+   fPATTERN_OPT x1;
+   fNODE "simpl" 1
 | CT_unfold(x1) ->
    fUNFOLD_NE_LIST x1;
    fNODE "unfold" 1
@@ -978,9 +996,11 @@ and fSTRING_OPT = function
 | CT_coerce_NONE_to_STRING_OPT x -> fNONE x
 | CT_coerce_STRING_to_STRING_OPT x -> fSTRING x
 and fTACTIC_ARG = function
+| CT_coerce_EVAL_CMD_to_TACTIC_ARG x -> fEVAL_CMD x
 | CT_coerce_FORMULA_to_TACTIC_ARG x -> fFORMULA x
 | CT_coerce_ID_OR_INT_to_TACTIC_ARG x -> fID_OR_INT x
 | CT_coerce_TACTIC_COM_to_TACTIC_ARG x -> fTACTIC_COM x
+| CT_coerce_TERM_CHANGE_to_TACTIC_ARG x -> fTERM_CHANGE x
 | CT_void -> fNODE "void" 0
 and fTACTIC_ARG_LIST = function
 | CT_tactic_arg_list(x,l) ->
@@ -1030,8 +1050,13 @@ and fTACTIC_COM = function
    fNODE "cdhyp" 1
 | CT_change(x1, x2) ->
    fFORMULA x1;
-   fID_LIST x2;
+   fID_OR_INTYPE_LIST x2;
    fNODE "change" 2
+| CT_change_local(x1, x2, x3) ->
+   fPATTERN x1;
+   fFORMULA x2;
+   fID_OR_INTYPE_LIST x3;
+   fNODE "change_local" 3
 | CT_clear(x1) ->
    fID_NE_LIST x1;
    fNODE "clear" 1
@@ -1072,6 +1097,12 @@ and fTACTIC_COM = function
    fID_NE_LIST x1;
    fFORMULA x2;
    fNODE "decompose_list" 2
+| CT_decompose_record(x1) ->
+   fFORMULA x1;
+   fNODE "decompose_record" 1
+| CT_decompose_sum(x1) ->
+   fFORMULA x1;
+   fNODE "decompose_sum" 1
 | CT_depinversion(x1, x2, x3) ->
    fINV_TYPE x1;
    fID_OR_INT x2;
@@ -1162,7 +1193,7 @@ and fTACTIC_COM = function
    fINTRO_PATT_LIST x1;
    fNODE "intros" 1
 | CT_intros_until(x1) ->
-   fID x1;
+   fID_OR_INT x1;
    fNODE "intros_until" 1
 | CT_inversion(x1, x2, x3) ->
    fINV_TYPE x1;
@@ -1180,6 +1211,10 @@ and fTACTIC_COM = function
    fCONTEXT_RULE x;
    (List.iter fCONTEXT_RULE l);
    fNODE "match_context" (1 + (List.length l))
+| CT_match_context_reverse(x,l) ->
+   fCONTEXT_RULE x;
+   (List.iter fCONTEXT_RULE l);
+   fNODE "match_context_reverse" (1 + (List.length l))
 | CT_match_tac(x1, x2) ->
    fLET_VALUE x1;
    fMATCH_TAC_RULES x2;
@@ -1214,9 +1249,13 @@ and fTACTIC_COM = function
    fNODE "rec_tactic_in" 2
 | CT_reduce(x1, x2) ->
    fRED_COM x1;
-   fID_LIST x2;
+   fID_OR_INTYPE_LIST x2;
    fNODE "reduce" 2
 | CT_reflexivity -> fNODE "reflexivity" 0
+| CT_rename(x1, x2) ->
+   fID x1;
+   fID x2;
+   fNODE "rename" 2
 | CT_repeat(x1) ->
    fTACTIC_COM x1;
    fNODE "repeat" 1
@@ -1323,6 +1362,14 @@ and fTARG_LIST = function
 | CT_targ_list l ->
    (List.iter fTARG l);
    fNODE "targ_list" (List.length l)
+and fTERM_CHANGE = function
+| CT_check_term(x1) ->
+   fFORMULA x1;
+   fNODE "check_term" 1
+| CT_inst_term(x1, x2) ->
+   fID x1;
+   fFORMULA x2;
+   fNODE "inst_term" 2
 and fTEXT = function
 | CT_coerce_ID_to_TEXT x -> fID x
 | CT_text_formula(x1) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 2e791e8d5..43a2aad72 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -87,6 +87,11 @@ let ctv_ID_OPT_OR_ALL_NONE =
 let ctv_FORMULA_OPT_NONE =
   CT_coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT CT_none);;
 
+let ctv_PATTERN_OPT_NONE = CT_coerce_NONE_to_PATTERN_OPT CT_none;;
+
+let ctv_DEF_BODY_OPT_NONE = CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT 
+			      ctv_FORMULA_OPT_NONE;;
+
 let ctf_ID_OPT_OR_ALL_SOME s =
  CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (ctf_ID_OPT_SOME s);;
 
@@ -218,7 +223,7 @@ let id_to_pattern_var ctid =
  | CT_ident id_string ->
      CT_coerce_ID_OPT_to_MATCH_PATTERN 
        (CT_coerce_ID_to_ID_OPT (CT_ident id_string))
- | _ -> assert false;;
+ | CT_metac _ -> assert false;;
 
 exception Not_natural;;
 
@@ -280,7 +285,8 @@ and xlate_formula_opt =
 
 and  xlate_binder_l = function
     LocalRawAssum(l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
-    |_ -> xlate_error "TODO: Local Def bindings";
+  | LocalRawDef(n,v) -> CT_coerce_DEF_to_BINDER(CT_def(xlate_id_opt n,
+						       xlate_formula v))
 and 
   xlate_match_pattern_ne_list = function
     [] -> assert false
@@ -333,7 +339,9 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
    | CNumeral(_, i) -> CT_int_encapsulator(Bignat.bigint_to_string i)
    | CHole _ -> CT_existvarc 
-   | CDynamic (_, _) -> xlate_error "TODO:CDynamic"
+(* I assume CDynamic has been inserted to make free form extension of
+   the language possible, but this would go agains the logic of pcoq anyway. *)
+   | CDynamic (_, _) -> assert false
    | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula  num)
    | CCast (_, e, t) -> 
        CT_coerce_TYPED_FORMULA_to_FORMULA
@@ -376,11 +384,12 @@ and xlate_formula_ne_list = function
 
 let xlate_hyp_location =
  function
-  | InHyp (AI (_,id)) -> xlate_ident id
+  | InHyp (AI (_,id)) -> CT_coerce_ID_to_ID_OR_INTYPE (xlate_ident id)
   | InHyp (MetaId _) -> xlate_error "MetaId should occur only in quotations"
-  | InHypType id -> xlate_error "TODO: in (Type of id)"
+  | InHypType(AI (_, id)) -> CT_intype(xlate_ident id)
+  | InHypType _ -> xlate_error "MetaId not supported in xlate_hyp_location"
 
-let xlate_clause l = CT_id_list (List.map xlate_hyp_location l)
+let xlate_clause l = CT_id_or_intype_list (List.map xlate_hyp_location l)
 
 (** Tactics
    *)
@@ -541,8 +550,12 @@ let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
 	failwith "Dynamics not treated in xlate_ast"
     | ConstrMayEval (ConstrTerm c) ->
 	CT_coerce_FORMULA_to_TACTIC_ARG (xlate_formula c)
-    | ConstrMayEval _ ->
-	xlate_error "TODO: Eval/Inst as tactic argument"
+    | ConstrMayEval(ConstrEval(r,c)) ->
+	CT_coerce_EVAL_CMD_to_TACTIC_ARG
+	  (CT_eval(CT_coerce_NONE_to_INT_OPT CT_none, xlate_red_tactic r,
+		   xlate_formula c))
+    | ConstrMayEval(ConstrTypeOf(c)) -> 
+	CT_coerce_TERM_CHANGE_to_TACTIC_ARG(CT_check_term(xlate_formula c))
     | MetaIdArg _ ->
 	xlate_error "MetaIdArg should only be used in quotations"
     | MetaNumArg (_,n) ->
@@ -559,15 +572,19 @@ and (xlate_call_or_tacarg:raw_tactic_arg -> ct_TACTIC_COM) =
 	  (reference_to_ct_ID r,
 	    CT_tactic_arg_list(xlate_tacarg a,List.map xlate_tacarg l))
     | Reference (Ident (_,s)) -> ident_tac s
-    | t -> xlate_error "TODO: result other than tactic or constr"
+    | t -> xlate_error "TODO LATER: result other than tactic or constr"
 
 and xlate_red_tactic =
  function
   | Red true -> xlate_error ""
   | Red false -> CT_red
   | Hnf -> CT_hnf
-  | Simpl None -> CT_simpl
-  | Simpl (Some c) -> xlate_error "Simpl: TODO"
+  | Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
+  | Simpl (Some (l,c)) -> 
+      CT_simpl 
+	(CT_coerce_PATTERN_to_PATTERN_OPT
+	   (CT_pattern_occ
+	      (CT_int_list(List.map (fun n -> CT_int n) l), xlate_formula c)))
   | Cbv flag_list ->
      let conv_flags, red_ids = get_flag flag_list in
      CT_cbv (CT_conversion_flag_list conv_flags, red_ids)
@@ -591,7 +608,27 @@ and xlate_red_tactic =
      (match pat_list with
       | first :: others -> CT_pattern (CT_pattern_ne_list (first, others))
       | [] -> error "Expecting at least one pattern in a Pattern command")
-  | ExtraRedExpr _ -> xlate_error "TODO: ExtraRedExpr"
+  | ExtraRedExpr _ -> xlate_error "TODO LATER: ExtraRedExpr (probably dead code)"
+
+and xlate_rec_tac = function
+  | ((_,x),TacFun (argl,tac)) ->
+      let fst, rest = xlate_largs_to_id_unit ((Some x)::argl) in
+	CT_rec_tactic_fun(xlate_ident x,
+			  CT_id_unit_list(fst, rest),
+			  xlate_tactic tac)
+  | ((_,x),tac) ->
+      CT_rec_tactic_fun(xlate_ident x,
+			CT_id_unit_list (xlate_id_unit (Some x), []),
+			xlate_tactic tac)
+
+and xlate_local_rec_tac = function 
+ (* TODO LATER: local recursive tactics and global ones should be handled in
+    the same manner *)
+  | ((_,x),(argl,tac)) ->
+      let fst, rest = xlate_largs_to_id_unit ((Some x)::argl) in
+	CT_rec_tactic_fun(xlate_ident x,
+			  CT_id_unit_list(fst, rest),
+			  xlate_tactic tac)
 
 and xlate_tactic =
  function
@@ -640,33 +677,47 @@ and xlate_tactic =
                          | fst::others ->
                              CT_match_tac_rules(fst, others))
    | TacMatchContext (_,[]) -> failwith ""
-   | TacMatchContext (lr,rule1::rules) ->
-         (* TODO : traiter la direction "lr" *)
+   | TacMatchContext (false,rule1::rules) ->
          CT_match_context(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
+   | TacMatchContext (true,rule1::rules) ->
+         CT_match_context_reverse(xlate_context_rule rule1,
+                          List.map xlate_context_rule rules)
    | TacLetIn (l, t) ->
        let cvt_clause =
          function
              ((_,s),None,ConstrMayEval v) ->
                  CT_let_clause(xlate_ident s,
+			       ctv_DEF_BODY_OPT_NONE,
                                CT_coerce_DEF_BODY_to_LET_VALUE
                                (formula_to_def_body v))
            | ((_,s),None,Tacexp t) -> 
                  CT_let_clause(xlate_ident s,
+			       ctv_DEF_BODY_OPT_NONE,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
                                (xlate_tactic t))
            | ((_,s),None,t) -> 
                  CT_let_clause(xlate_ident s,
+			       ctv_DEF_BODY_OPT_NONE,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
                                (xlate_call_or_tacarg t))
-           | ((_,s),Some c,v) -> xlate_error "TODO: Let id : c := t In t'" in
+           | ((_,s),Some c,t) -> 
+	       CT_let_clause(xlate_ident s,
+			     CT_coerce_DEF_BODY_to_DEF_BODY_OPT
+			     (formula_to_def_body c),
+                               CT_coerce_TACTIC_COM_to_LET_VALUE
+				 (xlate_call_or_tacarg t)) in
          let cl_l = List.map cvt_clause l in
          (match cl_l with
             | [] -> assert false 
             | fst::others ->
                 CT_lettac (CT_let_clauses(fst, others), mk_let_value t))
    | TacLetCut _ -> xlate_error "Unclear future of syntax Let x := t"
-   | TacLetRecIn _ -> xlate_error "TODO: Rec x = t In"
+   | TacLetRecIn([], _) -> xlate_error "recursive definition with no definition"
+   | TacLetRecIn(f1::l, t) -> 
+       let tl =  CT_rec_tactic_fun_list
+		   (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
+       CT_rec_tactic_in(tl, xlate_tactic t)
    | TacAtom (_, t) -> xlate_tac t 
    | TacFail n -> CT_fail (CT_int n)
    | TacId -> CT_idtac
@@ -678,7 +729,13 @@ and xlate_tac =
     | TacExtend (_,"Absurd",[c]) ->
        CT_absurd (xlate_formula (out_gen rawwit_constr c))
     | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
-    | TacChange (_, f, b) -> xlate_error "TODO: Change subterms"
+    | TacChange (Some(l,c), f, b) -> 
+	(* TODO LATER: combine with other constructions of pattern_occ *)
+	CT_change_local(
+	  CT_pattern_occ(CT_int_list(List.map (fun n -> CT_int n) l), 
+			 xlate_formula c),
+	  xlate_formula f,
+	  xlate_clause b)
     | TacExtend (_,"Contradiction",[]) -> CT_contradiction
     | TacDoubleInduction (n1, n2) ->
 	CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2)
@@ -707,8 +764,10 @@ and xlate_tac =
      CT_cofixtactic
       (CT_coerce_ID_to_ID_OPT (xlate_ident id),
       CT_cofix_tac_list (List.map f cofixtac_list))
-    | TacIntrosUntil (NamedHyp id) -> CT_intros_until (xlate_ident id)
-    | TacIntrosUntil (AnonHyp n) -> xlate_error "TODO: Intros until n"
+    | TacIntrosUntil (NamedHyp id) -> 
+	CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
+    | TacIntrosUntil (AnonHyp n) -> 
+	CT_intros_until (CT_coerce_INT_to_ID_OR_INT (CT_int n))
     | TacIntroMove (Some id1, Some (_,id2)) ->
      CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_ident id2)
     | TacIntroMove (None, Some (_,id2)) ->
@@ -866,8 +925,8 @@ and xlate_tac =
 	let id' = qualid_or_meta_to_ct_ID id in
 	let l' = List.map qualid_or_meta_to_ct_ID l in
         CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c)
-    | TacDecomposeAnd c -> xlate_error "TODO: Decompose Record"
-    | TacDecomposeOr c -> xlate_error "TODO: Decompose Sum"
+    | TacDecomposeAnd c -> CT_decompose_record (xlate_formula c)
+    | TacDecomposeOr c -> CT_decompose_sum(xlate_formula c)
     | TacClear [] ->
 	xlate_error "Clear expects a non empty list of identifiers"
     | TacClear (id::idl) ->
@@ -904,7 +963,7 @@ and xlate_tac =
      CT_use_inversion (id, xlate_formula c,
        CT_id_list (List.map xlate_ident idlist))
     | TacExtend (_,"Omega", []) -> CT_omega
-    | TacRename (_, _) -> xlate_error "TODO: Rename id into id'"
+    | TacRename ((_,id1), (_,id2)) -> CT_rename(xlate_ident id1, xlate_ident id2)
     | TacClearBody _ -> xlate_error "TODO: Clear Body H"
     | TacDAuto (_, _) -> xlate_error "TODO: DAuto"
     | TacNewDestruct _ -> xlate_error "TODO: NewDestruct"
@@ -1173,17 +1232,7 @@ let xlate_vernac =
    | VernacDeclareTacticDefinition 
        (true,((id,TacFun (largs,tac))::_ as the_list)) ->
        let x_rec_tacs =
-	 List.map
-           (function
-	     | ((_,x),TacFun (argl,tac)) ->
-		  let fst, rest = xlate_largs_to_id_unit ((Some x)::argl) in
-	 	  CT_rec_tactic_fun(xlate_ident x,
-				 CT_id_unit_list(fst, rest),
-				 xlate_tactic tac)
-	     | ((_,x),tac) ->
-	 	  CT_rec_tactic_fun(xlate_ident x,
-				 CT_id_unit_list (xlate_id_unit (Some x), []),
-				 xlate_tactic tac)) the_list in
+	 List.map xlate_rec_tac the_list in
        let fst, others = match x_rec_tacs with
 	   fst::others -> fst, others
 	 | _ -> assert false in