removes all references to ctast.ml the Makefile has been updated accordingly.

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

8 files changed, 80 insertions, 427 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index b62339fa5..a72963293 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -228,10 +228,11 @@ and ct_FORMULA =
   | CT_bang of ct_INT_OPT * ct_FORMULA
   | CT_cases of ct_FORMULA_OPT * ct_FORMULA_NE_LIST * ct_EQN_LIST
   | CT_cofixc of ct_ID * ct_COFIX_REC_LIST
-  | CT_elimc of ct_CASE * ct_FORMULA * ct_FORMULA * ct_FORMULA_LIST
+  | 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_OPT * ct_FORMULA * ct_FORMULA * ct_FORMULA
+  | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
   | CT_int_encapsulator of string
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
   | CT_letin of ct_DEF * ct_FORMULA
@@ -519,7 +520,7 @@ and ct_TACTIC_COM =
   | CT_split of ct_SPEC_LIST
   | CT_superauto of ct_INT_OPT * ct_ID_LIST * ct_DESTRUCTING * ct_USINGTDB
   | CT_symmetry
-  | CT_tac_double of ct_INT * ct_INT
+  | CT_tac_double of ct_ID_OR_INT * ct_ID_OR_INT
   | CT_tacsolve of ct_TACTIC_COM * ct_TACTIC_COM list
   | CT_tactic_fun of ct_ID_UNIT_LIST * ct_TACTIC_COM
   | CT_then of ct_TACTIC_COM * ct_TACTIC_COM list
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 1a660a89f..fe25cb07d 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -37,7 +37,7 @@ open Translate;;
 open Name_to_ast;;
 open Pbp;;
 open Blast;;
-open Dad;;
+(* open Dad;; *)
 open Debug_tac;;
 open Search;;
 open Constrintern;;
@@ -330,11 +330,13 @@ let globcv x =
 	       (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
+(* <\cpa> 
 let pbp_tac_pcoq =
     pbp_tac (function (x:raw_tactic_expr) -> 
       output_results
         (ctf_header "pbp_results" !global_request_id)
        (Some (P_t(xlate_tactic x))));;
+</cpa> *)
 
 let blast_tac_pcoq =
     blast_tac (function (x:raw_tactic_expr) -> 
@@ -342,12 +344,13 @@ let blast_tac_pcoq =
 	(ctf_header "pbp_results" !global_request_id)
        (Some (P_t(xlate_tactic x))));;
 
-
+(* <\cpa> 
 let dad_tac_pcoq =
   dad_tac(function x -> 
     output_results
     (ctf_header "pbp_results" !global_request_id)
     (Some (P_t(xlate_tactic x))));;
+</cpa> *)
 
 let search_output_results () =
   output_results
@@ -551,6 +554,9 @@ let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
 let pcoq_search s l =
   ctv_SEARCH_LIST:=[];
   begin match s with
+  | SearchAbout locqid -> 
+      raw_search_about (filter_by_module_from_list l) add_search
+	(Nametab.global locqid)
   | SearchPattern c ->
       let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
       raw_pattern_search (filter_by_module_from_list l) add_search pat
@@ -573,7 +579,7 @@ let pcoq_print_check j =
   let a,b = print_check j in output_results a b
 
 let pcoq_print_eval redfun env c j =
-  let strm, vtp = ct_print_eval (Ctast.ast_to_ct c) redfun env j in
+  let strm, vtp = ct_print_eval c redfun env j in
   output_results strm vtp;;
 
 open Vernacentries
@@ -879,6 +885,7 @@ let command_creations = [
 ];;
 *)
 
+(* <\cpa> 
 TACTIC EXTEND Pbp
 | [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> 
     [ if_pcoq pbp_tac_pcoq idopt nl ]
@@ -891,6 +898,7 @@ TACTIC EXTEND Dad
 | [ "Dad" natural_list(nl1) "to" natural_list(nl2) ] ->
     [ if_pcoq dad_tac_pcoq nl1 nl2 ]
 END
+ </cpa> *)
 
 TACTIC EXTEND CtDebugTac
 | [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq t ]
@@ -904,8 +912,9 @@ END
 let start_pcoq_mode debug = 
   begin
     pcoq_started := Some debug;
+(* <\cpa> 
     start_dad();
-    set_xlate_mut_stuff (fun x ->Ctast.ast_to_ct (globcv (Ctast.ct_to_ast x)));
+</cpa> *)
     declare_in_coq();
 (*
     add_tactic "PcoqPbp" pbp_tac_pcoq;
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 00a4bb07e..4f03fb06f 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -11,7 +11,6 @@ open Tactics;;
 open Tacticals;;
 open Pattern;;
 open Reduction;;
-open Ctast;;
 open Constrextern;;
 open Constrintern;;
 open Vernacinterp;;
@@ -47,9 +46,7 @@ type dad_rule =
     constr_expr * int list * int list * int * int list
     * raw_atomic_tactic_expr;;
 
-(* This value will be used systematically when constructing objects of
-   type Ctast.t, the value is stupid and meaningless, but it is needed
-   to construct well-typed terms. *)
+(* This value will be used systematically when constructing objects *)
 
 let zz = (0,0);;
 
@@ -70,17 +67,7 @@ let rec get_subterm  (depth:int) (path: int list) (constr:constr) =
    first argument, an object of type env, is necessary to
    transform constr terms into abstract syntax trees.  The second argument is
    the substitution, a list of pairs linking an integer and a constr term. *)
-(*
-let map_subst (env :env) 
-   (subst:(int * Term.constr) list) =
-   let rec map_subst_aux = function
-    Coqast.Node(_, "META", [Coqast.Num(_, i)]) ->
-      let constr = List.assoc i subst in
-      ast_of_constr false env constr
-  | Coqast.Node(loc, s, l) -> Coqast.Node(loc, s, List.map map_subst_aux l)
-  | ast -> ast in
-    map_subst_aux;;
-*)
+
 let rec map_subst (env :env) (subst:(int * Term.constr) list) = function
   | CMeta (_,i) ->
       let constr = List.assoc i subst in
@@ -274,7 +261,7 @@ let start_dad () = dad_status := true;;
 
 let add_dad_rule_fn name pat p1 p2 tac =
   let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
-  add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr tac;;
+  add_dad_rule name pat p1 p2 (List.length pr) pr tac;;
 
 (* To be parsed by camlp4
 
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 80009d783..039127cc5 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -155,17 +155,7 @@ let make_variable_ast name typ implicits =
     ((Local,Definitional), [false,(name, constr_to_ast (body_of_type typ))]))
   ::(implicits_to_ast_list implicits);;
     
-(*
-let make_definition_ast name c typ implicits =
- (ope("DEFINITION",
-      [string "DEFINITION";
-       nvar name;
-       ope("COMMAND",
-           [ope("CAST",
-                [(constr_to_ast c);
-		 (constr_to_ast (body_of_type typ))])])]))::
-  (implicits_to_ast_list implicits);;
-*)
+
 let make_definition_ast name c typ implicits =
   VernacDefinition (Global, name, DefineBody ([], None,
     (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index bc9f706c5..d4d134f64 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -7,7 +7,6 @@ open Tacticals;;
 open Hipattern;;
 open Pattern;;
 open Reduction;;
-open Ctast;;
 open Rawterm;;
 open Environ;;
 
@@ -88,34 +87,9 @@ type pbp_rule = (identifier list *
                        identifier option -> (types, constr) kind_of_term -> int list -> pbp_sequence)) ->
                     pbp_sequence option;;
 
-(*
-let make_named_intro s =
-    Node(zz, "Intros",
-          [Node(zz,"INTROPATTERN",
-            [Node(zz,"LISTPATTERN",
-              [Node(zz, "IDENTIFIER", 
-                [Nvar(zz, s)])])])]);;
-*)
+
 let make_named_intro id = PbpIntros [id]
 
-(*
-let get_name_from_intro = function
-    Node(a, "Intros",
-          [Node(b,"INTROPATTERN",
-            [Node(c,"LISTPATTERN",
-              [Node(d, "IDENTIFIER", 
-                [Nvar(e, s)])])])]) ->
-		  Some s
-  | _ -> None;;
-*)
-(*
-let make_clears =  function
-    [] -> Node(zz, "Idtac",[])
-  | str_list ->
-      Node(zz, "TRY", [Node(zz,"Clear",
-	   [Node(zz, "CLAUSE", List.map (function s -> Nvar(zz,s)) str_list)])
-	       ]);;
-*)
 let make_clears str_list = PbpThen [PbpTryClear str_list]
 
 let add_clear_names_if_necessary tactic clear_names =
@@ -124,7 +98,6 @@ let add_clear_names_if_necessary tactic clear_names =
     | l -> chain_tactics [PbpTryClear l] tactic;;
 
 let make_final_cmd f optname clear_names constr path =
-(*    let tactic = f optname constr path in*)
     add_clear_names_if_necessary (f optname constr path) clear_names;;
 
 let (rem_cast:pbp_rule) = function
@@ -336,23 +309,7 @@ let (not_intro: pbp_rule) = function
 
 
 
-(*
-let elim_with_bindings hyp_name names =
-  Node(zz,"Elim", 
-       [Node(zz, "COMMAND", [Nvar(zz,hyp_name)]);
-	 Node(zz,"BINDINGS", 
-	      List.map 
-		(function s -> 
-		  Node(zz,"BINDING",
-		       [Nvar(zz,s);
-			 Node
-			   (zz,"COMMAND",
-			    [Node
-				(zz,"APPLIST",
-				 [Nvar(zz,"PBP_META");
-				   Nvar(zz,
-					"value_for_" ^ s)])])])) names)]);;
-*)
+
 let elim_with_bindings hyp_name names =
   PbpElim (hyp_name, names);;
 
@@ -448,114 +405,6 @@ let (mk_db_indices: int list -> int -> int list) =
    answer is true, then the built command takes advantage of the power of
    head tactics.  *)
 
-(*
-let (head_tactic_patt: pbp_rule) = function
-    avoid, clear_names, clear_flag, Some h, cstr, path, f ->
-    (match down_prods (cstr, path, 0) with
-    | (str_list, _, nprems, 
-       App(oper,[|c1|]), 2::1::path) 
-      	when
- 	  (is_matching_local (notconstr ()) oper) or
- 	  (is_matching_local (notTconstr ()) oper) ->
-	 Some(Node(zz, "TACTICLIST",
-		   [elim_with_bindings h str_list;
-		     f avoid clear_names false None (kind_of_term c1) path]))
-    | (str_list, _, nprems, 
-       App(oper, [|c1; c2|]), 2::a::path) 
-      when ((is_matching_local (andconstr()) oper) or
-	    (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
-	let h1 = next_global_ident_away (id_of_string "H") avoid in
-	let str_h1 = (string_of_id h1) in
-	let h2 = next_global_ident_away (id_of_string "H") (h1::avoid) in
-	let str_h2 = (string_of_id h2) in
-	Some(Node(zz,"TACTICLIST",
-                  [elim_with_bindings h str_list;
-		    make_named_intro str_h1;
-		    make_named_intro str_h2;
-		    let cont_body = 
-		      if a = 1 then c1 else c2 in
-		    let cont_tac = 
-		      f (h2::h1::avoid) (h::clear_names) 
-                        false (Some (if 1 = a then str_h1 else str_h2))
-                        (kind_of_term cont_body) path in
-		    if nprems = 0 then
-		      cont_tac
-		    else
-		      Node(zz,"TACLIST",
-			   cont_tac::(auxiliary_goals
-					clear_names clear_flag
-					h nprems))]))
-    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
-      when ((is_matching_local (exconstr ()) oper) or
-	    (is_matching_local (exTconstr ()) oper) or
-	    (is_matching_local (sigconstr ()) oper) or
-	    (is_matching_local (sigTconstr()) oper)) & a = 2 ->
-		   (match (kind_of_term c2),path with
-		     Lambda(Name x, _,body), (2::path) ->
-		       Some(Node(zz,"TACTICLIST",
-		    		 [elim_with_bindings h str_list;
-				   let x' = next_global_ident_away x avoid in
-				   let cont_body =
-				     Prod(Name x', c1,
-					    mkProd(Anonymous, body, 
-						   mkVar(dummy_id))) in
-				   let cont_tac 
-				       = f avoid (h::clear_names) false None
-				       cont_body (2::1::path) in
-				   if nprems = 0 then
-				     cont_tac
-				   else
-				     Node(zz,"TACLIST",
-					  cont_tac::(auxiliary_goals
-						       clear_names clear_flag
-						       h nprems))]))
-		   | _ -> None)
-    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
-	when ((is_matching_local (orconstr ()) oper) or
-              (is_matching_local (sumboolconstr ()) oper) or
-	      (is_matching_local (sumconstr ()) oper)) &
-                (a = 1 or a = 2) ->
-	  Some(Node(zz, "TACTICLIST",
-		    [elim_with_bindings h str_list;
-		      let cont_body =
-			if a = 1 then c1 else c2 in
-                      (* h' is the name for the new intro *)
-		      let h' = next_global_ident_away (id_of_string "H") avoid in
-		      let str_h' = (string_of_id h') in
-		      let cont_tac =
-                        Node(zz,"TACTICLIST",
-			     [make_named_intro str_h';
-			       f 
-				 (* h' should not be used again *)
-				 (h'::avoid)
-				 (* the disjunct itself can be discarded *)
-				 (h::clear_names) false (Some str_h')
-                          (kind_of_term cont_body) path]) in
-		      let snd_tac = 
-			Node(zz, "TACTICLIST", 
-			     [make_named_intro str_h';
-			       make_clears (h::clear_names)]) in
-		      let tacs1 = 
-			if a = 1 then
-			  [cont_tac; snd_tac]
-		      	else
-			  [snd_tac; cont_tac] in
-		      Node(zz,"TACLIST",
-			   tacs1@(auxiliary_goals (h::clear_names)
-				   false "dummy" nprems))]))
-    | (str_list, int_list, nprems, c, []) 
-        when  (check_apply c (mk_db_indices int_list nprems)) &
-              (match c with Prod(_,_,_) -> false
-              |  _ -> true) &
-              (List.length int_list) + nprems > 0 ->
-          Some(add_clear_names_if_necessary
-	     (Node(zz,"Apply", [Node(zz,"COMMAND",[Nvar(zz, h)]);
-			     Node(zz,"BINDINGS", [])]))
-             clear_names)
-    | _ -> None)
-  | _ -> None;;
-*)
-
 let (head_tactic_patt: pbp_rule) = function
     avoid, clear_names, clear_flag, Some h, cstr, path, f ->
     (match down_prods (cstr, path, 0) with
@@ -652,11 +501,6 @@ let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2;
 		      and_intro; or_intro; not_intro; ex_intro];;
 
 
-(* The tactic traced_try was intended to be used in tactics instead of
-   Try, with an argument  Node(zz, "TACTIC", [b]) where b is the tactic to
-   try.  However, the current design is not very robust to the fact that
-   Traced_Try may occur several times in the executed command! *)
-
 let try_trace = ref true;;
 
 let traced_try (f1:tactic) g =
@@ -670,24 +514,10 @@ let traced_try_entry = function
   |  _ -> failwith "traced_try_entry received wrong arguments";;
 
 
-let rec clean_trace flag =
-      function
-          Node(a,"Traced_Try", [Node(_,_,[b])]) ->
-             if flag then b else Node(zz,"Idtac",[])
-      	| Node(a,b,c) -> Node(a,b,List.map (clean_trace flag) c)
-        | t -> t;;
-
 (* When the recursive descent along the path is over, one includes the
    command requested by the point-and-shoot strategy.  Default is
    Try Assumption--Try Exact.  *)
 
-(*
-let default_ast optname constr path =
-      match optname with
-        None ->  Node(zz, "TRY", [Node(zz, "Assumption",[])])
-      | Some(a) -> Node(zz, "TRY", 
-                   [Node(zz, "Exact",[Node(zz,"COMMAND",[Nvar(zz,a)])])]);;
-*)
 
 let default_ast optname constr path = PbpThen [PbpTryAssumption optname]
 
@@ -710,100 +540,12 @@ let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path =
 (* these are the optimisation functions. *)
 (* This function takes care of flattening successive then commands. *)
 
-(*
-let rec optim1 =
-    function
-        Node(a,"TACTICLIST",b) ->
-          let tacs = List.map optim1 b in
-          let rec flatten = function
-            | [Node(a, "TACTICLIST", b')] ->
-                let rec last = function
-                    [] -> failwith "function last is called on an empty list"
-		  | [b] -> b
-		  | a::b -> last b in
-		(match last b' with
-		  Node(a, "TACLIST",_) -> [Node(a,"TACTICLIST", b')]
-		| _ -> flatten b')
-            | Node(a, "TACTICLIST", b')::others -> List.append (flatten b')
-                                                       (flatten others)
-            | Node(a, "Idtac",[])::others -> (flatten others)
-            | [Node(a, "TACLIST",tacs)] ->
-                 [Node(a, "TACLIST", List.map optim1 tacs)]
-            | t1::others -> t1::(flatten others)
-            | [] -> [] in
-          (match (flatten tacs) with
-            [] -> Node(zz,"Idtac", [])
-          | [t] -> t
-          | args -> Node(zz,"TACTICLIST", args))
-      |	t -> t;;
-*)
 
 (* Invariant: in [flatten_sequence t], occurrences of [PbpThenCont(l,t)] enjoy
     that t is some [PbpAtom t] *)
-(*
-let rec flatten_sequence =
-  function
-      PbpThens (tl1,tl2) -> PbpThens (tl1,List.map flatten_sequence tl2)
-    | PbpThen (tl1,t1) as x ->
-	(match flatten_sequence t1 with
-	  | PbpThenCont (tl2,t2) -> PbpThenCont (tl1@tl2,t2)
-	  | PbpThens (tl2,tl3) -> PbpThens (tl1@tl2,tl3)
-	  | PbpAtom _ -> x)
-    | PbpAtom t as x -> x;;
-*)
 
 (* This optimization function takes care of compacting successive Intro commands
    together. *)
-(*
-let rec optim2 =
-    function
-	Node(a,"TACTICLIST",b) ->
-         let get_ids = 
-           List.map (function Node(_,"IDENTIFIER", [Nvar(_,s)])->s
-             | Node(_,s,_) -> (failwith "unexpected node " ^ s)
-             |  _ -> failwith "get_ids expected an identifier") in
-         let put_ids ids =
-           Node(zz,"Intros",
-               	[Node(zz,"INTROPATTERN",
-		      [Node(zz,"LISTPATTERN", 
-			    List.map 
-			      (function s -> Node(zz,"IDENTIFIER",[Nvar(zz,s)]))
-			      ids)])]) in
-         let rec group_intros names = function
-             [] -> (match names with
-               [] -> []
-	     | l -> [put_ids l])
-           | Node(_,"Intros", 
-		  [Node(_,"INTROPATTERN",[Node(_,"LISTPATTERN", ids)])])::others ->
-		    group_intros (names@(get_ids ids)) others
-           | [Node(a,"TACLIST",b')] ->
-	       [Node(a,"TACLIST", List.map optim2 b')]
-           | t1::others -> 
-	       (match names with
-		 [] -> t1::(group_intros [] others)
-	       | l -> (put_ids l)::t1::(group_intros [] others)) in
-	 Node(a,"TACTICLIST",group_intros [] b)
-   | t -> t;;
-*)
-(*
-let rec optim2 = function
-  | TacThens (t,tl) -> TacThens (optim2 t, List.map optim2 tl)
-  | t ->
-      let get_ids = 
-	List.map (function IntroIdentifier _ as x -> x
-	  |  _ -> failwith "get_ids expected an identifier") in
-      let rec group_intros names = function
-	  [] -> (match names with
-              [] -> []
-	    | l -> [TacIntroPattern l])
-	| (TacIntroPattern ids)::others ->
-	    group_intros (names@(get_ids ids)) others
-	| t1::others -> 
-	    (match names with
-		[] -> t1::(group_intros [] others)
-	      | l -> (TacIntroPattern l)::t1::(group_intros [] others)) in
-      make_then (group_intros [] (flatten_sequence t))
-*)
 
 let rec group_intros names = function
     [] -> (match names with
@@ -819,37 +561,7 @@ let rec optim2 = function
   | PbpThens (tl1,tl2) -> PbpThens (group_intros [] tl1, List.map optim2 tl2)
   | PbpThen tl -> PbpThen (group_intros [] tl)
 
-(*
-let rec merge_ast_in_command com1 com2 =
-    let args1 =
-     (match com1 with
-	Node(_, "APPLIST", args) -> args
-     | _ -> failwith "unexpected com1 in merge_ast_in_command") in
-    let args2 =
-     (match com2 with
-        Node(_, "APPLIST", hyp::args) -> args
-     | _ -> failwith "unexpected com2 in merge_ast_in_command") in
-      Node(zz, "COMMAND", [Node(zz, "APPLIST", args1@args2)]);;
-*)
-(*
-let cleanup_clears empty_allowed names str_list other =
-  let rec clean_aux = function
-      [] -> []
-    | (Nvar(_,x) as fst_one)::tail ->
-      if List.mem x str_list then
-         clean_aux tail
-      else
-         fst_one::(clean_aux tail)
-    | _ -> failwith "unexpected argument in clean_aux" in
-  match clean_aux names with
-    [] -> (match other with 
-            [] -> 
-	      if empty_allowed then
-		[]
-	      else [Node(zz,"Idtac",[])]
-          | _ -> other)
-  | l -> Node(zz, "TRY", [Node(zz, "Clear", [Node(zz,"CLAUSE", l)])])::other;;
-*)
+
 let rec cleanup_clears str_list = function
     [] -> []
   | x::tail ->
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 1a6bfc4ca..3e7cfd82a 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -590,7 +590,7 @@ and fFORMULA = function
    fNODE "cofixc" 2
 | CT_elimc(x1, x2, x3, x4) ->
    fCASE x1;
-   fFORMULA x2;
+   fFORMULA_OPT x2;
    fFORMULA x3;
    fFORMULA_LIST x4;
    fNODE "elimc" 4
@@ -605,6 +605,12 @@ and fFORMULA = function
    fFORMULA x3;
    fFORMULA x4;
    fNODE "if" 4
+| CT_inductive_let(x1, x2, x3, x4) ->
+   fFORMULA_OPT x1;
+   fID_OPT_NE_LIST x2;
+   fFORMULA x3;
+   fFORMULA x4;
+   fNODE "inductive_let" 4
 | CT_int_encapsulator x -> fATOM "int_encapsulator";
    (f_atom_string x);
    print_string "\n"| CT_lambdac(x1, x2) ->
@@ -1257,8 +1263,8 @@ and fTACTIC_COM = function
    fNODE "superauto" 4
 | CT_symmetry -> fNODE "symmetry" 0
 | CT_tac_double(x1, x2) ->
-   fINT x1;
-   fINT x2;
+   fID_OR_INT x1;
+   fID_OR_INT x2;
    fNODE "tac_double" 2
 | CT_tacsolve(x,l) ->
    fTACTIC_COM x;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3ac46fa7d..2e791e8d5 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -5,7 +5,6 @@ open Char;;
 open Util;;
 open Ast;;
 open Names;;
-open Ctast;;
 open Ascent;;
 open Genarg;;
 open Rawterm;;
@@ -18,12 +17,6 @@ open Libnames;;
 
 let in_coq_ref = ref false;;
 
-let xlate_mut_stuff = ref ((fun _ -> 
-          Nvar((0,0), "function xlate_mut_stuff should not be used here")):
-              Ctast.t -> Ctast.t);;
-
-let set_xlate_mut_stuff v = xlate_mut_stuff := v;;
-
 let declare_in_coq () = in_coq_ref:=true;;
 
 let in_coq () = !in_coq_ref;;
@@ -168,18 +161,6 @@ let coerce_VARG_to_ID =
      x
     | _ -> xlate_error "coerce_VARG_to_ID";;
 
-let xlate_id =
- function
-    | Nvar (_, id) ->
-     (match id with
-     | "_" -> xlate_error "xlate_id: '_' is ident option"
-     | s -> CT_ident s)
-    | Id (_, id) ->
-     (match id with
-     | "_" -> xlate_error "xlate_id: '_' is ident option"
-     | s -> CT_ident s)
-    | _ -> xlate_error "xlate_id: not an identifier";;
-
 let xlate_id_unit = function
     None -> CT_unit
   | Some x -> CT_coerce_ID_to_ID_UNIT (xlate_ident x);;
@@ -189,11 +170,6 @@ let xlate_ident_opt =
     | None -> ctv_ID_OPT_NONE
     | Some id -> ctf_ID_OPT_SOME (xlate_ident id)
 
-let xlate_int =
- function
-    | Num (_, n) -> CT_int n
-    | _ -> xlate_error "xlate_int: not an int";;
-
 let xlate_id_to_id_or_int_opt s =
    CT_coerce_ID_OPT_to_ID_OR_INT_OPT
      (CT_coerce_ID_to_ID_OPT (CT_ident (string_of_id s)));;
@@ -210,11 +186,6 @@ let xlate_int_opt = function
   | Some n -> CT_coerce_INT_to_INT_OPT (CT_int n)
   | None ->  CT_coerce_NONE_to_INT_OPT CT_none
 
-let xlate_string =
- function
-    | Str (_, s) -> CT_string s
-    | _ -> xlate_error "xlate_string: not a string";;
-
 let tac_qualid_to_ct_ID ref = 
   CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
 
@@ -240,16 +211,6 @@ let xlate_class = function
   | SortClass -> CT_ident "SORTCLASS"
   | RefClass qid -> loc_qualid_to_ct_ID qid
 
-let split_params =
- let rec sprec acc =
-  function
-     | (Id _ as p) :: l -> sprec (p::acc) l
-     | (Str _ as p) :: l -> sprec (p::acc) l
-     | (Num _ as p) :: l -> sprec (p::acc) l
-     | (Path _ as p) :: l -> sprec (p::acc) l
-     | l -> List.rev acc, l in
- sprec [];;
-
 let id_to_pattern_var ctid =
  match ctid with
  | CT_ident "_" -> 
@@ -261,14 +222,6 @@ let id_to_pattern_var ctid =
 
 exception Not_natural;;
 
-let rec nat_to_number =
- function
-    | Node (_, "APPLIST", ((Nvar (_, "S")) :: (v :: []) as v0)) ->
-     1 + nat_to_number v
-    | Nvar (_, "O") -> 0
-    | _ -> raise Not_natural;;
-
-
 let xlate_sort =
   function
     | RProp Term.Pos -> CT_sortc "Set"
@@ -291,8 +244,9 @@ let xlate_reference = function
 let rec xlate_match_pattern =
  function
    | CPatAtom(_, Some s) -> id_to_pattern_var (xlate_reference  s)
-   |CPatAtom(_, None) -> id_to_pattern_var (CT_ident "_")
-   |  CPatCstr (_, f1 , (arg1 :: args)) ->
+   | CPatAtom(_, None) -> id_to_pattern_var (CT_ident "_")
+   | CPatCstr(_, f, []) -> id_to_pattern_var (xlate_reference f)
+   | CPatCstr (_, f1 , (arg1 :: args)) ->
      CT_pattern_app
       (id_to_pattern_var (xlate_reference  f1),
       CT_match_pattern_ne_list
@@ -301,7 +255,9 @@ let rec xlate_match_pattern =
     | CPatAlias  (_,  pattern, id) ->
      CT_pattern_as
       (xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
-    | _ -> xlate_error "Unexpected data while translating a pattern";;
+    | CPatDelimiters(_, _, _) -> xlate_error "CPatDelimitors"
+    | CPatNumeral(_,_) -> xlate_error "CPatNumeral";;
+
 
 
 
@@ -340,6 +296,8 @@ and
 and 
   xlate_binder_list = function
   l -> CT_binder_list( List.map xlate_binder_l l)
+and  cvt_fixpoint_binders bl =
+  CT_binder_list(List.map xlate_binder bl)
 and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 
      CRef r -> varc (xlate_reference r)
@@ -361,19 +319,49 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> 
 		   CT_if(xlate_formula_opt po,
                    xlate_formula c,xlate_formula b1,xlate_formula b2)		
-
+   | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
+       CT_inductive_let(xlate_formula_opt po,
+	       xlate_id_opt_ne_list l,
+	       xlate_formula c, xlate_formula b) 
+   | COrderedCase (_,c,v,e,l) -> 
+       let case_string = match c with
+	   Term.MatchStyle -> "Match"
+	 | _ -> "Case" in
+	 CT_elimc(CT_case "Case", xlate_formula_opt v, xlate_formula e,
+		  CT_formula_list(List.map xlate_formula l))
    | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
    | 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 
-   | COrderedCase (_,_,_,_,_) -> xlate_error "TODO:COrderedCase"
    | CDynamic (_, _) -> xlate_error "TODO:CDynamic"
    | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula  num)
-   | CCast (_, _, _) -> xlate_error "TODO:CCast"
-   | CMeta (_, _) -> xlate_error "TODO:CMeta"
-   | CCoFix (_, _, _) -> xlate_error "TODO:CCoFix"
-   | CFix (_, _, _) -> xlate_error "TODO:CFix"
-
+   | CCast (_, e, t) -> 
+       CT_coerce_TYPED_FORMULA_to_FORMULA
+	 (CT_typed_formula(xlate_formula e, xlate_formula t))
+   | CMeta (_, i) -> CT_coerce_ID_to_FORMULA(CT_metac (CT_int i))
+   | CCoFix (_, (_, id), lm::lmi) -> 
+     let strip_mutcorec (fid, arf, ardef) =
+	CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in
+        CT_cofixc(xlate_ident id,
+	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
+   | CFix (_, (_, id), lm::lmi) ->       
+     let strip_mutrec (fid, n, arf, ardef) =
+        let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
+        let arf = xlate_formula arf in
+        let ardef = xlate_formula ardef in
+	match cvt_fixpoint_binders bl with
+	  | CT_binder_list (b :: bl) ->
+	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
+                arf, ardef)
+          | _ -> xlate_error "mutual recursive" in
+       CT_fixc (xlate_ident id, 
+         	CT_fix_binder_list
+		  (CT_coerce_FIX_REC_to_FIX_BINDER 
+		     (strip_mutrec lm), List.map 
+		       (fun x-> CT_coerce_FIX_REC_to_FIX_BINDER (strip_mutrec x))
+		       lmi)) 
+   | CCoFix _ -> assert false
+   | CFix _ -> assert false
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
   | (a, i) -> CT_bang(xlate_int_opt i, xlate_formula a)
@@ -519,17 +507,6 @@ let is_tactic_special_case = function
     "AutoRewrite" -> true
   | _ -> false;;
 
-let tactic_special_case cont_function cvt_arg = function
-    "AutoRewrite", (tac::v::bl) ->
-      CT_autorewrite
-	(CT_id_ne_list(xlate_id v, List.map xlate_id bl),
-	   CT_coerce_TACTIC_COM_to_TACTIC_OPT(cont_function tac))
-  | "AutoRewrite", (v::bl) ->
-      CT_autorewrite
-	(CT_id_ne_list(xlate_id v, List.map xlate_id bl),
-	 CT_coerce_NONE_to_TACTIC_OPT CT_none)
-  | _ -> assert false;;
-	      
 let xlate_context_pattern = function
   | Term v -> 
       CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v)
@@ -703,9 +680,8 @@ and xlate_tac =
     | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
     | TacChange (_, f, b) -> xlate_error "TODO: Change subterms"
     | TacExtend (_,"Contradiction",[]) -> CT_contradiction
-    | TacDoubleInduction (AnonHyp n1, AnonHyp n2) ->
-	CT_tac_double (CT_int n1, CT_int n2)
-    | TacDoubleInduction _ -> xlate_error "TODO: Double Induction id1 id2"
+    | TacDoubleInduction (n1, n2) ->
+	CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2)
     | TacExtend (_,"Discriminate", [idopt]) ->
      CT_discriminate_eq
          (xlate_quantified_hypothesis_opt
@@ -1146,30 +1122,6 @@ let build_record_field_list l =
       xlate_error "TODO: manifest fields in Record" in
  CT_recconstr_list (List.map build_record_field l);;
 
-let xlate_ast =
- let rec xlate_ast_aux =
-  function
-     | Node (_, s, tl) ->
-      CT_astnode (CT_ident s, CT_ast_list (List.map xlate_ast_aux tl))
-     | Nvar (_, s) ->
-      CT_coerce_ID_OR_STRING_to_AST
-       (CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
-     | Slam (_, (Some s), t) ->
-      CT_astslam (CT_coerce_ID_to_ID_OPT (CT_ident s), xlate_ast_aux t)
-     | Slam (_, None, t) -> CT_astslam (ctv_ID_OPT_NONE, xlate_ast_aux t)
-     | Num (_, i) -> failwith "Numbers not treated in xlate_ast"
-     | Id (_, s) ->
-      CT_coerce_ID_OR_STRING_to_AST
-       (CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
-     | Str (_, s) ->
-      CT_coerce_ID_OR_STRING_to_AST
-       (CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
-     | Dynamic(_,_) -> failwith "Dynamics not treated in xlate_ast"
-     | Path (_, sl) ->
-      CT_astpath
-       (CT_id_list (List.map (function s -> CT_ident s) sl)) in
- xlate_ast_aux;;
-
 let get_require_flags impexp spec =
  let ct_impexp =
   match impexp with
@@ -1198,8 +1150,7 @@ let cvt_vernac_binder = function
 let cvt_vernac_binders args =
   CT_binder_list(List.map cvt_vernac_binder args)
 
-let cvt_fixpoint_binders bl =
-  CT_binder_list(List.map xlate_binder bl)
+
 
 let xlate_comment = function
     CommentConstr c -> CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula c)
diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli
index 6109816b5..bedb4ac82 100644
--- a/contrib/interface/xlate.mli
+++ b/contrib/interface/xlate.mli
@@ -3,10 +3,7 @@ open Ascent;;
 val xlate_vernac : Vernacexpr.vernac_expr -> ct_COMMAND;;
 val xlate_tactic : Tacexpr.raw_tactic_expr -> ct_TACTIC_COM;;
 val xlate_formula : Topconstr.constr_expr -> ct_FORMULA;;
-val xlate_int : Ctast.t -> ct_INT;;
-val xlate_string : Ctast.t -> ct_STRING;;
 val xlate_ident : Names.identifier -> ct_ID;;
 val xlate_vernac_list : Vernacexpr.vernac_expr -> ct_COMMAND_LIST;;
 
-val set_xlate_mut_stuff : (Ctast.t -> Ctast.t) -> unit;;
 val declare_in_coq : (unit -> unit);;