Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

17 files changed, 1869 insertions, 1103 deletions

diff --git a/contrib/interface/COPYRIGHT b/contrib/interface/COPYRIGHT
index 2fb11c6b..23aeb6bb 100644
--- a/contrib/interface/COPYRIGHT
+++ b/contrib/interface/COPYRIGHT
@@ -1,8 +1,9 @@
 (*****************************************************************************)
 (*                                                                           *)
-(*            Coq support for the Pcoq Graphical Interface of Coq            *)
+(*      Coq support for the Pcoq and tmEgg Graphical Interfaces of Coq       *)
 (*                                                                           *)
 (*        Copyright (C) 1999-2004 INRIA Sophia-Antipolis (Lemme team)        *)
+(*        Copyright (C) 2006,2007 Lionel Elie Mamane                         *)
 (*                                                                           *)
 (*****************************************************************************)
 
@@ -10,6 +11,9 @@ The current directory contrib/interface implements Coq support for the
 Pcoq Graphical Interface of Coq. It has been developed by Yves Bertot
 with contributions from Loïc Pottier and Laurence Rideau.
 
+Modifications by Lionel Elie Mamane <lionel@mamane.lu> for
+generalising the protocol to suit other Coq interfaces.
+
 The Pcoq Graphical Interface (see http://www-sop.inria.fr/lemme/pcoq)
 is developed by the Lemme team at INRIA Sophia-Antipolis (see
 http://www-sop.inria.fr/lemme)
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index ef1d095e..32338523 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -113,7 +113,6 @@ and ct_COMMAND =
   | 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
   | CT_print
   | CT_print_about of ct_ID
@@ -189,13 +188,13 @@ and ct_COMMAND =
   | CT_show_script
   | CT_show_tree
   | CT_solve of ct_INT * ct_TACTIC_COM * ct_DOTDOT_OPT
+  | CT_strategy of ct_LEVEL_LIST
   | CT_suspend
   | CT_syntax_macro of ct_ID * ct_FORMULA * ct_INT_OPT
   | CT_tactic_definition of ct_TAC_DEF_NE_LIST
   | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT
   | CT_time of ct_COMMAND
-  | CT_transparent of ct_ID_NE_LIST
   | CT_undo of ct_INT_OPT
   | CT_unfocus
   | CT_unset_option of ct_TABLE
@@ -204,6 +203,12 @@ and ct_COMMAND =
   | CT_user_vernac of ct_ID * ct_VARG_LIST
   | CT_variable of ct_VAR * ct_BINDER_NE_LIST
   | CT_write_module of ct_ID * ct_STRING_OPT
+and ct_LEVEL_LIST =
+    CT_level_list of (ct_LEVEL * ct_ID_LIST) list
+and ct_LEVEL =
+    CT_Opaque
+  | CT_Level of ct_INT
+  | CT_Expand
 and ct_COMMAND_LIST =
     CT_command_list of ct_COMMAND * ct_COMMAND list
 and ct_COMMENT =
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index dc27cf98..6ec0fac4 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -151,7 +151,7 @@ let pp_string x =
 let unify_e_resolve  (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false clenv' gls in
-  vernac_e_resolve_constr c gls
+    Hiddentac.h_simplest_eapply c gls
 
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl = 
@@ -161,33 +161,36 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
-	     (Hint_db.add_list hintl local_db) g'))) ::
+	     (add_hint_list hintl local_db) g'))) ::
     (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
 
 and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
+  let flags = Auto.auto_unif_flags in
   let hintl =
     if occur_existential concl then 
-      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
+      list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x))
+	(Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
+      list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) 
+	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in 
   let tac_of_hint = 
-    fun ({pri=b; pat = p; code=t} as _patac) -> 
+    fun (st, ({pri=b; pat = p; code=t} as _patac)) -> 
       (b, 
        let tac =
 	 match t with
-	   | Res_pf (term,cl) -> unify_resolve (term,cl)
+	   | Res_pf (term,cl) -> unify_resolve st (term,cl)
 	   | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
 	   | Give_exact (c) -> e_give_exact_constr c
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve (term,cl)) 
 		 (e_trivial_fail_db db_list local_db)
-	   | Unfold_nth c -> unfold_in_concl [[],c]
+	   | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	   | Extern tacast -> Auto.conclPattern concl 
-	       (out_some p) tacast
+	       (Option.get p) tacast
        in 
        (free_try tac,fmt_autotactic t))
        (*i
@@ -227,8 +230,8 @@ module MySearchProblem = struct
     depth : int; (*r depth of search before failing *)
     tacres : goal list sigma * validation;
     last_tactic : std_ppcmds;
-    dblist : Auto.Hint_db.t list;
-    localdb :  Auto.Hint_db.t list }
+    dblist : Auto.hint_db list;
+    localdb :  Auto.hint_db list }
 		 
   let success s = (sig_it (fst s.tacres)) = []
 
@@ -242,9 +245,6 @@ module MySearchProblem = struct
 	with e when Logic.catchable_exception e ->
 	  filter_tactics (glls,v) tacl
 
-  let rec list_addn n x l = 
-    if n = 0 then l else x :: (list_addn (pred n) x l)
-
   (* Ordering of states is lexicographic on depth (greatest first) then
      number of remaining goals. *)
   let compare s s' =
@@ -279,7 +279,7 @@ module MySearchProblem = struct
 	     let hintl = 
 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 	     in
-             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
+             let ldb = add_hint_list hintl (List.hd s.localdb) in
 	     { depth = s.depth; tacres = res; 
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb })
@@ -337,7 +337,7 @@ let e_breadth_search debug n db_list local_db gl =
   with Not_found -> error "EAuto: breadth first search failed"
 
 let e_search_auto debug (n,p) db_list gl = 
-  let local_db = make_local_hint_db [] gl in 
+  let local_db = make_local_hint_db true [] gl in 
   if n = 0 then 
     e_depth_search debug p db_list local_db gl
   else 
@@ -357,7 +357,7 @@ let full_eauto debug n gl =
   let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
-  let _local_db = make_local_hint_db [] gl in
+  let _local_db = make_local_hint_db true [] gl in
   tclTRY (e_search_auto debug n db_list) gl
 
 let my_full_eauto n gl = full_eauto false (n,0) gl
@@ -375,7 +375,7 @@ let rec trivial_fail_db db_list local_db gl =
     tclTHEN intro 
       (fun g'->
 	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-	 in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
+	 in trivial_fail_db db_list (add_hint_list hintl local_db) g')
   in
   tclFIRST 
     (assumption::intro_tac::
@@ -383,27 +383,29 @@ let rec trivial_fail_db db_list local_db gl =
 	(trivial_resolve db_list local_db (pf_concl gl)))) gl
 
 and my_find_search db_list local_db hdc concl =
+  let flags = Auto.auto_unif_flags in
   let tacl = 
     if occur_existential concl then 
-      list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list)
+      list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) 
+	(Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db)
-      	(local_db::db_list)
+      list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
+	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in
   List.map 
-    (fun ({pri=b; pat=p; code=t} as _patac) -> 
+    (fun (st, {pri=b; pat=p; code=t} as _patac) -> 
        (b,
 	match t with
-	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
+	  | Res_pf (term,cl)  -> unify_resolve st (term,cl)
 	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
 	  | Give_exact c  -> exact_check c
 	  | Res_pf_THEN_trivial_fail (term,cl) -> 
 	      tclTHEN 
-		(unify_resolve (term,cl)) 
+		(unify_resolve st (term,cl)) 
 		(trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> unfold_in_concl [[],c]
+	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	  | Extern tacast -> 
-	      conclPattern concl (out_some p) tacast))
+	      conclPattern concl (Option.get p) tacast))
     tacl
 
 and trivial_resolve db_list local_db cl = 
@@ -470,11 +472,12 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   try 
 	     [make_apply_entry (pf_env g') (project g')
 		(true,false) 
-		(mkVar hid,body_of_type htyp)]
+		None
+		(mkVar hid,htyp)]
 	   with Failure _ -> [] 
 	 in
          (free_try
-	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
+	  (search_gen decomp n db_list (add_hint_list hintl local_db) [d])
 	  g'))
   in
   let rec_tacs = 
@@ -497,7 +500,7 @@ let full_auto n gl =
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db [] gl) hyps) gl
+  tclTRY (search n db_list (make_local_hint_db false [] gl) hyps) gl
   
 let default_full_auto gl = full_auto !default_search_depth gl
 (************************************************************************)
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 730e055b..a4dc0eac 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -1,11 +1,28 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
+(*
+ * This file has been modified by Lionel Elie Mamane <lionel@mamane.lu>
+ * to implement the following features
+ * - Terms (optionally) as pretty-printed string and not trees
+ * - (Optionally) give most commands their usual Coq semantics
+ * - Add the backtracking information to the status message.
+ * in the following time period
+ * - May-November 2006
+ * and
+ * - Make use of new Command.save_hook to generate dependencies at
+ *   save-time.
+ * in
+ *  - June 2007
+ *)
+
 (*Toplevel loop for the communication between Coq and Centaur *)
 open Names;;
 open Nameops;;
 open Util;;
 open Term;;
 open Pp;;
+open Ppconstr;;
+open Prettyp;;
 open Libnames;;
 open Libobject;;
 open Library;;
@@ -43,6 +60,7 @@ open Showproof;;
 open Showproof_ct;;
 open Tacexpr;;
 open Vernacexpr;;
+open Printer;;
 
 let pcoq_started = ref None;;
 
@@ -51,6 +69,11 @@ let if_pcoq f a =
 
 let text_proof_flag = ref "en";;
 
+let pcoq_history = ref true;;
+
+let assert_pcoq_history f a =
+  if !pcoq_history then f a else error "Pcoq-style history tracking deactivated";;
+
 let current_proof_name () = 
   try 
     string_of_id (get_current_proof_name ())
@@ -85,10 +108,33 @@ let kill_proof_node index =
  History.border_length (current_proof_name());;
 
 
+type vtp_tree =
+  | P_rl of ct_RULE_LIST
+  | P_r of ct_RULE
+  | P_s_int of ct_SIGNED_INT_LIST
+  | P_pl of ct_PREMISES_LIST
+  | P_cl of ct_COMMAND_LIST
+  | P_t of ct_TACTIC_COM
+  | P_text of ct_TEXT
+  | P_ids of ct_ID_LIST;;
+
+let print_tree t = 
+  (match t with
+  | P_rl x -> fRULE_LIST x
+  | P_r x -> fRULE x
+  | P_s_int x -> fSIGNED_INT_LIST x
+  | P_pl x -> fPREMISES_LIST x
+  | P_cl x -> fCOMMAND_LIST x
+  | P_t x -> fTACTIC_COM x
+  | P_text x -> fTEXT x
+  | P_ids x -> fID_LIST x)
+  ++ (str "e\nblabla\n");;
+
+
 (*Message functions, the text of these messages is recognized by the protocols *)
 (*of CtCoq                                                                     *)
 let ctf_header message_name request_id =
- fnl () ++ str "message" ++ fnl() ++ str message_name ++ fnl() ++
+ str "message" ++ fnl() ++ str message_name ++ fnl() ++
  int request_id ++ fnl();;
 
 let ctf_acknowledge_command request_id command_count opt_exn =
@@ -97,14 +143,20 @@ let ctf_acknowledge_command request_id command_count opt_exn =
       let g_count =
         List.length 
           (fst (frontier (proof_of_pftreestate (get_pftreestate ())))) in
-        g_count, (min g_count !current_goal_index)
+        g_count, !current_goal_index
     else
-      (0, 0) in
+      (0, 0)
+  and statnum = Lib.current_command_label ()
+  and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0
+  and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in
    (ctf_header "acknowledge" request_id ++
     int command_count ++ fnl() ++
     int goal_count ++ fnl () ++
     int goal_index ++ fnl () ++
     str (current_proof_name()) ++ fnl() ++
+    int statnum ++ fnl() ++
+    print_tree (P_ids pending) ++
+    int dpth ++ fnl() ++
     (match opt_exn with
       Some e -> Cerrors.explain_exn e
     | None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
@@ -126,6 +178,8 @@ let ctf_PathGoalMessage () =
 
 let ctf_GoalReqIdMessage = ctf_header "single_goal_state";;
 
+let ctf_GoalsReqIdMessage = ctf_header "goals_state";;
+
 let ctf_NewStateMessage = ctf_header "fresh_state";;
 
 let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++
@@ -153,39 +207,16 @@ let ctf_ResetIdentMessage request_id s =
  ctf_header "reset_ident" request_id ++ str s ++ fnl () ++
   str  "E-n-d---M-e-s-s-a-g-e" ++ fnl();;
 
-type vtp_tree =
-  | P_rl of ct_RULE_LIST
-  | P_r of ct_RULE
-  | P_s_int of ct_SIGNED_INT_LIST
-  | P_pl of ct_PREMISES_LIST
-  | P_cl of ct_COMMAND_LIST
-  | P_t of ct_TACTIC_COM
-  | P_text of ct_TEXT
-  | P_ids of ct_ID_LIST;;
-
-let print_tree t = 
-  (match t with
-  | P_rl x -> fRULE_LIST x
-  | P_r x -> fRULE x
-  | P_s_int x -> fSIGNED_INT_LIST x
-  | P_pl x -> fPREMISES_LIST x
-  | P_cl x -> fCOMMAND_LIST x
-  | P_t x -> fTACTIC_COM x
-  | P_text x -> fTEXT x
-  | P_ids x -> fID_LIST x);
-  print_string "e\nblabla\n";;
-
-
 
 let break_happened = ref false;;
 
 let output_results stream vtp_tree =
     let _ = Sys.signal Sys.sigint
        (Sys.Signal_handle(fun i -> (break_happened := true;()))) in
-    msg stream;
-    match vtp_tree with
-      Some t -> print_tree t
-    | None -> ();;
+    msg (stream ++
+    (match vtp_tree with
+       Some t -> print_tree t
+     | None -> mt()));;
 
 let output_results_nl stream =
     let _ = Sys.signal Sys.sigint
@@ -221,20 +252,18 @@ let print_past_goal index =
 
 let show_nth n =
   try
-    let pf = proof_of_pftreestate (get_pftreestate()) in
-    if (!text_proof_flag<>"off") then
-       (if n=0
-	   then output_results (ctf_TextMessage !global_request_id)
-                               (Some (P_text (show_proof !text_proof_flag [])))
-           else			       
-	   let path = History.get_nth_open_path (current_proof_name()) n in
-	   output_results (ctf_TextMessage !global_request_id)
-                          (Some (P_text (show_proof !text_proof_flag path))))
-    else
-      output_results (ctf_GoalReqIdMessage !global_request_id)
-      (let goal = List.nth (fst (frontier pf))
-                   (n - 1) in
-      (Some (P_r (translate_goal goal))))
+    output_results (ctf_GoalReqIdMessage !global_request_id
+		    ++ pr_nth_open_subgoal n)
+      None
+  with
+  | Invalid_argument s -> 
+       error "No focused proof (No proof-editing in progress)";;
+
+let show_subgoals () =
+  try
+    output_results (ctf_GoalReqIdMessage !global_request_id
+		    ++ pr_open_subgoals ())
+      None
   with
   | Invalid_argument s -> 
        error "No focused proof (No proof-editing in progress)";;
@@ -275,39 +304,24 @@ let ctf_EmptyGoalMessage id =
   fnl () ++ str "Empty Goal is a no-op.  Fun oh fun." ++ fnl ();;
 
 
-let print_check judg =
- let {uj_val=value; uj_type=typ} = judg in
- let value_ct_ast = 
-     (try translate_constr false (Global.env()) value 
-      with UserError(f,str) ->
-           raise(UserError(f,Printer.pr_lconstr value ++
-			      fnl () ++ str ))) in
- let type_ct_ast =
-     (try translate_constr false (Global.env()) typ
-      with UserError(f,str) ->
-           raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in
- ((ctf_SearchResults !global_request_id),
- (Some  (P_pl
-  (CT_premises_list
-  [CT_coerce_TYPED_FORMULA_to_PREMISE
-    (CT_typed_formula(value_ct_ast,type_ct_ast)
-    )]))));;
-
-let ct_print_eval ast red_fun env judg =
-((if refining() then traverse_to []);
-let {uj_val=value; uj_type=typ} = judg in
-let nvalue = red_fun value
-(* // Attention , ici il faut peut être utiliser des environnemenst locaux *)
-and ntyp = nf_betaiota typ in
-(ctf_SearchResults !global_request_id,
- Some (P_pl
-  (CT_premises_list
-  [CT_eval_result
-    (xlate_formula ast,
-    translate_constr false env nvalue,
-    translate_constr false env ntyp)]))));;
-
-
+let print_check env judg =
+ ((ctf_SearchResults !global_request_id) ++
+    print_judgment env judg,
+  None);;
+
+let ct_print_eval red_fun env evmap ast judg =
+  (if refining() then traverse_to []);
+  let {uj_val=value; uj_type=typ} = judg in
+  let nvalue = (red_fun env evmap) value
+    (* // Attention , ici il faut peut être utiliser des environnemenst locaux *)
+  and ntyp = nf_betaiota typ in
+    print_tree
+      (P_pl
+	 (CT_premises_list
+	    [CT_eval_result
+	       (xlate_formula ast,
+		translate_constr false env nvalue,
+		translate_constr false env ntyp)]));;
 
 let pbp_tac_pcoq =
     pbp_tac (function (x:raw_tactic_expr) -> 
@@ -330,6 +344,7 @@ let dad_tac_pcoq =
 </cpa> *)
 
 let search_output_results () =
+  (* LEM: See comments for pcoq_search *)
   output_results
        (ctf_SearchResults !global_request_id)
        (Some (P_pl (CT_premises_list
@@ -393,7 +408,7 @@ let inspect n =
              	oname, Lib.Leaf lobj ->
 		  (match oname, object_tag lobj with
                        (sp,_), "VARIABLE" ->
-			 let (_, _, v) = get_variable (basename sp) in
+			 let (_, _, v) = Global.lookup_named (basename sp) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
 		     | (sp,kn), "CONSTANT" ->
 			 let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in
@@ -491,19 +506,19 @@ VERNAC COMMAND EXTEND OutputGoal
 END
 
 VERNAC COMMAND EXTEND OutputGoal
-  [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ simulate_solve n tac ]
+  [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ assert_pcoq_history (simulate_solve n) tac ]
 END
 
 VERNAC COMMAND EXTEND KillProofAfter
-| [ "Kill" "Proof" "after"  natural(n) ] -> [ kill_node_verbose n ]
+| [ "Kill" "Proof" "after"  natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ]
 END
 
 VERNAC COMMAND EXTEND KillProofAt
-| [ "Kill" "Proof" "at"  natural(n) ] -> [ kill_node_verbose n ]
+| [ "Kill" "Proof" "at"  natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ]
 END
 
 VERNAC COMMAND EXTEND KillSubProof
-  [ "Kill" "SubProof" natural(n) ] -> [ logical_kill n ]
+  [ "Kill" "SubProof" natural(n) ] -> [ assert_pcoq_history logical_kill n ]
 END
 
 VERNAC COMMAND EXTEND PcoqReset
@@ -515,18 +530,17 @@ VERNAC COMMAND EXTEND PcoqResetInitial
 END
 
 let start_proof_hook () =
-  History.start_proof (current_proof_name());
+  if !pcoq_history then History.start_proof (current_proof_name());
   current_goal_index := 1
 
 let solve_hook n =
-  let name = current_proof_name () in
-  let old_n_count = History.border_length name in
-  let pf = proof_of_pftreestate (get_pftreestate ()) in
-  let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in
-  begin
-    current_goal_index := n;
-    History.push_command name  n n_goals
-  end
+  current_goal_index := n;
+  if !pcoq_history then
+    let name = current_proof_name () in
+    let old_n_count = History.border_length name in
+    let pf = proof_of_pftreestate (get_pftreestate ()) in
+    let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in
+      History.push_command name n n_goals
 
 let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
 
@@ -535,6 +549,12 @@ let interp_search_about_item = function
   | SearchString s -> GlobSearchString s
 
 let pcoq_search s l =
+  (* LEM: I don't understand why this is done in this way (redoing the
+   *      match on s here) instead of making the code in
+   *      parsing/search.ml call the right function instead of
+   *      "plain_display". Investigates this later.
+   * TODO
+   *)
   ctv_SEARCH_LIST:=[];
   begin match s with
   | SearchAbout sl -> 
@@ -581,27 +601,25 @@ let hyp_search_pattern c l =
       (Some
 	 (P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));;
 let pcoq_print_name ref =
-  let results = xlate_vernac_list (name_to_ast ref) in
   output_results 
-    (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ())
-    (Some (P_cl results))
+    (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl () ++ print_name ref )
+    None
 
-let pcoq_print_check j =
-  let a,b = print_check j in output_results a b
+let pcoq_print_check env j =
+  let a,b = print_check env j in output_results a b
 
-let pcoq_print_eval redfun env c j =
-  let strm, vtp = ct_print_eval c redfun env j in
-  output_results strm vtp;;
+let pcoq_print_eval redfun env evmap c j =
+  output_results
+    (ctf_SearchResults !global_request_id
+     ++ Prettyp.print_eval redfun env evmap c j)
+    None;;
 
 open Vernacentries
 
 let pcoq_show_goal = function
   | Some n -> show_nth n
-  | None ->
-      if !pcoq_started = Some true (* = debug *) then
-	msg (Printer.pr_open_subgoals ())
-      else errorlabstrm "show_goal"
-	(str "Show must be followed by an integer in Centaur mode");;
+  | None -> show_subgoals ()
+;;
 
 let pcoq_hook = {
   start_proof = start_proof_hook;
@@ -614,6 +632,165 @@ let pcoq_hook = {
   show_goal = pcoq_show_goal
 }
 
+let pcoq_term_pr = {
+  pr_constr_expr   = (fun c -> str "pcoq_constr_expr\n"  ++ (default_term_pr.pr_constr_expr   c));
+  (* In future translate_constr false (Global.env())
+   * Except with right bool/env which I'll get :)
+   *)
+  pr_lconstr_expr  = (fun c -> fFORMULA (xlate_formula c) ++ str "(pcoq_lconstr_expr of " ++ (default_term_pr.pr_lconstr_expr  c) ++ str ")");
+  pr_pattern_expr  = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_pattern_expr  c));
+  pr_lpattern_expr = (fun c -> str "pcoq_constr_expr\n"  ++ (default_term_pr.pr_lpattern_expr c))
+}
+
+let start_pcoq_trees () =
+  set_term_pr pcoq_term_pr
+
+(* BEGIN functions for object_pr *)
+
+(* These functions in general mirror what name_to_ast does in a subcase,
+   and then print the corresponding object as a PCoq tree. *)
+
+let object_to_ast_template object_to_ast_list sp =
+  let l = object_to_ast_list sp in
+    VernacList (List.map (fun x -> (dummy_loc, x)) l)
+
+let pcoq_print_object_template object_to_ast_list sp =
+  let results = xlate_vernac_list (object_to_ast_template object_to_ast_list sp) in
+    print_tree (P_cl results)
+
+(* This function mirror what print_check does *)
+
+let pcoq_print_typed_value_in_env env (value, typ) =
+ let value_ct_ast = 
+     (try translate_constr false (Global.env()) value 
+      with UserError(f,str) ->
+           raise(UserError(f,Printer.pr_lconstr value ++
+			      fnl () ++ str ))) in
+ let type_ct_ast =
+     (try translate_constr false (Global.env()) typ
+      with UserError(f,str) ->
+           raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in
+   print_tree
+     (P_pl
+	(CT_premises_list
+	   [CT_coerce_TYPED_FORMULA_to_PREMISE
+	      (CT_typed_formula(value_ct_ast,type_ct_ast)
+	      )]))
+;;
+
+(* This function mirrors what show_nth does *)
+
+let pcoq_pr_subgoal n gl =
+  try
+    print_tree
+      (if (!text_proof_flag<>"off") then
+	   (* This is a horrendeous hack; it ignores the "gl" argument
+              and just takes the currently focused proof. This will bite
+	      us back one day.
+	      TODO: Fix this.
+	   *)
+	   (
+	    if not !pcoq_history then error "Text mode requires Pcoq history tracking.";
+	    if n=0
+	    then (P_text (show_proof !text_proof_flag []))
+	    else
+		let path = History.get_nth_open_path (current_proof_name()) n in
+		  (P_text (show_proof !text_proof_flag path)))
+       else
+	   (let goal = List.nth gl (n - 1) in
+	      (P_r (translate_goal goal))))
+  with
+  | Invalid_argument _
+  | Failure "nth"
+  | Not_found           -> error "No such goal";;
+
+let pcoq_pr_subgoals close_cmd evar gl =
+  (*LEM: TODO: we should check for evar emptiness or not, and do something *)
+  try
+    print_tree
+      (if (!text_proof_flag<>"off") then
+	   raise (Anomaly ("centaur.ml4:pcoq_pr_subgoals", str "Text mode show all subgoals not implemented"))
+       else
+	   (P_rl (translate_goals gl)))
+  with
+  | Invalid_argument _
+  | Failure "nth"
+  | Not_found           -> error "No such goal";;
+
+
+(*  END functions for object_pr  *)
+
+let pcoq_object_pr = {
+  print_inductive           = pcoq_print_object_template inductive_to_ast_list;
+  (* TODO: Check what that with_infos means, and adapt accordingly *)
+  print_constant_with_infos = pcoq_print_object_template constant_to_ast_list;
+  print_section_variable    = pcoq_print_object_template variable_to_ast_list;
+  print_syntactic_def       = pcoq_print_object_template (fun x -> errorlabstrm "print"
+      (str "printing of syntax definitions not implemented in PCoq syntax"));
+  (* TODO: These are placeholders only; write them *)
+  print_module              = (fun x y -> str "pcoq_print_module not implemented");
+  print_modtype             = (fun x   -> str "pcoq_print_modtype not implemented");
+  print_named_decl          = (fun x   -> str "pcoq_print_named_decl not implemented");
+  (* TODO: Find out what the first argument x (a bool) is about and react accordingly *)
+  print_leaf_entry          = (fun x -> pcoq_print_object_template leaf_entry_to_ast_list);
+  print_library_entry       = (fun x y -> Some (str "pcoq_print_library_entry not implemented"));
+  print_context             = (fun x y z -> str "pcoq_print_context not implemented");
+  print_typed_value_in_env  = pcoq_print_typed_value_in_env;
+  Prettyp.print_eval        = ct_print_eval;
+};;
+
+let pcoq_printer_pr = {
+ pr_subgoals = pcoq_pr_subgoals;
+ pr_subgoal  = pcoq_pr_subgoal;
+ pr_goal     = (fun x   -> str "pcoq_pr_goal not implemented");
+};;
+
+
+let start_pcoq_objects () =
+  set_object_pr pcoq_object_pr;
+  set_printer_pr pcoq_printer_pr
+
+let start_default_objects () =
+  set_object_pr default_object_pr;
+  set_printer_pr default_printer_pr
+
+let full_name_of_ref r =
+  (match r with
+     | VarRef _ -> str "VAR"
+     | ConstRef _ -> str "CST"
+     | IndRef _ -> str "IND"
+     | ConstructRef _ -> str "CSR")
+  ++ str " " ++ (pr_sp (Nametab.sp_of_global r))
+    (* LEM TODO: Cleanly separate path from id (see Libnames.string_of_path) *)
+
+let string_of_ref =
+  (*LEM TODO: Will I need the Var/Const/Ind/Construct info?*)
+  Depends.o Libnames.string_of_path Nametab.sp_of_global
+
+let print_depends compute_depends ptree =
+  output_results (List.fold_left (fun x y -> x ++ (full_name_of_ref y) ++ fnl())
+		    (str "This object depends on:" ++ fnl())
+		    (compute_depends ptree))
+                 None
+
+let output_depends compute_depends ptree =
+  (* Using an ident list for that is arguably stretching it, but less effort than touching the vtp types *)
+  output_results (ctf_header "depends" !global_request_id ++
+		    print_tree (P_ids (CT_id_list (List.map
+						     (fun x -> CT_ident (string_of_ref x))
+						     (compute_depends ptree)))))
+                 None
+
+let gen_start_depends_dumps print_depends print_depends' print_depends'' print_depends''' =
+  Command.set_declare_definition_hook (print_depends' (Depends.depends_of_definition_entry ~acc:[]));
+  Command.set_declare_assumption_hook (print_depends  (fun (c:types) -> Depends.depends_of_constr c []));
+  Command.set_start_hook (print_depends    (fun c -> Depends.depends_of_constr c []));
+  Command.set_save_hook  (print_depends''  (Depends.depends_of_pftreestate Depends.depends_of_pftree));
+  Refiner.set_solve_hook (print_depends''' (fun pt -> Depends.depends_of_pftree_head pt []))
+
+let start_depends_dumps () = gen_start_depends_dumps output_depends output_depends output_depends output_depends
+
+let start_depends_dumps_debug () = gen_start_depends_dumps print_depends print_depends print_depends print_depends
 
 TACTIC EXTEND pbp
 | [ "pbp" ident_opt(idopt) natural_list(nl) ] -> 
@@ -635,7 +812,6 @@ let start_pcoq_mode debug =
 (* <\cpa> 
     start_dad();
 </cpa> *)
-    declare_in_coq();
 (* The following ones are added to enable rich comments in pcoq *)
 (* TODO ...
     add_tactic "Image" (fun _ -> tclIDTAC);
@@ -649,6 +825,8 @@ let start_pcoq_mode debug =
       List.iter (fun (a,b) -> overwriting_vinterp_add a b) non_debug_changes;
 *)
     set_pcoq_hook pcoq_hook;
+    start_pcoq_objects();
+    Flags.print_emacs := false; Pp.make_pp_nonemacs(); 
   end;;
 
 
@@ -681,3 +859,23 @@ END
 VERNAC COMMAND EXTEND StartPcoqDebug
 | [ "Start" "Pcoq" "Debug" "Mode" ] -> [ start_pcoq_debug () ]
 END
+
+VERNAC COMMAND EXTEND StartPcoqTerms
+| [ "Start" "Pcoq" "Trees" ] -> [ start_pcoq_trees () ]
+END
+
+VERNAC COMMAND EXTEND StartPcoqObjects
+| [ "Start" "Pcoq" "Objects" ] -> [ start_pcoq_objects () ]
+END
+
+VERNAC COMMAND EXTEND StartDefaultObjects
+| [ "Start" "Default" "Objects" ] -> [ start_default_objects () ]
+END
+
+VERNAC COMMAND EXTEND StartDependencyDumps
+| [ "Start" "Dependency" "Dumps" ] -> [ start_depends_dumps () ]
+END
+
+VERNAC COMMAND EXTEND StopPcoqHistory
+| [ "Stop" "Pcoq" "History" ] -> [ pcoq_history := false ]
+END
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index 890bb3ce..aad3a765 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -113,7 +113,7 @@ let count_subgoals2
 let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function
     TacThens (a,l) ->
       (fun report_holder -> checked_thens report_holder a l)
-  | TacThen (a,b) ->
+  | TacThen (a,[||],b,[||]) ->
       (fun report_holder -> checked_then report_holder a b)
   | t ->
       (fun report_holder g ->
@@ -279,7 +279,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
       	| Failed n -> TacId []
       	| Tree_fail r -> reconstruct_success_tac a r
       	| Mismatch (n,p) -> a)
-  | TacThen (a,b) ->
+  | TacThen (a,[||],b,[||]) ->
       (function
 	  Report_node(true, n, l) -> tac
 	| Report_node(false, n, rl) ->
@@ -340,7 +340,7 @@ Tacinterp.add_tactic "OnThen" on_then;;
 
 let rec clean_path tac l = 
   match tac, l with
-  | TacThen (a,b), fst::tl ->
+  | TacThen (a,[||],b,[||]), fst::tl ->
       fst::(clean_path (if fst = 1 then a else b) tl)
   | TacThens (a,l), 1::tl ->
       1::(clean_path a tl)
@@ -390,7 +390,7 @@ let rec report_error
 	  | t::tl -> (report_error t the_goal the_ast returned_path (n::2::path))::
 	      (fold_num (n + 1) tl) in
 	fold_num 1 l)
-    | TacThen (a,b) ->
+    | TacThen (a,[||],b,[||]) ->
 	let the_count = ref 1 in
 	tclTHEN
 	  (fun g ->
@@ -398,7 +398,7 @@ let rec report_error
 	      report_error a the_goal the_ast returned_path (1::path) g
 	    with
 	      e ->
-		(the_ast := TacThen (!the_ast, b);
+		(the_ast := TacThen (!the_ast,[||], b,[||]);
 		 raise e))
 	  (fun g ->
 	    try
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
new file mode 100644
index 00000000..dd40c5cc
--- /dev/null
+++ b/contrib/interface/depends.ml
@@ -0,0 +1,454 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant                                  *)
+(* <O___,, *                                                            *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *      GNU Lesser General Public License Version 2.1,        *)
+(*         *      or (at your option) any later version.                *)
+(************************************************************************)
+
+(* Copyright © 2007, Lionel Elie Mamane <lionel@mamane.lu> *)
+
+(* This is distributed in the hope that it will be useful,           *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of    *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *)
+(* Lesser General Public License for more details.                   *)
+
+(* You should have received a copy of the GNU Lesser General Public    *)
+(* License along with this library; if not, write to the Free Software *)
+(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,          *)
+(* MA  02110-1301, USA                                                 *)
+
+
+(* LEM TODO: a .mli file *)
+
+open Refiner
+open Proof_type
+open Rawterm
+open Term
+open Libnames
+open Util
+open Tacexpr
+open Entries
+
+(* DBG utilities, to be removed *)
+let print_bool b = print_string (string_of_bool b)
+let string_of_ppcmds p = Pp.pp_with Format.str_formatter p; Format.flush_str_formatter()
+let acc_str f = List.fold_left (fun a b -> a ^ (f b) ^ "+") "O"
+(* End utilities, to be removed *)
+
+let explore_tree pfs =
+  print_string "explore_tree called\n";
+  print_string "pfs is a top: ";
+  (* We expect yes. *)
+  print_string (if (is_top_pftreestate pfs) then "yes" else "no");
+  print_newline();
+  let rec explain_tree (pt:proof_tree) =
+    match pt.ref with
+      | None -> "none"
+      | Some (Prim p, l) -> "<Prim (" ^ (explain_prim p) ^ ") | " ^ (acc_str explain_tree l) ^ ">"
+      | Some (Nested (t,p), l) -> "<Nested (" ^ explain_compound t ^ ", " ^ (explain_tree p) ^ ") | " ^ (acc_str explain_tree l) ^ ">"
+      | Some (Decl_proof _, _) -> "Decl_proof"
+      | Some (Daimon, _) -> "Daimon"
+  and explain_compound cr =
+    match cr with
+      | Tactic (texp, b) -> "Tactic (" ^ (string_of_ppcmds (Tactic_printer.pr_tactic texp)) ^ ", " ^ (string_of_bool b) ^ ")"
+      | Proof_instr (b, instr) -> "Proof_instr (" ^ (string_of_bool b) ^ (string_of_ppcmds (Tactic_printer.pr_proof_instr instr)) ^ ")"
+  and explain_prim = function
+    | Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
+    | Intro identifier -> "Intro"
+    | Intro_replacing identifier -> "Intro_replacing"
+    | Cut (bool, identifier, types) -> "Cut"
+    | FixRule (identifier, int, l) -> "FixRule"
+    | Cofix (identifier, l) -> "Cofix"
+    | Convert_concl (types, cast_kind) -> "Convert_concl"
+    | Convert_hyp named_declaration -> "Convert_hyp"
+    | Thin identifier_list -> "Thin"
+    | ThinBody identifier_list -> "ThinBody"
+    | Move (bool, identifier, identifier') -> "Move"
+    | Rename (identifier, identifier') -> "Rename"
+    | Change_evars -> "Change_evars"
+  in
+  let pt = proof_of_pftreestate pfs in
+    (* We expect 0 *)
+    print_string "Number of open subgoals: ";
+    print_int pt.open_subgoals;
+    print_newline();
+    print_string "First rule is a ";
+    print_string (explain_tree pt);
+    print_newline()
+
+
+let o f g x = f (g x)
+let fst_of_3 (x, _, _) = x
+let snd_of_3 (_, x, _) = x
+let trd_of_3 (_, _, x) = x
+
+(* TODO: These for now return a Libnames.global_reference, but a
+   prooftree will also depend on things like tactic declarations, etc
+   so we may need a new type for that. *)
+let rec depends_of_hole_kind hk acc = match hk with
+  | Evd.ImplicitArg (gr,_)            -> gr::acc
+  | Evd.TomatchTypeParameter (ind, _) -> (IndRef ind)::acc
+  | Evd.BinderType _
+  | Evd.QuestionMark _
+  | Evd.CasesType
+  | Evd.InternalHole
+  | Evd.GoalEvar
+  | Evd.ImpossibleCase  -> acc
+
+let depends_of_'a_cast_type depends_of_'a act acc = match act with
+  | CastConv (ck, a) -> depends_of_'a a acc
+  | CastCoerce       -> acc
+
+let depends_of_'a_bindings depends_of_'a ab acc = match ab with
+  | ImplicitBindings al  -> list_union_map depends_of_'a al acc
+  | ExplicitBindings apl -> list_union_map (fun x y -> depends_of_'a (trd_of_3 x) y) apl acc
+  | NoBindings -> acc
+
+let depends_of_'a_with_bindings depends_of_'a (a, ab) acc =
+  depends_of_'a a (depends_of_'a_bindings depends_of_'a ab acc)
+
+(* let depends_of_constr_with_bindings = depends_of_'a_with_bindings depends_of_constr *)
+(* and depends_of_open_constr_with_bindings = depends_of_'a_with_bindings depends_of_open_let *)
+
+let depends_of_'a_induction_arg depends_of_'a aia acc = match aia with
+  | ElimOnConstr a -> depends_of_'a a acc
+  | ElimOnIdent _ ->
+      (* TODO: Check that this really refers only to an hypothesis (not a section variable, etc.)
+       * It *seems* thaat section variables are seen as hypotheses, so we have a problem :-(
+
+       * Plan: Load all section variables before anything in that
+       * section and call the user's proof script "brittle" and refuse
+       * to handle if it breaks because of that
+       *)
+      acc
+  | ElimOnAnonHyp _ -> acc
+
+let depends_of_'a_or_var depends_of_'a aov acc = match aov with
+  | ArgArg a -> depends_of_'a a acc
+  | ArgVar _ -> acc
+
+let depends_of_'a_with_occurences depends_of_'a (_,a) acc =
+  depends_of_'a a acc
+
+let depends_of_'a_'b_red_expr_gen depends_of_'a reg acc = match reg with
+  (* TODO: dirty assumption that the 'b doesn't make any dependency *)
+  | Red _
+  | Hnf
+  | Cbv _
+  | Lazy _
+  | Unfold _
+  | ExtraRedExpr _
+  | CbvVm           -> acc
+  | Simpl awoo ->
+      Option.fold_right
+	(depends_of_'a_with_occurences depends_of_'a)
+	awoo
+	acc
+  | Fold al -> list_union_map depends_of_'a al acc
+  | Pattern awol ->
+      list_union_map
+	(depends_of_'a_with_occurences depends_of_'a)
+	awol
+	acc
+
+let depends_of_'a_'b_inversion_strength depends_of_'a is acc = match is with
+  (* TODO: dirty assumption that the 'b doesn't make any dependency *)
+  | NonDepInversion _       -> acc
+  | DepInversion (_, ao, _) -> Option.fold_right depends_of_'a ao acc
+  | InversionUsing (a, _)   -> depends_of_'a a acc
+
+let depends_of_'a_pexistential depends_of_'a (_, aa) acc = array_union_map depends_of_'a aa acc
+
+let depends_of_named_vals nvs acc =
+  (* TODO: I'm stopping here because I have noooo idea what to do with values... *)
+  acc
+
+let depends_of_inductive ind acc = (IndRef ind)::acc
+
+let rec depends_of_constr c acc = match kind_of_term c with
+  | Rel       _                -> acc
+  | Var       id               -> (VarRef id)::acc
+  | Meta      _                -> acc
+  | Evar      ev               -> depends_of_'a_pexistential depends_of_constr ev acc
+  | Sort      _                -> acc
+  | Cast      (c, _, t)        -> depends_of_constr c (depends_of_constr t acc)
+  | Prod      (_, t, t')       -> depends_of_constr t (depends_of_constr t' acc)
+  | Lambda    (_, t, c)        -> depends_of_constr t (depends_of_constr c acc)
+  | LetIn     (_, c, t, c')    -> depends_of_constr c (depends_of_constr t (depends_of_constr c' acc))
+  | App       (c, ca)          -> depends_of_constr c (array_union_map depends_of_constr ca acc)
+  | Const     cnst             -> (ConstRef cnst)::acc
+  | Ind       ind              -> (IndRef ind)::acc
+  | Construct cons             -> (ConstructRef cons)::acc
+  | Case      (_, c, c', ca)   -> depends_of_constr c (depends_of_constr c' (array_union_map depends_of_constr ca acc))
+  | Fix       (_, (_, ta, ca))
+  | CoFix     (_, (_, ta, ca)) -> array_union_map depends_of_constr ca (array_union_map depends_of_constr ta acc)
+and depends_of_evar_map evm acc =
+  Evd.fold (fun ev evi -> depends_of_evar_info evi) evm acc
+and depends_of_evar_info evi acc =
+  (* TODO: evi.evar_extra contains a dynamic... Figure out what to do with it. *)
+  depends_of_constr evi.Evd.evar_concl (depends_of_evar_body evi.Evd.evar_body (depends_of_named_context_val evi.Evd.evar_hyps acc))
+and depends_of_evar_body evb acc = match evb with
+  | Evd.Evar_empty -> acc
+  | Evd.Evar_defined c -> depends_of_constr c acc
+and depends_of_named_context nc acc = list_union_map depends_of_named_declaration nc acc
+and depends_of_named_context_val ncv acc =
+  depends_of_named_context (Environ.named_context_of_val ncv) (depends_of_named_vals (Environ.named_vals_of_val ncv) acc)
+and depends_of_named_declaration (_,co,t) acc = depends_of_constr t (Option.fold_right depends_of_constr co acc)
+
+
+
+let depends_of_open_constr (evm,c) acc =
+  depends_of_constr c (depends_of_evar_map evm acc)
+
+let rec depends_of_rawconstr rc acc = match rc with
+  | RRef (_,r)         -> r::acc
+  | RVar (_, id)       -> (VarRef id)::acc
+  | REvar (_, _, rclo) -> Option.fold_right depends_of_rawconstr_list rclo acc
+  | RPatVar _          -> acc
+  | RApp (_, rc, rcl)  -> depends_of_rawconstr rc (depends_of_rawconstr_list rcl acc)
+  | RLambda (_, _, _, rct, rcb)
+  | RProd   (_, _, _, rct, rcb)
+  | RLetIn  (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc)
+  | RCases  (_, _, rco, tmt, cc) ->
+      (* LEM TODO: handle the cc *)
+      (Option.fold_right depends_of_rawconstr rco
+         (list_union_map
+	    (fun (rc, pp) acc ->
+	       Option.fold_right (fun (_,ind,_,_) acc -> (IndRef ind)::acc) (snd pp)
+	       (depends_of_rawconstr rc acc))
+	    tmt
+	    acc))
+  | RLetTuple (_,_,(_,rco),rc0,rc1) ->
+     depends_of_rawconstr rc1 (depends_of_rawconstr rc0 (Option.fold_right depends_of_rawconstr rco acc))
+  | RIf (_, rcC, (_, rco), rcT, rcF) -> let dorc = depends_of_rawconstr in
+      dorc rcF (dorc rcT (dorc rcF (dorc rcC (Option.fold_right dorc rco acc))))
+  | RRec (_, _, _, rdla, rca0, rca1) -> let dorca = array_union_map depends_of_rawconstr in
+      dorca rca0 (dorca rca1 (array_union_map
+				(list_union_map (fun (_,_,rco,rc) acc -> depends_of_rawconstr rc (Option.fold_right depends_of_rawconstr rco acc)))
+				rdla
+				acc))
+  | RSort _ -> acc
+  | RHole (_, hk) -> depends_of_hole_kind hk acc
+  | RCast (_, rc, rcct) -> depends_of_rawconstr rc (depends_of_'a_cast_type depends_of_rawconstr rcct acc)
+  | RDynamic (_, dyn) -> failwith "Depends of a dyn not implemented yet" (* TODO: figure out how these dyns are used*)
+and depends_of_rawconstr_list l = list_union_map depends_of_rawconstr l
+
+let depends_of_rawconstr_and_expr (rc, _) acc =
+  (* TODO Le constr_expr représente le même terme que le rawconstr. Vérifier ça. *)
+  depends_of_rawconstr rc acc
+
+let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of_'tac =
+  (* TODO:
+   * Dirty assumptions that the 'id, 'cst, 'ref don't generate dependencies
+   *)
+  let rec depends_of_tacexpr texp acc = match texp with
+    | TacAtom (_, atexpr) -> depends_of_atomic_tacexpr atexpr acc
+    | TacThen (tac0, taca0, tac1, taca1) ->
+	depends_of_tacexpr tac0 (array_union_map depends_of_tacexpr taca0 (depends_of_tacexpr tac1 (array_union_map depends_of_tacexpr taca1 acc)))
+    | TacThens (tac, tacl) ->
+	depends_of_tacexpr tac (list_union_map depends_of_tacexpr tacl acc)
+    | TacFirst tacl -> list_union_map depends_of_tacexpr tacl acc
+    | TacComplete tac -> depends_of_tacexpr tac acc
+    | TacSolve tacl -> list_union_map depends_of_tacexpr tacl acc
+    | TacTry tac -> depends_of_tacexpr tac acc
+    | TacOrelse (tac0, tac1) -> depends_of_tacexpr tac0 (depends_of_tacexpr tac1 acc)
+    | TacDo (_, tac) -> depends_of_tacexpr tac acc
+    | TacRepeat tac -> depends_of_tacexpr tac acc
+    | TacProgress tac -> depends_of_tacexpr tac acc
+    | TacAbstract (tac, _) -> depends_of_tacexpr tac acc
+    | TacId _
+    | TacFail _ -> acc
+    | TacInfo tac -> depends_of_tacexpr tac acc
+    | TacLetIn (_, igtal, tac) ->
+	depends_of_tacexpr
+	  tac
+	  (list_union_map
+	     (fun x y -> depends_of_tac_arg (snd x) y)
+	     igtal
+	     acc)
+    | TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet"
+    | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
+    | TacFun tacfa -> depends_of_tac_fun_ast tacfa acc
+    | TacArg tacarg -> depends_of_tac_arg tacarg acc
+  and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with
+      (* Basic tactics *)
+    | TacIntroPattern _
+    | TacIntrosUntil _
+    | TacIntroMove _
+    | TacAssumption  -> acc
+    | TacExact          c
+    | TacExactNoCheck   c
+    | TacVmCastNoCheck  c  -> depends_of_'constr c acc
+    | TacApply (_, _, cb) -> depends_of_'constr_with_bindings cb acc
+    | TacElim (_, cwb, cwbo) ->
+	depends_of_'constr_with_bindings cwb
+	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
+    | TacElimType c -> depends_of_'constr c acc
+    | TacCase (_, cb) -> depends_of_'constr_with_bindings cb acc
+    | TacCaseType c -> depends_of_'constr c acc
+    | TacFix _
+    | TacMutualFix _
+    | TacCofix _
+    | TacMutualCofix _ -> failwith "depends_of_atomic_tacexpr of a Tac(Mutual)(Co)Fix not implemented yet"
+    | TacCut c -> depends_of_'constr c acc
+    | TacAssert (taco, _, c) ->
+	Option.fold_right depends_of_'tac taco (depends_of_'constr c acc)
+    | TacGeneralize cl ->
+	list_union_map depends_of_'constr (List.map (fun ((_,c),_) -> c) cl)
+	acc
+    | TacGeneralizeDep c -> depends_of_'constr c acc
+    | TacLetTac (_,c,_,_) -> depends_of_'constr c acc
+
+    (* Derived basic tactics *)
+    | TacSimpleInduction _
+    | TacSimpleDestruct  _
+    | TacDoubleInduction _ -> acc
+    | TacNewInduction (_, cwbial, cwbo, _, _)
+    | TacNewDestruct (_, cwbial, cwbo, _, _) ->
+	list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings)
+	  cwbial
+	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
+    | TacDecomposeAnd c
+    | TacDecomposeOr  c -> depends_of_'constr c acc
+    | TacDecompose (il, c) -> depends_of_'constr c (list_union_map depends_of_'ind il acc)
+    | TacSpecialize (_,cwb) -> depends_of_'constr_with_bindings cwb acc
+    | TacLApply c -> depends_of_'constr c acc
+
+    (* Automation tactics *)
+    | TacTrivial (cl, bs) -> 
+	(* TODO: Maybe make use of bs: list of hint bases to be used. *)
+	list_union_map depends_of_'constr cl acc
+    | TacAuto (_, cs, bs) ->
+	(* TODO: Maybe make use of bs: list of hint bases to be used.
+           None -> all ("with *")
+           Some list -> a list, "core" added implicitly *)
+	list_union_map depends_of_'constr cs acc
+    | TacAutoTDB _     -> acc
+    | TacDestructHyp _ -> acc
+    | TacDestructConcl -> acc
+    | TacSuperAuto _ -> (* TODO: this reference thing is scary*)
+	acc
+    | TacDAuto     _ -> acc
+
+    (* Context management *)
+    | TacClear     _
+    | TacClearBody _
+    | TacMove      _
+    | TacRename    _ 
+    | TacRevert    _ -> acc
+
+    (* Constructors *)
+    | TacLeft        (_,cb)
+    | TacRight       (_,cb)
+    | TacSplit       (_, _, cb)
+    | TacConstructor (_, _, cb) -> depends_of_'a_bindings depends_of_'constr cb acc
+    | TacAnyConstructor (_,taco) -> Option.fold_right depends_of_'tac taco acc
+
+    (* Conversion *)
+    | TacReduce  (reg,_) ->
+	depends_of_'a_'b_red_expr_gen depends_of_'constr reg acc
+    | TacChange (cwoo, c, _) ->
+	depends_of_'constr
+	  c
+	  (Option.fold_right (depends_of_'a_with_occurences depends_of_'constr) cwoo acc)
+
+    (* Equivalence relations *)
+    | TacReflexivity
+    | TacSymmetry     _ -> acc
+    | TacTransitivity c -> depends_of_'constr c acc
+
+    (* Equality and inversion *)
+    | TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc
+    | TacInversion (is, _)  -> depends_of_'a_'b_inversion_strength depends_of_'constr is acc
+
+    (* For ML extensions *)
+    | TacExtend (_, _, cgal) -> failwith "depends of TacExtend not implemented because depends of a generic_argument not implemented"
+
+    (* For syntax extensions *)
+    | TacAlias (_,_,gal,(_,gte)) -> failwith "depends of a TacAlias not implemented because depends of a generic_argument not implemented"
+  and depends_of_tac_fun_ast tfa acc = failwith "depend_of_tac_fun_ast not implemented yet"
+  and depends_of_tac_arg ta acc = match ta with
+    | TacDynamic (_,d)  -> failwith "Don't know what to do with a Dyn in tac_arg"
+    | TacVoid           -> acc
+    | MetaIdArg  _      -> failwith "Don't know what to do with a MetaIdArg in tac_arg"
+    | ConstrMayEval  me -> failwith "TODO: depends_of_tac_arg of a ConstrMayEval"
+    | IntroPattern   _  -> acc
+    | Reference     ltc -> acc (* TODO: This assumes the "ltac constant" cannot somehow refer to a named object... *)
+    | Integer       _   -> acc
+    | TacCall (_,ltc,l) -> (* TODO: This assumes the "ltac constant" cannot somehow refer to a named object... *)
+	list_union_map depends_of_tac_arg l acc
+    | TacExternal (_,_,_,l) -> list_union_map depends_of_tac_arg l acc
+    | TacFreshId     _  -> acc
+    | Tacexp       tac  ->
+	depends_of_'tac tac acc
+  in
+    depends_of_tacexpr
+
+let rec depends_of_glob_tactic_expr (gte:glob_tactic_expr) acc =
+  depends_of_gen_tactic_expr
+    depends_of_rawconstr_and_expr
+    (depends_of_'a_or_var depends_of_inductive)
+    depends_of_glob_tactic_expr
+    gte
+    acc
+
+let rec depends_of_tacexpr te acc =
+  depends_of_gen_tactic_expr
+    depends_of_open_constr
+    depends_of_inductive
+    depends_of_glob_tactic_expr
+    te
+    acc
+
+let depends_of_compound_rule cr acc = match cr with
+  | Tactic (texp, _) -> depends_of_tacexpr texp acc
+  | Proof_instr (b, instr) ->
+      (* TODO: What is the boolean b? Should check. *)
+      failwith "Dependency calculation of Proof_instr not implemented yet"
+and depends_of_prim_rule pr acc = match pr with
+  | Refine c                     -> depends_of_constr c acc
+  | Intro id                     -> acc
+  | Intro_replacing id           -> acc
+  | Cut (_, _, t)                -> depends_of_constr t acc (* TODO: check what 2nd argument contains *)
+  | FixRule (_, _, l)            -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
+  | Cofix (_, l)                 -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
+  | Convert_concl (t, _)         -> depends_of_constr t acc
+  | Convert_hyp (_, None, t)     -> depends_of_constr t acc
+  | Convert_hyp (_, (Some c), t) -> depends_of_constr c (depends_of_constr t acc)
+  | Thin _                       -> acc
+  | ThinBody _                   -> acc
+  | Move _                       -> acc
+  | Rename _                     -> acc
+  | Change_evars                 -> acc
+
+let rec depends_of_pftree pt acc =
+  match pt.ref with
+    | None -> acc
+    | Some (Prim   pr    , l) -> depends_of_prim_rule pr (list_union_map depends_of_pftree l  acc)
+    | Some (Nested (t, p), l) -> depends_of_compound_rule t (depends_of_pftree p (list_union_map depends_of_pftree l acc))
+    | Some (Decl_proof _ , l) -> list_union_map depends_of_pftree l acc
+    | Some (Daimon,        l) -> list_union_map depends_of_pftree l acc
+
+let rec depends_of_pftree_head pt acc =
+  match pt.ref with
+    | None -> acc
+    | Some (Prim   pr    , l) -> depends_of_prim_rule pr acc
+    | Some (Nested (t, p), l) -> depends_of_compound_rule t (depends_of_pftree p acc)
+    | Some (Decl_proof _ , l) -> acc
+    | Some (Daimon,        l) -> acc
+
+let depends_of_pftreestate depends_of_pftree pfs =
+(*   print_string "depends_of_pftreestate called\n"; *)
+(*   explore_tree pfs; *)
+  let pt = proof_of_pftreestate pfs in
+    assert (is_top_pftreestate pfs);
+    assert (pt.open_subgoals = 0);
+    depends_of_pftree pt []
+
+let depends_of_definition_entry de ~acc =
+  Option.fold_right
+    depends_of_constr
+    de.const_entry_type
+    (depends_of_constr de.const_entry_body acc)
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 9a503cfb..6b17e739 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -28,7 +28,7 @@ let convert_env =
     let convert_binder env (na, b, c) =
       match b with 
        | Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b)
-       | None -> LocalRawAssum ([dummy_loc,na], extern_constr true env c) in
+       | None -> LocalRawAssum ([dummy_loc,na], default_binder_kind, extern_constr true env c) in
     let rec cvrec env = function
        [] -> []
      | b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in
@@ -134,14 +134,14 @@ let implicits_to_ast_list implicits =
 
 let make_variable_ast name typ implicits =
   (VernacAssumption
-    ((Local,Definitional),
-     [false,([dummy_loc,name], constr_to_ast (body_of_type typ))]))
+    ((Local,Definitional),false,(*inline flag*)
+     [false,([dummy_loc,name], constr_to_ast typ)]))
   ::(implicits_to_ast_list implicits);;
     
 
 let make_definition_ast name c typ implicits =
-  VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None,
-    (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
+  VernacDefinition ((Global,false,Definition), (dummy_loc,name), 
+		   DefineBody ([], None, constr_to_ast c, Some (constr_to_ast typ)),
     (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
 
@@ -158,7 +158,7 @@ let constant_to_ast_list kn =
 	make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l)
 
 let variable_to_ast_list sp =
-  let (id, c, v) = get_variable sp in
+  let (id, c, v) = Global.lookup_named sp in
   let l = implicits_of_global (VarRef sp) in
     (match c with
 	 None -> 
diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli
index b8c2d7dc..f9e83b5e 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/contrib/interface/name_to_ast.mli
@@ -1 +1,5 @@
 val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;;
+val inductive_to_ast_list : Names.mutual_inductive -> Vernacexpr.vernac_expr list;;
+val constant_to_ast_list : Names.constant -> Vernacexpr.vernac_expr list;;
+val variable_to_ast_list : Names.variable -> Vernacexpr.vernac_expr list;;
+val leaf_entry_to_ast_list : (Libnames.section_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 8cca7614..bf8614b4 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -21,18 +21,19 @@ type parsed_tree =
   | P_i of ct_INT;;
 
 let print_parse_results n msg =
-  print_string "message\nparsed\n";
-  print_int n;
-  print_string "\n";
-  (match msg with
-  | P_cl x -> fCOMMAND_LIST x
-  | P_c x -> fCOMMAND x
-  | P_t x -> fTACTIC_COM x
-  | P_f x -> fFORMULA x
-  | P_id x -> fID x
-  | P_s x -> fSTRING x
-  | P_i x -> fINT x);
-  print_string "e\nblabla\n";
+  Pp.msg
+  ( str "message\nparsed\n" ++
+    int n ++
+    str "\n" ++
+    (match msg with
+     | P_cl x -> fCOMMAND_LIST x
+     | P_c x -> fCOMMAND x
+     | P_t x -> fTACTIC_COM x
+     | P_f x -> fFORMULA x
+     | P_id x -> fID x
+     | P_s x -> fSTRING x
+     | P_i x -> fINT x) ++
+    str "e\nblabla\n");
   flush stdout;;
 
 let ctf_SyntaxErrorMessage reqid pps =
@@ -329,7 +330,7 @@ let add_path_action reqid string_arg =
 
 let print_version_action () =
   msgnl (mt ());
-  msgnl (str "$Id: parse.ml 9397 2006-11-21 21:50:54Z herbelin $");;
+  msgnl (str "$Id: parse.ml 9476 2007-01-10 15:44:44Z lmamane $");;
 
 let load_syntax_action reqid module_name =
  msg (str "loading " ++ str module_name ++ str "... ");
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index d2f71bfc..06b957d9 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -156,29 +156,29 @@ let make_pbp_pattern x =
 let rec make_then = function
   | [] -> TacId []
   | [t] -> t
-  | t1::t2::l -> make_then (TacThen (t1,t2)::l)
+  | t1::t2::l -> make_then (TacThen (t1,[||],t2,[||])::l)
 
 let make_pbp_atomic_tactic = function
   | PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption))
   | PbpTryAssumption (Some a) ->
       TacTry (TacAtom (zz, TacExact (make_var a)))
   | PbpExists x -> 
-      TacAtom (zz, TacSplit (true,ImplicitBindings [make_pbp_pattern x]))
+      TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x]))
   | PbpGeneralize (h,args) ->
       let l = List.map make_pbp_pattern args in
-      TacAtom (zz, TacGeneralize [make_app (make_var h) l])
-  | PbpLeft -> TacAtom (zz, TacLeft NoBindings)
-  | PbpRight -> TacAtom (zz, TacRight NoBindings)
+      TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous])
+  | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings))
+  | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
-  | PbpApply h -> TacAtom (zz, TacApply (make_var h,NoBindings))
+  | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings)))
   | PbpElim (hyp_name, names) ->
       let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
       TacAtom
-	(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
+	(zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
       TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
-  | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
+  | PbpSplit -> TacAtom (zz, TacSplit (false,false,NoBindings));;
 
 let rec make_pbp_tactic = function
   | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 4bec7350..953fb5e7 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -166,7 +166,7 @@ let rule_to_ntactic r =
    let rt =
      (match r with
        Nested(Tactic (t,_),_) -> t
-     | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h)
+     | Prim (Refine h) -> TacAtom (dummy_loc,TacExact (Tactics.inj_open h))
      | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in
    if rule_is_complex r
    then (match rt with
@@ -1183,8 +1183,8 @@ let rec natural_ntree ig ntree =
 	    TacIntroPattern _ -> natural_intros ig lh g gs ltree
 	  | TacIntroMove _ -> natural_intros ig lh g gs ltree
 	  | TacFix (_,n) -> natural_fix ig lh g gs n ltree
-	  | TacSplit (_,NoBindings) -> natural_split ig lh g gs ge [] ltree
-	  | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge l ltree
+	  | TacSplit (_,_,NoBindings) -> natural_split ig lh g gs ge [] ltree
+	  | TacSplit(_,_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree
 	  | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree
 	  | TacRight _ -> natural_right ig lh g gs ltree
 	  | TacLeft _ -> natural_left ig lh g gs ltree
@@ -1202,17 +1202,18 @@ let rec natural_ntree ig ntree =
 	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
               natural_induction ig lh g gs ge id ltree true
-	  | TacApply (c,_) -> natural_apply ig lh g gs c ltree
-	  | TacExact c -> natural_exact ig lh g gs c ltree
-	  | TacCut c -> natural_cut ig lh g gs c ltree
+	  | TacApply (_,false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree
+	  | TacExact c -> natural_exact ig lh g gs (snd c) ltree
+	  | TacCut c -> natural_cut ig lh g gs (snd c) ltree
 	  | TacExtend (_,"CutIntro",[a]) ->
 	      let _c = out_gen wit_constr a in
 	      natural_cutintro ig lh g gs a ltree
-	  | TacCase (c,_) -> natural_case ig lh g gs ge c ltree false
+	  | TacCase (_,(c,_)) -> natural_case ig lh g gs ge (snd c) ltree false
 	  | TacExtend (_,"CaseIntro",[a]) ->
 	      let c = out_gen wit_constr a in
 	      natural_case ig lh g gs ge c ltree true
-	  | TacElim ((c,_),_) -> natural_elim ig lh g gs ge c ltree false
+	  | TacElim (_,(c,_),_) ->
+	      natural_elim ig lh g gs ge (snd c) ltree false
 	  | TacExtend (_,"ElimIntro",[a]) ->
 	      let c = out_gen wit_constr a in
 	      natural_elim ig lh g gs ge c ltree true
@@ -1611,7 +1612,7 @@ and natural_fix ig lh g gs narg ltree =
    | _ -> assert false
 and natural_reduce ig lh g gs ge mode la ltree =
   match la with
-    {onhyps=Some[];onconcl=true} -> 
+    {onhyps=Some[]} when la.concl_occs <> no_occurrences_expr -> 
       spv
         [  (natural_lhyp lh ig.ihsg);
           (show_goal2 lh ig g gs ""); 
@@ -1619,7 +1620,7 @@ and natural_reduce ig lh g gs ge mode la ltree =
 		  {ihsg=All_subgoals_hyp;isgintro="simpl"})
              ltree)
         ]
-  | {onhyps=Some[hyp]; onconcl=false} ->
+  | {onhyps=Some[hyp]} when la.concl_occs = no_occurrences_expr ->
       spv
         [  (natural_lhyp lh ig.ihsg);
           (show_goal2 lh ig g gs ""); 
@@ -1651,7 +1652,7 @@ and natural_split ig lh g gs ge la ltree =
   | _ -> assert false
 and natural_generalize ig lh g gs ge la ltree =
   match la with
-    [arg] ->
+    [(_,(_,arg)),_] ->
       let _env= (gLOB ge) in
       let arg1= (*dbize env*) arg in
       let _type_arg=type_of (Global.env()) Evd.empty arg in
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index 6e4782be..559860b2 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -75,3 +75,6 @@ let translate_path l =
 (*translates a path and a goal into a centaur-tree --> RULE *)
 let translate_goal (g:goal) =
  CT_rule(translate_sign (evar_env g), translate_constr true (evar_env g) g.evar_concl);;
+
+let translate_goals (gl: goal list) =
+ CT_rule_list (List.map translate_goal gl);;
diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli
index 65d8331b..34841fc4 100644
--- a/contrib/interface/translate.mli
+++ b/contrib/interface/translate.mli
@@ -5,6 +5,7 @@ open Environ;;
 open Term;;
 
 val translate_goal : goal -> ct_RULE;;
+val translate_goals : goal list -> ct_RULE_LIST;;
 (* The boolean argument indicates whether names from the environment should *)
 (*  be avoided (same interpretation as for prterm_env and ast_of_constr)    *)
 val translate_constr : bool -> env -> constr -> ct_FORMULA;;
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 166a0cbf..551ad3a3 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1,103 +1,108 @@
 open Ascent;;
+open Pp;;
+
+(* LEM: This is actually generated automatically *)
 
 let fNODE s n =
-    print_string "n\n";
-    print_string ("vernac$" ^ s);
-    print_string "\n";
-    print_int n;
-    print_string "\n";;
+    (str "n\n") ++
+    (str ("vernac$" ^ s)) ++
+    (str "\n") ++
+    (int n) ++
+    (str "\n");;
 
 let fATOM s1 =
-    print_string "a\n";
-    print_string ("vernac$" ^ s1);
-    print_string "\n";;
+    (str "a\n") ++
+    (str ("vernac$" ^ s1)) ++
+    (str "\n");;
 
-let f_atom_string = print_string;;
-let f_atom_int = print_int;;
+let f_atom_string = str;;
+let f_atom_int = int;;
 let rec fAST = function
 | CT_coerce_ID_OR_INT_to_AST x -> fID_OR_INT x
 | CT_coerce_ID_OR_STRING_to_AST x -> fID_OR_STRING x
 | CT_coerce_SINGLE_OPTION_VALUE_to_AST x -> fSINGLE_OPTION_VALUE x
 | CT_astnode(x1, x2) ->
-   fID x1;
-   fAST_LIST x2;
+   fID x1 ++
+   fAST_LIST x2 ++
    fNODE "astnode" 2
 | CT_astpath(x1) ->
-   fID_LIST x1;
+   fID_LIST x1 ++
    fNODE "astpath" 1
 | CT_astslam(x1, x2) ->
-   fID_OPT x1;
-   fAST x2;
+   fID_OPT x1 ++
+   fAST x2 ++
    fNODE "astslam" 2
 and fAST_LIST = function
 | CT_ast_list l ->
-   (List.iter fAST l);
+   (List.fold_left (++) (mt()) (List.map fAST l)) ++
    fNODE "ast_list" (List.length l)
 and fBINARY = function
-| CT_binary x -> fATOM "binary";
-   (f_atom_int x);
-   print_string "\n"and fBINDER = function
+| CT_binary x -> fATOM "binary" ++
+   (f_atom_int x) ++
+   str "\n"
+and fBINDER = function
 | CT_coerce_DEF_to_BINDER x -> fDEF x
 | CT_binder(x1, x2) ->
-   fID_OPT_NE_LIST x1;
-   fFORMULA x2;
+   fID_OPT_NE_LIST x1 ++
+   fFORMULA x2 ++
    fNODE "binder" 2
 | CT_binder_coercion(x1, x2) ->
-   fID_OPT_NE_LIST x1;
-   fFORMULA x2;
+   fID_OPT_NE_LIST x1 ++
+   fFORMULA x2 ++
    fNODE "binder_coercion" 2
 and fBINDER_LIST = function
 | CT_binder_list l ->
-   (List.iter fBINDER l);
+   (List.fold_left (++) (mt()) (List.map fBINDER l)) ++
    fNODE "binder_list" (List.length l)
 and fBINDER_NE_LIST = function
 | CT_binder_ne_list(x,l) ->
-   fBINDER x;
-   (List.iter fBINDER l);
+   fBINDER x ++
+   (List.fold_left (++) (mt()) (List.map fBINDER l)) ++
    fNODE "binder_ne_list" (1 + (List.length l))
 and fBINDING = function
 | CT_binding(x1, x2) ->
-   fID_OR_INT x1;
-   fFORMULA x2;
+   fID_OR_INT x1 ++
+   fFORMULA x2 ++
    fNODE "binding" 2
 and fBINDING_LIST = function
 | CT_binding_list l ->
-   (List.iter fBINDING l);
+   (List.fold_left (++) (mt()) (List.map fBINDING l)) ++
    fNODE "binding_list" (List.length l)
 and fBOOL = function
 | CT_false -> fNODE "false" 0
 | CT_true -> fNODE "true" 0
 and fCASE = function
-| CT_case x -> fATOM "case";
-   (f_atom_string x);
-   print_string "\n"and fCLAUSE = function
+| CT_case x -> fATOM "case" ++
+   (f_atom_string x) ++
+   str "\n"
+and fCLAUSE = function
 | CT_clause(x1, x2) ->
-   fHYP_LOCATION_LIST_OR_STAR x1;
-   fSTAR_OPT 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 fCOFIXTAC = function
 | CT_cofixtac(x1, x2) ->
-   fID x1;
-   fFORMULA x2;
+   fID x1 ++
+   fFORMULA x2 ++
    fNODE "cofixtac" 2
 and fCOFIX_REC = function
 | CT_cofix_rec(x1, x2, x3, x4) ->
-   fID x1;
-   fBINDER_LIST x2;
-   fFORMULA x3;
-   fFORMULA x4;
+   fID x1 ++
+   fBINDER_LIST x2 ++
+   fFORMULA x3 ++
+   fFORMULA x4 ++
    fNODE "cofix_rec" 4
 and fCOFIX_REC_LIST = function
 | CT_cofix_rec_list(x,l) ->
-   fCOFIX_REC x;
-   (List.iter fCOFIX_REC l);
+   fCOFIX_REC x ++
+   (List.fold_left (++) (mt()) (List.map fCOFIX_REC l)) ++
    fNODE "cofix_rec_list" (1 + (List.length l))
 and fCOFIX_TAC_LIST = function
 | CT_cofix_tac_list l ->
-   (List.iter fCOFIXTAC l);
+   (List.fold_left (++) (mt()) (List.map fCOFIXTAC l)) ++
    fNODE "cofix_tac_list" (List.length l)
 and fCOMMAND = function
 | CT_coerce_COMMAND_LIST_to_COMMAND x -> fCOMMAND_LIST x
@@ -105,479 +110,476 @@ and fCOMMAND = function
 | CT_coerce_SECTION_BEGIN_to_COMMAND x -> fSECTION_BEGIN x
 | CT_coerce_THEOREM_GOAL_to_COMMAND x -> fTHEOREM_GOAL x
 | CT_abort(x1) ->
-   fID_OPT_OR_ALL x1;
+   fID_OPT_OR_ALL x1 ++
    fNODE "abort" 1
 | CT_abstraction(x1, x2, x3) ->
-   fID x1;
-   fFORMULA x2;
-   fINT_LIST x3;
+   fID x1 ++
+   fFORMULA x2 ++
+   fINT_LIST x3 ++
    fNODE "abstraction" 3
 | CT_add_field(x1, x2, x3, x4) ->
-   fFORMULA x1;
-   fFORMULA x2;
-   fFORMULA x3;
-   fFORMULA_OPT x4;
+   fFORMULA x1 ++
+   fFORMULA x2 ++
+   fFORMULA x3 ++
+   fFORMULA_OPT x4 ++
    fNODE "add_field" 4
 | CT_add_natural_feature(x1, x2) ->
-   fNATURAL_FEATURE x1;
-   fID x2;
+   fNATURAL_FEATURE x1 ++
+   fID x2 ++
    fNODE "add_natural_feature" 2
 | CT_addpath(x1, x2) ->
-   fSTRING x1;
-   fID_OPT x2;
+   fSTRING x1 ++
+   fID_OPT x2 ++
    fNODE "addpath" 2
 | CT_arguments_scope(x1, x2) ->
-   fID x1;
-   fID_OPT_LIST x2;
+   fID x1 ++
+   fID_OPT_LIST x2 ++
    fNODE "arguments_scope" 2
 | CT_bind_scope(x1, x2) ->
-   fID x1;
-   fID_NE_LIST x2;
+   fID x1 ++
+   fID_NE_LIST x2 ++
    fNODE "bind_scope" 2
 | CT_cd(x1) ->
-   fSTRING_OPT x1;
+   fSTRING_OPT x1 ++
    fNODE "cd" 1
 | CT_check(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "check" 1
 | CT_class(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "class" 1
 | CT_close_scope(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "close_scope" 1
 | CT_coercion(x1, x2, x3, x4, x5) ->
-   fLOCAL_OPT x1;
-   fIDENTITY_OPT x2;
-   fID x3;
-   fID x4;
-   fID x5;
+   fLOCAL_OPT x1 ++
+   fIDENTITY_OPT x2 ++
+   fID x3 ++
+   fID x4 ++
+   fID x5 ++
    fNODE "coercion" 5
 | CT_cofix_decl(x1) ->
-   fCOFIX_REC_LIST x1;
+   fCOFIX_REC_LIST x1 ++
    fNODE "cofix_decl" 1
 | CT_compile_module(x1, x2, x3) ->
-   fVERBOSE_OPT x1;
-   fID x2;
-   fSTRING_OPT x3;
+   fVERBOSE_OPT x1 ++
+   fID x2 ++
+   fSTRING_OPT x3 ++
    fNODE "compile_module" 3
 | CT_declare_module(x1, x2, x3, x4) ->
-   fID x1;
-   fMODULE_BINDER_LIST x2;
-   fMODULE_TYPE_CHECK x3;
-   fMODULE_EXPR x4;
+   fID x1 ++
+   fMODULE_BINDER_LIST x2 ++
+   fMODULE_TYPE_CHECK x3 ++
+   fMODULE_EXPR x4 ++
    fNODE "declare_module" 4
 | CT_define_notation(x1, x2, x3, x4) ->
-   fSTRING x1;
-   fFORMULA x2;
-   fMODIFIER_LIST x3;
-   fID_OPT x4;
+   fSTRING x1 ++
+   fFORMULA x2 ++
+   fMODIFIER_LIST x3 ++
+   fID_OPT x4 ++
    fNODE "define_notation" 4
 | CT_definition(x1, x2, x3, x4, x5) ->
-   fDEFN x1;
-   fID x2;
-   fBINDER_LIST x3;
-   fDEF_BODY x4;
-   fFORMULA_OPT x5;
+   fDEFN x1 ++
+   fID x2 ++
+   fBINDER_LIST x3 ++
+   fDEF_BODY x4 ++
+   fFORMULA_OPT x5 ++
    fNODE "definition" 5
 | CT_delim_scope(x1, x2) ->
-   fID x1;
-   fID x2;
+   fID x1 ++
+   fID x2 ++
    fNODE "delim_scope" 2
 | CT_delpath(x1) ->
-   fSTRING x1;
+   fSTRING x1 ++
    fNODE "delpath" 1
 | CT_derive_depinversion(x1, x2, x3, x4) ->
-   fINV_TYPE x1;
-   fID x2;
-   fFORMULA x3;
-   fSORT_TYPE x4;
+   fINV_TYPE x1 ++
+   fID x2 ++
+   fFORMULA x3 ++
+   fSORT_TYPE x4 ++
    fNODE "derive_depinversion" 4
 | CT_derive_inversion(x1, x2, x3, x4) ->
-   fINV_TYPE x1;
-   fINT_OPT x2;
-   fID x3;
-   fID x4;
+   fINV_TYPE x1 ++
+   fINT_OPT x2 ++
+   fID x3 ++
+   fID x4 ++
    fNODE "derive_inversion" 4
 | CT_derive_inversion_with(x1, x2, x3, x4) ->
-   fINV_TYPE x1;
-   fID x2;
-   fFORMULA x3;
-   fSORT_TYPE x4;
+   fINV_TYPE x1 ++
+   fID x2 ++
+   fFORMULA x3 ++
+   fSORT_TYPE x4 ++
    fNODE "derive_inversion_with" 4
 | CT_explain_proof(x1) ->
-   fINT_LIST x1;
+   fINT_LIST x1 ++
    fNODE "explain_proof" 1
 | CT_explain_prooftree(x1) ->
-   fINT_LIST x1;
+   fINT_LIST x1 ++
    fNODE "explain_prooftree" 1
 | CT_export_id(x1) ->
-   fID_NE_LIST x1;
+   fID_NE_LIST x1 ++
    fNODE "export_id" 1
 | CT_extract_to_file(x1, x2) ->
-   fSTRING x1;
-   fID_NE_LIST x2;
+   fSTRING x1 ++
+   fID_NE_LIST x2 ++
    fNODE "extract_to_file" 2
 | CT_extraction(x1) ->
-   fID_OPT x1;
+   fID_OPT x1 ++
    fNODE "extraction" 1
 | CT_fix_decl(x1) ->
-   fFIX_REC_LIST x1;
+   fFIX_REC_LIST x1 ++
    fNODE "fix_decl" 1
 | CT_focus(x1) ->
-   fINT_OPT x1;
+   fINT_OPT x1 ++
    fNODE "focus" 1
 | CT_go(x1) ->
-   fINT_OR_LOCN x1;
+   fINT_OR_LOCN x1 ++
    fNODE "go" 1
 | CT_guarded -> fNODE "guarded" 0
 | CT_hint_destruct(x1, x2, x3, x4, x5, x6) ->
-   fID x1;
-   fINT x2;
-   fDESTRUCT_LOCATION x3;
-   fFORMULA x4;
-   fTACTIC_COM x5;
-   fID_LIST x6;
+   fID x1 ++
+   fINT x2 ++
+   fDESTRUCT_LOCATION x3 ++
+   fFORMULA x4 ++
+   fTACTIC_COM x5 ++
+   fID_LIST x6 ++
    fNODE "hint_destruct" 6
 | CT_hint_extern(x1, x2, x3, x4) ->
-   fINT x1;
-   fFORMULA x2;
-   fTACTIC_COM x3;
-   fID_LIST x4;
+   fINT x1 ++
+   fFORMULA x2 ++
+   fTACTIC_COM x3 ++
+   fID_LIST x4 ++
    fNODE "hint_extern" 4
 | CT_hintrewrite(x1, x2, x3, x4) ->
-   fORIENTATION x1;
-   fFORMULA_NE_LIST x2;
-   fID x3;
-   fTACTIC_COM x4;
+   fORIENTATION x1 ++
+   fFORMULA_NE_LIST x2 ++
+   fID x3 ++
+   fTACTIC_COM x4 ++
    fNODE "hintrewrite" 4
 | CT_hints(x1, x2, x3) ->
-   fID x1;
-   fID_NE_LIST x2;
-   fID_LIST x3;
+   fID x1 ++
+   fID_NE_LIST x2 ++
+   fID_LIST x3 ++
    fNODE "hints" 3
 | CT_hints_immediate(x1, x2) ->
-   fFORMULA_NE_LIST x1;
-   fID_LIST x2;
+   fFORMULA_NE_LIST x1 ++
+   fID_LIST x2 ++
    fNODE "hints_immediate" 2
 | CT_hints_resolve(x1, x2) ->
-   fFORMULA_NE_LIST x1;
-   fID_LIST x2;
+   fFORMULA_NE_LIST x1 ++
+   fID_LIST x2 ++
    fNODE "hints_resolve" 2
 | CT_hyp_search_pattern(x1, x2) ->
-   fFORMULA x1;
-   fIN_OR_OUT_MODULES x2;
+   fFORMULA x1 ++
+   fIN_OR_OUT_MODULES x2 ++
    fNODE "hyp_search_pattern" 2
 | CT_implicits(x1, x2) ->
-   fID x1;
-   fID_LIST_OPT x2;
+   fID x1 ++
+   fID_LIST_OPT x2 ++
    fNODE "implicits" 2
 | CT_import_id(x1) ->
-   fID_NE_LIST x1;
+   fID_NE_LIST x1 ++
    fNODE "import_id" 1
 | CT_ind_scheme(x1) ->
-   fSCHEME_SPEC_LIST x1;
+   fSCHEME_SPEC_LIST x1 ++
    fNODE "ind_scheme" 1
 | CT_infix(x1, x2, x3, x4) ->
-   fSTRING x1;
-   fID x2;
-   fMODIFIER_LIST x3;
-   fID_OPT x4;
+   fSTRING x1 ++
+   fID x2 ++
+   fMODIFIER_LIST x3 ++
+   fID_OPT x4 ++
    fNODE "infix" 4
 | CT_inline(x1) ->
-   fID_NE_LIST x1;
+   fID_NE_LIST x1 ++
    fNODE "inline" 1
 | CT_inspect(x1) ->
-   fINT x1;
+   fINT x1 ++
    fNODE "inspect" 1
 | CT_kill_node(x1) ->
-   fINT x1;
+   fINT x1 ++
    fNODE "kill_node" 1
 | CT_load(x1, x2) ->
-   fVERBOSE_OPT x1;
-   fID_OR_STRING x2;
+   fVERBOSE_OPT x1 ++
+   fID_OR_STRING x2 ++
    fNODE "load" 2
 | CT_local_close_scope(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "local_close_scope" 1
 | CT_local_define_notation(x1, x2, x3, x4) ->
-   fSTRING x1;
-   fFORMULA x2;
-   fMODIFIER_LIST x3;
-   fID_OPT x4;
+   fSTRING x1 ++
+   fFORMULA x2 ++
+   fMODIFIER_LIST x3 ++
+   fID_OPT x4 ++
    fNODE "local_define_notation" 4
 | CT_local_hint_destruct(x1, x2, x3, x4, x5, x6) ->
-   fID x1;
-   fINT x2;
-   fDESTRUCT_LOCATION x3;
-   fFORMULA x4;
-   fTACTIC_COM x5;
-   fID_LIST x6;
+   fID x1 ++
+   fINT x2 ++
+   fDESTRUCT_LOCATION x3 ++
+   fFORMULA x4 ++
+   fTACTIC_COM x5 ++
+   fID_LIST x6 ++
    fNODE "local_hint_destruct" 6
 | CT_local_hint_extern(x1, x2, x3, x4) ->
-   fINT x1;
-   fFORMULA x2;
-   fTACTIC_COM x3;
-   fID_LIST x4;
+   fINT x1 ++
+   fFORMULA x2 ++
+   fTACTIC_COM x3 ++
+   fID_LIST x4 ++
    fNODE "local_hint_extern" 4
 | CT_local_hints(x1, x2, x3) ->
-   fID x1;
-   fID_NE_LIST x2;
-   fID_LIST x3;
+   fID x1 ++
+   fID_NE_LIST x2 ++
+   fID_LIST x3 ++
    fNODE "local_hints" 3
 | CT_local_hints_immediate(x1, x2) ->
-   fFORMULA_NE_LIST x1;
-   fID_LIST x2;
+   fFORMULA_NE_LIST x1 ++
+   fID_LIST x2 ++
    fNODE "local_hints_immediate" 2
 | CT_local_hints_resolve(x1, x2) ->
-   fFORMULA_NE_LIST x1;
-   fID_LIST x2;
+   fFORMULA_NE_LIST x1 ++
+   fID_LIST x2 ++
    fNODE "local_hints_resolve" 2
 | CT_local_infix(x1, x2, x3, x4) ->
-   fSTRING x1;
-   fID x2;
-   fMODIFIER_LIST x3;
-   fID_OPT x4;
+   fSTRING x1 ++
+   fID x2 ++
+   fMODIFIER_LIST x3 ++
+   fID_OPT x4 ++
    fNODE "local_infix" 4
 | CT_local_open_scope(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "local_open_scope" 1
 | CT_local_reserve_notation(x1, x2) ->
-   fSTRING x1;
-   fMODIFIER_LIST x2;
+   fSTRING x1 ++
+   fMODIFIER_LIST x2 ++
    fNODE "local_reserve_notation" 2
 | CT_locate(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "locate" 1
 | CT_locate_file(x1) ->
-   fSTRING x1;
+   fSTRING x1 ++
    fNODE "locate_file" 1
 | CT_locate_lib(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "locate_lib" 1
 | CT_locate_notation(x1) ->
-   fSTRING x1;
+   fSTRING x1 ++
    fNODE "locate_notation" 1
 | CT_mind_decl(x1, x2) ->
-   fCO_IND x1;
-   fIND_SPEC_LIST x2;
+   fCO_IND x1 ++
+   fIND_SPEC_LIST x2 ++
    fNODE "mind_decl" 2
 | CT_ml_add_path(x1) ->
-   fSTRING x1;
+   fSTRING x1 ++
    fNODE "ml_add_path" 1
 | CT_ml_declare_modules(x1) ->
-   fSTRING_NE_LIST x1;
+   fSTRING_NE_LIST x1 ++
    fNODE "ml_declare_modules" 1
 | CT_ml_print_modules -> fNODE "ml_print_modules" 0
 | CT_ml_print_path -> fNODE "ml_print_path" 0
 | CT_module(x1, x2, x3, x4) ->
-   fID x1;
-   fMODULE_BINDER_LIST x2;
-   fMODULE_TYPE_CHECK x3;
-   fMODULE_EXPR x4;
+   fID x1 ++
+   fMODULE_BINDER_LIST x2 ++
+   fMODULE_TYPE_CHECK x3 ++
+   fMODULE_EXPR x4 ++
    fNODE "module" 4
 | CT_module_type_decl(x1, x2, x3) ->
-   fID x1;
-   fMODULE_BINDER_LIST x2;
-   fMODULE_TYPE_OPT x3;
+   fID x1 ++
+   fMODULE_BINDER_LIST x2 ++
+   fMODULE_TYPE_OPT x3 ++
    fNODE "module_type_decl" 3
 | CT_no_inline(x1) ->
-   fID_NE_LIST x1;
+   fID_NE_LIST x1 ++
    fNODE "no_inline" 1
 | CT_omega_flag(x1, x2) ->
-   fOMEGA_MODE x1;
-   fOMEGA_FEATURE x2;
+   fOMEGA_MODE x1 ++
+   fOMEGA_FEATURE x2 ++
    fNODE "omega_flag" 2
-| CT_opaque(x1) ->
-   fID_NE_LIST x1;
-   fNODE "opaque" 1
 | CT_open_scope(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "open_scope" 1
 | CT_print -> fNODE "print" 0
 | CT_print_about(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_about" 1
 | CT_print_all -> fNODE "print_all" 0
 | CT_print_classes -> fNODE "print_classes" 0
 | CT_print_ltac id ->
-   fID id;
+   fID id ++
    fNODE "print_ltac" 1
 | CT_print_coercions -> fNODE "print_coercions" 0
 | CT_print_grammar(x1) ->
-   fGRAMMAR x1;
+   fGRAMMAR x1 ++
    fNODE "print_grammar" 1
 | CT_print_graph -> fNODE "print_graph" 0
 | CT_print_hint(x1) ->
-   fID_OPT x1;
+   fID_OPT x1 ++
    fNODE "print_hint" 1
 | CT_print_hintdb(x1) ->
-   fID_OR_STAR x1;
+   fID_OR_STAR x1 ++
    fNODE "print_hintdb" 1
 | CT_print_rewrite_hintdb(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_rewrite_hintdb" 1
 | CT_print_id(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_id" 1
 | CT_print_implicit(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_implicit" 1
 | CT_print_loadpath -> fNODE "print_loadpath" 0
 | CT_print_module(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_module" 1
 | CT_print_module_type(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_module_type" 1
 | CT_print_modules -> fNODE "print_modules" 0
 | CT_print_natural(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_natural" 1
 | CT_print_natural_feature(x1) ->
-   fNATURAL_FEATURE x1;
+   fNATURAL_FEATURE x1 ++
    fNODE "print_natural_feature" 1
 | CT_print_opaqueid(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_opaqueid" 1
 | CT_print_path(x1, x2) ->
-   fID x1;
-   fID x2;
+   fID x1 ++
+   fID x2 ++
    fNODE "print_path" 2
 | CT_print_proof(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_proof" 1
 | CT_print_scope(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_scope" 1
 | CT_print_setoids -> fNODE "print_setoids" 0
 | CT_print_scopes -> fNODE "print_scopes" 0
 | CT_print_section(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "print_section" 1
 | CT_print_states -> fNODE "print_states" 0
 | CT_print_tables -> fNODE "print_tables" 0
 | CT_print_universes(x1) ->
-   fSTRING_OPT x1;
+   fSTRING_OPT x1 ++
    fNODE "print_universes" 1
 | CT_print_visibility(x1) ->
-   fID_OPT x1;
+   fID_OPT x1 ++
    fNODE "print_visibility" 1
 | CT_proof(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "proof" 1
 | CT_proof_no_op -> fNODE "proof_no_op" 0
 | CT_proof_with(x1) ->
-   fTACTIC_COM x1;
+   fTACTIC_COM x1 ++
    fNODE "proof_with" 1
 | CT_pwd -> fNODE "pwd" 0
 | CT_quit -> fNODE "quit" 0
 | CT_read_module(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "read_module" 1
 | CT_rec_ml_add_path(x1) ->
-   fSTRING x1;
+   fSTRING x1 ++
    fNODE "rec_ml_add_path" 1
 | CT_recaddpath(x1, x2) ->
-   fSTRING x1;
-   fID_OPT x2;
+   fSTRING x1 ++
+   fID_OPT x2 ++
    fNODE "recaddpath" 2
 | CT_record(x1, x2, x3, x4, x5, x6) ->
-   fCOERCION_OPT x1;
-   fID x2;
-   fBINDER_LIST x3;
-   fFORMULA x4;
-   fID_OPT x5;
-   fRECCONSTR_LIST x6;
+   fCOERCION_OPT x1 ++
+   fID x2 ++
+   fBINDER_LIST x3 ++
+   fFORMULA x4 ++
+   fID_OPT x5 ++
+   fRECCONSTR_LIST x6 ++
    fNODE "record" 6
 | CT_remove_natural_feature(x1, x2) ->
-   fNATURAL_FEATURE x1;
-   fID x2;
+   fNATURAL_FEATURE x1 ++
+   fID x2 ++
    fNODE "remove_natural_feature" 2
 | CT_require(x1, x2, x3) ->
-   fIMPEXP x1;
-   fSPEC_OPT x2;
-   fID_NE_LIST_OR_STRING x3;
+   fIMPEXP x1 ++
+   fSPEC_OPT x2 ++
+   fID_NE_LIST_OR_STRING x3 ++
    fNODE "require" 3
 | CT_reserve(x1, x2) ->
-   fID_NE_LIST x1;
-   fFORMULA x2;
+   fID_NE_LIST x1 ++
+   fFORMULA x2 ++
    fNODE "reserve" 2
 | CT_reserve_notation(x1, x2) ->
-   fSTRING x1;
-   fMODIFIER_LIST x2;
+   fSTRING x1 ++
+   fMODIFIER_LIST x2 ++
    fNODE "reserve_notation" 2
 | CT_reset(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "reset" 1
 | CT_reset_section(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "reset_section" 1
 | CT_restart -> fNODE "restart" 0
 | CT_restore_state(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "restore_state" 1
 | CT_resume(x1) ->
-   fID_OPT x1;
+   fID_OPT x1 ++
    fNODE "resume" 1
 | CT_save(x1, x2) ->
-   fTHM_OPT x1;
-   fID_OPT x2;
+   fTHM_OPT x1 ++
+   fID_OPT x2 ++
    fNODE "save" 2
 | CT_scomments(x1) ->
-   fSCOMMENT_CONTENT_LIST x1;
+   fSCOMMENT_CONTENT_LIST x1 ++
    fNODE "scomments" 1
 | CT_search(x1, x2) ->
-   fID x1;
-   fIN_OR_OUT_MODULES x2;
+   fID x1 ++
+   fIN_OR_OUT_MODULES x2 ++
    fNODE "search" 2
 | CT_search_about(x1, x2) ->
-   fID_OR_STRING_NE_LIST x1;
-   fIN_OR_OUT_MODULES x2;
+   fID_OR_STRING_NE_LIST x1 ++
+   fIN_OR_OUT_MODULES x2 ++
    fNODE "search_about" 2
 | CT_search_pattern(x1, x2) ->
-   fFORMULA x1;
-   fIN_OR_OUT_MODULES x2;
+   fFORMULA x1 ++
+   fIN_OR_OUT_MODULES x2 ++
    fNODE "search_pattern" 2
 | CT_search_rewrite(x1, x2) ->
-   fFORMULA x1;
-   fIN_OR_OUT_MODULES x2;
+   fFORMULA x1 ++
+   fIN_OR_OUT_MODULES x2 ++
    fNODE "search_rewrite" 2
 | CT_section_end(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "section_end" 1
 | CT_section_struct(x1, x2, x3) ->
-   fSECTION_BEGIN x1;
-   fSECTION_BODY x2;
-   fCOMMAND x3;
+   fSECTION_BEGIN x1 ++
+   fSECTION_BODY x2 ++
+   fCOMMAND x3 ++
    fNODE "section_struct" 3
 | CT_set_natural(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "set_natural" 1
 | CT_set_natural_default -> fNODE "set_natural_default" 0
 | CT_set_option(x1) ->
-   fTABLE x1;
+   fTABLE x1 ++
    fNODE "set_option" 1
 | CT_set_option_value(x1, x2) ->
-   fTABLE x1;
-   fSINGLE_OPTION_VALUE x2;
+   fTABLE x1 ++
+   fSINGLE_OPTION_VALUE x2 ++
    fNODE "set_option_value" 2
 | CT_set_option_value2(x1, x2) ->
-   fTABLE x1;
-   fID_OR_STRING_NE_LIST x2;
+   fTABLE x1 ++
+   fID_OR_STRING_NE_LIST x2 ++
    fNODE "set_option_value2" 2
 | CT_sethyp(x1) ->
-   fINT x1;
+   fINT x1 ++
    fNODE "sethyp" 1
 | CT_setundo(x1) ->
-   fINT x1;
+   fINT x1 ++
    fNODE "setundo" 1
 | CT_show_existentials -> fNODE "show_existentials" 0
 | CT_show_goal(x1) ->
-   fINT_OPT x1;
+   fINT_OPT x1 ++
    fNODE "show_goal" 1
 | CT_show_implicit(x1) ->
-   fINT x1;
+   fINT x1 ++
    fNODE "show_implicit" 1
 | CT_show_intro -> fNODE "show_intro" 0
 | CT_show_intros -> fNODE "show_intros" 0
@@ -587,97 +589,103 @@ and fCOMMAND = function
 | CT_show_script -> fNODE "show_script" 0
 | CT_show_tree -> fNODE "show_tree" 0
 | CT_solve(x1, x2, x3) ->
-   fINT x1;
-   fTACTIC_COM x2;
-   fDOTDOT_OPT x3;
+   fINT x1 ++
+   fTACTIC_COM x2 ++
+   fDOTDOT_OPT x3 ++
    fNODE "solve" 3
+| CT_strategy(CT_level_list x1) ->
+   List.fold_left (++) (mt())
+     (List.map (fun(l,q) -> fLEVEL l ++ fID_LIST q ++ fNODE "pair"2) x1) ++
+   fNODE "strategy" (List.length x1)
 | CT_suspend -> fNODE "suspend" 0
 | CT_syntax_macro(x1, x2, x3) ->
-   fID x1;
-   fFORMULA x2;
-   fINT_OPT x3;
+   fID x1 ++
+   fFORMULA x2 ++
+   fINT_OPT x3 ++
    fNODE "syntax_macro" 3
 | CT_tactic_definition(x1) ->
-   fTAC_DEF_NE_LIST x1;
+   fTAC_DEF_NE_LIST x1 ++
    fNODE "tactic_definition" 1
 | CT_test_natural_feature(x1, x2) ->
-   fNATURAL_FEATURE x1;
-   fID x2;
+   fNATURAL_FEATURE x1 ++
+   fID x2 ++
    fNODE "test_natural_feature" 2
 | CT_theorem_struct(x1, x2) ->
-   fTHEOREM_GOAL x1;
-   fPROOF_SCRIPT x2;
+   fTHEOREM_GOAL x1 ++
+   fPROOF_SCRIPT x2 ++
    fNODE "theorem_struct" 2
 | CT_time(x1) ->
-   fCOMMAND x1;
+   fCOMMAND x1 ++
    fNODE "time" 1
-| CT_transparent(x1) ->
-   fID_NE_LIST x1;
-   fNODE "transparent" 1
 | CT_undo(x1) ->
-   fINT_OPT x1;
+   fINT_OPT x1 ++
    fNODE "undo" 1
 | CT_unfocus -> fNODE "unfocus" 0
 | CT_unset_option(x1) ->
-   fTABLE x1;
+   fTABLE x1 ++
    fNODE "unset_option" 1
 | CT_unsethyp -> fNODE "unsethyp" 0
 | CT_unsetundo -> fNODE "unsetundo" 0
 | CT_user_vernac(x1, x2) ->
-   fID x1;
-   fVARG_LIST x2;
+   fID x1 ++
+   fVARG_LIST x2 ++
    fNODE "user_vernac" 2
 | CT_variable(x1, x2) ->
-   fVAR x1;
-   fBINDER_NE_LIST x2;
+   fVAR x1 ++
+   fBINDER_NE_LIST x2 ++
    fNODE "variable" 2
 | CT_write_module(x1, x2) ->
-   fID x1;
-   fSTRING_OPT x2;
+   fID x1 ++
+   fSTRING_OPT x2 ++
    fNODE "write_module" 2
+and fLEVEL = function
+| CT_Opaque -> fNODE "opaque" 0
+| CT_Level n -> fINT n ++ fNODE "level" 1
+| CT_Expand -> fNODE "expand" 0
 and fCOMMAND_LIST = function
 | CT_command_list(x,l) ->
-   fCOMMAND x;
-   (List.iter fCOMMAND l);
+   fCOMMAND x ++
+   (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++
    fNODE "command_list" (1 + (List.length l))
 and fCOMMENT = function
-| CT_comment x -> fATOM "comment";
-   (f_atom_string x);
-   print_string "\n"and fCOMMENT_S = function
+| CT_comment x -> fATOM "comment" ++
+   (f_atom_string x) ++
+   str "\n"
+and fCOMMENT_S = function
 | CT_comment_s l ->
-   (List.iter fCOMMENT l);
+   (List.fold_left (++) (mt()) (List.map fCOMMENT l)) ++
    fNODE "comment_s" (List.length l)
 and fCONSTR = function
 | CT_constr(x1, x2) ->
-   fID x1;
-   fFORMULA x2;
+   fID x1 ++
+   fFORMULA x2 ++
    fNODE "constr" 2
 | CT_constr_coercion(x1, x2) ->
-   fID x1;
-   fFORMULA x2;
+   fID x1 ++
+   fFORMULA x2 ++
    fNODE "constr_coercion" 2
 and fCONSTR_LIST = function
 | CT_constr_list l ->
-   (List.iter fCONSTR l);
+   (List.fold_left (++) (mt()) (List.map fCONSTR l)) ++
    fNODE "constr_list" (List.length l)
 and fCONTEXT_HYP_LIST = function
 | CT_context_hyp_list l ->
-   (List.iter fPREMISE_PATTERN l);
+   (List.fold_left (++) (mt()) (List.map fPREMISE_PATTERN l)) ++
    fNODE "context_hyp_list" (List.length l)
 and fCONTEXT_PATTERN = function
 | CT_coerce_FORMULA_to_CONTEXT_PATTERN x -> fFORMULA x
 | CT_context(x1, x2) ->
-   fID_OPT x1;
-   fFORMULA x2;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
    fNODE "context" 2
 and fCONTEXT_RULE = function
 | CT_context_rule(x1, x2, x3) ->
-   fCONTEXT_HYP_LIST x1;
-   fCONTEXT_PATTERN x2;
-   fTACTIC_COM x3;
+   fCONTEXT_HYP_LIST x1 ++
+   fCONTEXT_PATTERN x2 ++
+   fTACTIC_COM x3 ++
    fNODE "context_rule" 3
 | CT_def_context_rule(x1) ->
-   fTACTIC_COM x1;
+   fTACTIC_COM x1 ++
    fNODE "def_context_rule" 1
 and fCONVERSION_FLAG = function
 | CT_beta -> fNODE "beta" 0
@@ -687,49 +695,52 @@ and fCONVERSION_FLAG = function
 | CT_zeta -> fNODE "zeta" 0
 and fCONVERSION_FLAG_LIST = function
 | CT_conversion_flag_list l ->
-   (List.iter fCONVERSION_FLAG l);
+   (List.fold_left (++) (mt()) (List.map fCONVERSION_FLAG l)) ++
    fNODE "conversion_flag_list" (List.length l)
 and fCONV_SET = function
 | CT_unf l ->
-   (List.iter fID l);
+   (List.fold_left (++) (mt()) (List.map fID l)) ++
    fNODE "unf" (List.length l)
 | CT_unfbut l ->
-   (List.iter fID l);
+   (List.fold_left (++) (mt()) (List.map fID l)) ++
    fNODE "unfbut" (List.length l)
 and fCO_IND = function
-| CT_co_ind x -> fATOM "co_ind";
-   (f_atom_string x);
-   print_string "\n"and fDECL_NOTATION_OPT = function
+| CT_co_ind x -> fATOM "co_ind" ++
+   (f_atom_string x) ++
+   str "\n"
+and fDECL_NOTATION_OPT = function
 | CT_coerce_NONE_to_DECL_NOTATION_OPT x -> fNONE x
 | CT_decl_notation(x1, x2, x3) ->
-   fSTRING x1;
-   fFORMULA x2;
-   fID_OPT x3;
+   fSTRING x1 ++
+   fFORMULA x2 ++
+   fID_OPT x3 ++
    fNODE "decl_notation" 3
 and fDEF = function
 | CT_def(x1, x2) ->
-   fID_OPT x1;
-   fFORMULA x2;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
    fNODE "def" 2
 and fDEFN = function
-| CT_defn x -> fATOM "defn";
-   (f_atom_string x);
-   print_string "\n"and fDEFN_OR_THM = function
+| CT_defn x -> fATOM "defn" ++
+   (f_atom_string x) ++
+   str "\n"
+and fDEFN_OR_THM = function
 | CT_coerce_DEFN_to_DEFN_OR_THM x -> fDEFN x
 | CT_coerce_THM_to_DEFN_OR_THM x -> fTHM x
 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
 | CT_type_of(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "type_of" 1
 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);
-   print_string "\n"and fDESTRUCTING = function
+| CT_dep x -> fATOM "dep" ++
+   (f_atom_string x) ++
+   str "\n"
+and fDESTRUCTING = function
 | CT_coerce_NONE_to_DESTRUCTING x -> fNONE x
 | CT_destructing -> fNODE "destructing" 0
 and fDESTRUCT_LOCATION = function
@@ -741,54 +752,54 @@ and fDOTDOT_OPT = function
 | CT_dotdot -> fNODE "dotdot" 0
 and fEQN = function
 | CT_eqn(x1, x2) ->
-   fMATCH_PATTERN_NE_LIST x1;
-   fFORMULA x2;
+   fMATCH_PATTERN_NE_LIST x1 ++
+   fFORMULA x2 ++
    fNODE "eqn" 2
 and fEQN_LIST = function
 | CT_eqn_list l ->
-   (List.iter fEQN l);
+   (List.fold_left (++) (mt()) (List.map fEQN l)) ++
    fNODE "eqn_list" (List.length l)
 and fEVAL_CMD = function
 | CT_eval(x1, x2, x3) ->
-   fINT_OPT x1;
-   fRED_COM x2;
-   fFORMULA x3;
+   fINT_OPT x1 ++
+   fRED_COM x2 ++
+   fFORMULA x3 ++
    fNODE "eval" 3
 and fFIXTAC = function
 | CT_fixtac(x1, x2, x3) ->
-   fID x1;
-   fINT x2;
-   fFORMULA x3;
+   fID x1 ++
+   fINT x2 ++
+   fFORMULA x3 ++
    fNODE "fixtac" 3
 and fFIX_BINDER = function
 | CT_coerce_FIX_REC_to_FIX_BINDER x -> fFIX_REC x
 | CT_fix_binder(x1, x2, x3, x4) ->
-   fID x1;
-   fINT x2;
-   fFORMULA x3;
-   fFORMULA x4;
+   fID x1 ++
+   fINT x2 ++
+   fFORMULA x3 ++
+   fFORMULA x4 ++
    fNODE "fix_binder" 4
 and fFIX_BINDER_LIST = function
 | CT_fix_binder_list(x,l) ->
-   fFIX_BINDER x;
-   (List.iter fFIX_BINDER l);
+   fFIX_BINDER x ++
+   (List.fold_left (++) (mt()) (List.map fFIX_BINDER l)) ++
    fNODE "fix_binder_list" (1 + (List.length l))
 and fFIX_REC = function
 | CT_fix_rec(x1, x2, x3, x4, x5) ->
-   fID x1;
-   fBINDER_NE_LIST x2;
-   fID_OPT x3;
-   fFORMULA x4;
-   fFORMULA x5;
+   fID x1 ++
+   fBINDER_NE_LIST x2 ++
+   fID_OPT x3 ++
+   fFORMULA x4 ++
+   fFORMULA x5 ++
    fNODE "fix_rec" 5
 and fFIX_REC_LIST = function
 | CT_fix_rec_list(x,l) ->
-   fFIX_REC x;
-   (List.iter fFIX_REC l);
+   fFIX_REC x ++
+   (List.fold_left (++) (mt()) (List.map fFIX_REC l)) ++
    fNODE "fix_rec_list" (1 + (List.length l))
 and fFIX_TAC_LIST = function
 | CT_fix_tac_list l ->
-   (List.iter fFIXTAC l);
+   (List.fold_left (++) (mt()) (List.map fFIXTAC l)) ++
    fNODE "fix_tac_list" (List.length l)
 and fFORMULA = function
 | CT_coerce_BINARY_to_FORMULA x -> fBINARY x
@@ -797,90 +808,90 @@ and fFORMULA = function
 | CT_coerce_SORT_TYPE_to_FORMULA x -> fSORT_TYPE x
 | CT_coerce_TYPED_FORMULA_to_FORMULA x -> fTYPED_FORMULA x
 | CT_appc(x1, x2) ->
-   fFORMULA x1;
-   fFORMULA_NE_LIST x2;
+   fFORMULA x1 ++
+   fFORMULA_NE_LIST x2 ++
    fNODE "appc" 2
 | CT_arrowc(x1, x2) ->
-   fFORMULA x1;
-   fFORMULA x2;
+   fFORMULA x1 ++
+   fFORMULA x2 ++
    fNODE "arrowc" 2
 | CT_bang(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "bang" 1
 | CT_cases(x1, x2, x3) ->
-   fMATCHED_FORMULA_NE_LIST x1;
-   fFORMULA_OPT x2;
-   fEQN_LIST x3;
+   fMATCHED_FORMULA_NE_LIST x1 ++
+   fFORMULA_OPT x2 ++
+   fEQN_LIST x3 ++
    fNODE "cases" 3
 | CT_cofixc(x1, x2) ->
-   fID x1;
-   fCOFIX_REC_LIST x2;
+   fID x1 ++
+   fCOFIX_REC_LIST x2 ++
    fNODE "cofixc" 2
 | CT_elimc(x1, x2, x3, x4) ->
-   fCASE x1;
-   fFORMULA_OPT x2;
-   fFORMULA x3;
-   fFORMULA_LIST x4;
+   fCASE x1 ++
+   fFORMULA_OPT x2 ++
+   fFORMULA x3 ++
+   fFORMULA_LIST x4 ++
    fNODE "elimc" 4
 | CT_existvarc -> fNODE "existvarc" 0
 | CT_fixc(x1, x2) ->
-   fID x1;
-   fFIX_BINDER_LIST x2;
+   fID x1 ++
+   fFIX_BINDER_LIST x2 ++
    fNODE "fixc" 2
 | CT_if(x1, x2, x3, x4) ->
-   fFORMULA x1;
-   fRETURN_INFO x2;
-   fFORMULA x3;
-   fFORMULA x4;
+   fFORMULA x1 ++
+   fRETURN_INFO x2 ++
+   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;
+   fFORMULA_OPT x1 ++
+   fID_OPT_NE_LIST x2 ++
+   fFORMULA x3 ++
+   fFORMULA x4 ++
    fNODE "inductive_let" 4
 | CT_labelled_arg(x1, x2) ->
-   fID x1;
-   fFORMULA x2;
+   fID x1 ++
+   fFORMULA x2 ++
    fNODE "labelled_arg" 2
 | CT_lambdac(x1, x2) ->
-   fBINDER_NE_LIST x1;
-   fFORMULA x2;
+   fBINDER_NE_LIST x1 ++
+   fFORMULA x2 ++
    fNODE "lambdac" 2
 | CT_let_tuple(x1, x2, x3, x4) ->
-   fID_OPT_NE_LIST x1;
-   fRETURN_INFO x2;
-   fFORMULA x3;
-   fFORMULA x4;
+   fID_OPT_NE_LIST x1 ++
+   fRETURN_INFO x2 ++
+   fFORMULA x3 ++
+   fFORMULA x4 ++
    fNODE "let_tuple" 4
 | CT_letin(x1, x2) ->
-   fDEF x1;
-   fFORMULA x2;
+   fDEF x1 ++
+   fFORMULA x2 ++
    fNODE "letin" 2
 | CT_notation(x1, x2) ->
-   fSTRING x1;
-   fFORMULA_LIST x2;
+   fSTRING x1 ++
+   fFORMULA_LIST x2 ++
    fNODE "notation" 2
 | CT_num_encapsulator(x1, x2) ->
-   fNUM_TYPE x1;
-   fFORMULA x2;
+   fNUM_TYPE x1 ++
+   fFORMULA x2 ++
    fNODE "num_encapsulator" 2
 | CT_prodc(x1, x2) ->
-   fBINDER_NE_LIST x1;
-   fFORMULA x2;
+   fBINDER_NE_LIST x1 ++
+   fFORMULA x2 ++
    fNODE "prodc" 2
 | CT_proj(x1, x2) ->
-   fFORMULA x1;
-   fFORMULA_NE_LIST x2;
+   fFORMULA x1 ++
+   fFORMULA_NE_LIST x2 ++
    fNODE "proj" 2
 and fFORMULA_LIST = function
 | CT_formula_list l ->
-   (List.iter fFORMULA l);
+   (List.fold_left (++) (mt()) (List.map fFORMULA l)) ++
    fNODE "formula_list" (List.length l)
 and fFORMULA_NE_LIST = function
 | CT_formula_ne_list(x,l) ->
-   fFORMULA x;
-   (List.iter fFORMULA l);
+   fFORMULA x ++
+   (List.fold_left (++) (mt()) (List.map fFORMULA l)) ++
    fNODE "formula_ne_list" (1 + (List.length l))
 and fFORMULA_OPT = function
 | CT_coerce_FORMULA_to_FORMULA_OPT x -> fFORMULA x
@@ -893,44 +904,46 @@ and fGRAMMAR = function
 and fHYP_LOCATION = function
 | CT_coerce_UNFOLD_to_HYP_LOCATION x -> fUNFOLD x
 | CT_intype(x1, x2) ->
-   fID x1;
-   fINT_LIST x2;
+   fID x1 ++
+   fINT_LIST x2 ++
    fNODE "intype" 2
 | CT_invalue(x1, x2) ->
-   fID x1;
-   fINT_LIST x2;
+   fID x1 ++
+   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);
+   (List.fold_left (++) (mt()) (List.map fHYP_LOCATION l)) ++
    fNODE "hyp_location_list" (List.length l)
 and fID = function
-| CT_ident x -> fATOM "ident";
-   (f_atom_string x);
-   print_string "\n"| CT_metac(x1) ->
-   fINT x1;
+| CT_ident x -> fATOM "ident" ++
+   (f_atom_string x) ++
+   str "\n"
+| CT_metac(x1) ->
+   fINT x1 ++
    fNODE "metac" 1
-| CT_metaid x -> fATOM "metaid";
-   (f_atom_string x);
-   print_string "\n"and fIDENTITY_OPT = function
+| CT_metaid x -> fATOM "metaid" ++
+   (f_atom_string x) ++
+   str "\n"
+and fIDENTITY_OPT = function
 | CT_coerce_NONE_to_IDENTITY_OPT x -> fNONE x
 | CT_identity -> fNODE "identity" 0
 and fID_LIST = function
 | CT_id_list l ->
-   (List.iter fID l);
+   (List.fold_left (++) (mt()) (List.map fID l)) ++
    fNODE "id_list" (List.length l)
 and fID_LIST_LIST = function
 | CT_id_list_list l ->
-   (List.iter fID_LIST l);
+   (List.fold_left (++) (mt()) (List.map fID_LIST l)) ++
    fNODE "id_list_list" (List.length l)
 and fID_LIST_OPT = function
 | CT_coerce_ID_LIST_to_ID_LIST_OPT x -> fID_LIST x
 | CT_coerce_NONE_to_ID_LIST_OPT x -> fNONE x
 and fID_NE_LIST = function
 | CT_id_ne_list(x,l) ->
-   fID x;
-   (List.iter fID l);
+   fID x ++
+   (List.fold_left (++) (mt()) (List.map fID l)) ++
    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
@@ -943,12 +956,12 @@ and fID_OPT = function
 | CT_coerce_NONE_to_ID_OPT x -> fNONE x
 and fID_OPT_LIST = function
 | CT_id_opt_list l ->
-   (List.iter fID_OPT l);
+   (List.fold_left (++) (mt()) (List.map fID_OPT l)) ++
    fNODE "id_opt_list" (List.length l)
 and fID_OPT_NE_LIST = function
 | CT_id_opt_ne_list(x,l) ->
-   fID_OPT x;
-   (List.iter fID_OPT l);
+   fID_OPT x ++
+   (List.fold_left (++) (mt()) (List.map fID_OPT l)) ++
    fNODE "id_opt_ne_list" (1 + (List.length l))
 and fID_OPT_OR_ALL = function
 | CT_coerce_ID_OPT_to_ID_OPT_OR_ALL x -> fID_OPT x
@@ -968,8 +981,8 @@ and fID_OR_STRING = function
 | CT_coerce_STRING_to_ID_OR_STRING x -> fSTRING x
 and fID_OR_STRING_NE_LIST = function
 | CT_id_or_string_ne_list(x,l) ->
-   fID_OR_STRING x;
-   (List.iter fID_OR_STRING l);
+   fID_OR_STRING x ++
+   (List.fold_left (++) (mt()) (List.map fID_OR_STRING l)) ++
    fNODE "id_or_string_ne_list" (1 + (List.length l))
 and fIMPEXP = function
 | CT_coerce_NONE_to_IMPEXP x -> fNONE x
@@ -977,40 +990,41 @@ and fIMPEXP = function
 | CT_import -> fNODE "import" 0
 and fIND_SPEC = function
 | CT_ind_spec(x1, x2, x3, x4, x5) ->
-   fID x1;
-   fBINDER_LIST x2;
-   fFORMULA x3;
-   fCONSTR_LIST x4;
-   fDECL_NOTATION_OPT x5;
+   fID x1 ++
+   fBINDER_LIST x2 ++
+   fFORMULA x3 ++
+   fCONSTR_LIST x4 ++
+   fDECL_NOTATION_OPT x5 ++
    fNODE "ind_spec" 5
 and fIND_SPEC_LIST = function
 | CT_ind_spec_list l ->
-   (List.iter fIND_SPEC l);
+   (List.fold_left (++) (mt()) (List.map fIND_SPEC l)) ++
    fNODE "ind_spec_list" (List.length l)
 and fINT = function
-| CT_int x -> fATOM "int";
-   (f_atom_int x);
-   print_string "\n"and fINTRO_PATT = function
+| CT_int x -> fATOM "int" ++
+   (f_atom_int x) ++
+   str "\n"
+and fINTRO_PATT = function
 | CT_coerce_ID_to_INTRO_PATT x -> fID x
 | CT_disj_pattern(x,l) ->
-   fINTRO_PATT_LIST x;
-   (List.iter fINTRO_PATT_LIST l);
+   fINTRO_PATT_LIST x ++
+   (List.fold_left (++) (mt()) (List.map fINTRO_PATT_LIST l)) ++
    fNODE "disj_pattern" (1 + (List.length l))
 and fINTRO_PATT_LIST = function
 | CT_intro_patt_list l ->
-   (List.iter fINTRO_PATT l);
+   (List.fold_left (++) (mt()) (List.map fINTRO_PATT l)) ++
    fNODE "intro_patt_list" (List.length l)
 and fINTRO_PATT_OPT = function
 | CT_coerce_ID_OPT_to_INTRO_PATT_OPT x -> fID_OPT x
 | CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT x -> fINTRO_PATT x
 and fINT_LIST = function
 | CT_int_list l ->
-   (List.iter fINT l);
+   (List.fold_left (++) (mt()) (List.map fINT l)) ++
    fNODE "int_list" (List.length l)
 and fINT_NE_LIST = function
 | CT_int_ne_list(x,l) ->
-   fINT x;
-   (List.iter fINT l);
+   fINT x ++
+   (List.fold_left (++) (mt()) (List.map fINT l)) ++
    fNODE "int_ne_list" (1 + (List.length l))
 and fINT_OPT = function
 | CT_coerce_INT_to_INT_OPT x -> fINT x
@@ -1028,21 +1042,21 @@ and fINV_TYPE = function
 and fIN_OR_OUT_MODULES = function
 | CT_coerce_NONE_to_IN_OR_OUT_MODULES x -> fNONE x
 | CT_in_modules(x1) ->
-   fID_NE_LIST x1;
+   fID_NE_LIST x1 ++
    fNODE "in_modules" 1
 | CT_out_modules(x1) ->
-   fID_NE_LIST x1;
+   fID_NE_LIST x1 ++
    fNODE "out_modules" 1
 and fLET_CLAUSE = function
 | CT_let_clause(x1, x2, x3) ->
-   fID x1;
-   fTACTIC_OPT x2;
-   fLET_VALUE x3;
+   fID x1 ++
+   fTACTIC_OPT x2 ++
+   fLET_VALUE x3 ++
    fNODE "let_clause" 3
 and fLET_CLAUSES = function
 | CT_let_clauses(x,l) ->
-   fLET_CLAUSE x;
-   (List.iter fLET_CLAUSE l);
+   fLET_CLAUSE x ++
+   (List.fold_left (++) (mt()) (List.map fLET_CLAUSE l)) ++
    fNODE "let_clauses" (1 + (List.length l))
 and fLET_VALUE = function
 | CT_coerce_DEF_BODY_to_LET_VALUE x -> fDEF_BODY x
@@ -1051,120 +1065,121 @@ and fLOCAL_OPT = function
 | CT_coerce_NONE_to_LOCAL_OPT x -> fNONE x
 | CT_local -> fNODE "local" 0
 and fLOCN = function
-| CT_locn x -> fATOM "locn";
-   (f_atom_string x);
-   print_string "\n"and fMATCHED_FORMULA = function
+| CT_locn x -> fATOM "locn" ++
+   (f_atom_string x) ++
+   str "\n"
+and fMATCHED_FORMULA = function
 | CT_coerce_FORMULA_to_MATCHED_FORMULA x -> fFORMULA x
 | CT_formula_as(x1, x2) ->
-   fFORMULA x1;
-   fID_OPT x2;
+   fFORMULA x1 ++
+   fID_OPT x2 ++
    fNODE "formula_as" 2
 | CT_formula_as_in(x1, x2, x3) ->
-   fFORMULA x1;
-   fID_OPT x2;
-   fFORMULA x3;
+   fFORMULA x1 ++
+   fID_OPT x2 ++
+   fFORMULA x3 ++
    fNODE "formula_as_in" 3
 | CT_formula_in(x1, x2) ->
-   fFORMULA x1;
-   fFORMULA 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);
+   fMATCHED_FORMULA x ++
+   (List.fold_left (++) (mt()) (List.map 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_coerce_NUM_to_MATCH_PATTERN x -> fNUM x
 | CT_pattern_app(x1, x2) ->
-   fMATCH_PATTERN x1;
-   fMATCH_PATTERN_NE_LIST x2;
+   fMATCH_PATTERN x1 ++
+   fMATCH_PATTERN_NE_LIST x2 ++
    fNODE "pattern_app" 2
 | CT_pattern_as(x1, x2) ->
-   fMATCH_PATTERN x1;
-   fID_OPT x2;
+   fMATCH_PATTERN x1 ++
+   fID_OPT x2 ++
    fNODE "pattern_as" 2
 | CT_pattern_delimitors(x1, x2) ->
-   fNUM_TYPE x1;
-   fMATCH_PATTERN x2;
+   fNUM_TYPE x1 ++
+   fMATCH_PATTERN x2 ++
    fNODE "pattern_delimitors" 2
 | CT_pattern_notation(x1, x2) ->
-   fSTRING x1;
-   fMATCH_PATTERN_LIST x2;
+   fSTRING x1 ++
+   fMATCH_PATTERN_LIST x2 ++
    fNODE "pattern_notation" 2
 and fMATCH_PATTERN_LIST = function
 | CT_match_pattern_list l ->
-   (List.iter fMATCH_PATTERN l);
+   (List.fold_left (++) (mt()) (List.map fMATCH_PATTERN l)) ++
    fNODE "match_pattern_list" (List.length l)
 and fMATCH_PATTERN_NE_LIST = function
 | CT_match_pattern_ne_list(x,l) ->
-   fMATCH_PATTERN x;
-   (List.iter fMATCH_PATTERN l);
+   fMATCH_PATTERN x ++
+   (List.fold_left (++) (mt()) (List.map fMATCH_PATTERN l)) ++
    fNODE "match_pattern_ne_list" (1 + (List.length l))
 and fMATCH_TAC_RULE = function
 | CT_match_tac_rule(x1, x2) ->
-   fCONTEXT_PATTERN x1;
-   fLET_VALUE x2;
+   fCONTEXT_PATTERN x1 ++
+   fLET_VALUE x2 ++
    fNODE "match_tac_rule" 2
 and fMATCH_TAC_RULES = function
 | CT_match_tac_rules(x,l) ->
-   fMATCH_TAC_RULE x;
-   (List.iter fMATCH_TAC_RULE l);
+   fMATCH_TAC_RULE x ++
+   (List.fold_left (++) (mt()) (List.map fMATCH_TAC_RULE l)) ++
    fNODE "match_tac_rules" (1 + (List.length l))
 and fMODIFIER = function
 | CT_entry_type(x1, x2) ->
-   fID x1;
-   fID x2;
+   fID x1 ++
+   fID x2 ++
    fNODE "entry_type" 2
 | CT_format(x1) ->
-   fSTRING x1;
+   fSTRING x1 ++
    fNODE "format" 1
 | CT_lefta -> fNODE "lefta" 0
 | CT_nona -> fNODE "nona" 0
 | CT_only_parsing -> fNODE "only_parsing" 0
 | CT_righta -> fNODE "righta" 0
 | CT_set_item_level(x1, x2) ->
-   fID_NE_LIST x1;
-   fINT_OR_NEXT x2;
+   fID_NE_LIST x1 ++
+   fINT_OR_NEXT x2 ++
    fNODE "set_item_level" 2
 | CT_set_level(x1) ->
-   fINT x1;
+   fINT x1 ++
    fNODE "set_level" 1
 and fMODIFIER_LIST = function
 | CT_modifier_list l ->
-   (List.iter fMODIFIER l);
+   (List.fold_left (++) (mt()) (List.map fMODIFIER l)) ++
    fNODE "modifier_list" (List.length l)
 and fMODULE_BINDER = function
 | CT_module_binder(x1, x2) ->
-   fID_NE_LIST x1;
-   fMODULE_TYPE x2;
+   fID_NE_LIST x1 ++
+   fMODULE_TYPE x2 ++
    fNODE "module_binder" 2
 and fMODULE_BINDER_LIST = function
 | CT_module_binder_list l ->
-   (List.iter fMODULE_BINDER l);
+   (List.fold_left (++) (mt()) (List.map fMODULE_BINDER l)) ++
    fNODE "module_binder_list" (List.length l)
 and fMODULE_EXPR = function
 | CT_coerce_ID_OPT_to_MODULE_EXPR x -> fID_OPT x
 | CT_module_app(x1, x2) ->
-   fMODULE_EXPR x1;
-   fMODULE_EXPR x2;
+   fMODULE_EXPR x1 ++
+   fMODULE_EXPR x2 ++
    fNODE "module_app" 2
 and fMODULE_TYPE = function
 | CT_coerce_ID_to_MODULE_TYPE x -> fID x
 | CT_module_type_with_def(x1, x2, x3) ->
-   fMODULE_TYPE x1;
-   fID_LIST x2;
-   fFORMULA x3;
+   fMODULE_TYPE x1 ++
+   fID_LIST x2 ++
+   fFORMULA x3 ++
    fNODE "module_type_with_def" 3
 | CT_module_type_with_mod(x1, x2, x3) ->
-   fMODULE_TYPE x1;
-   fID_LIST x2;
-   fID x3;
+   fMODULE_TYPE x1 ++
+   fID_LIST x2 ++
+   fID x3 ++
    fNODE "module_type_with_mod" 3
 and fMODULE_TYPE_CHECK = function
 | CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK x -> fMODULE_TYPE_OPT x
 | CT_only_check(x1) ->
-   fMODULE_TYPE x1;
+   fMODULE_TYPE x1 ++
    fNODE "only_check" 1
 and fMODULE_TYPE_OPT = function
 | CT_coerce_ID_OPT_to_MODULE_TYPE_OPT x -> fID_OPT x
@@ -1176,12 +1191,14 @@ and fNATURAL_FEATURE = function
 and fNONE = function
 | CT_none -> fNODE "none" 0
 and fNUM = function
-| CT_int_encapsulator x -> fATOM "int_encapsulator";
-   (f_atom_string x);
-   print_string "\n"and fNUM_TYPE = function
-| CT_num_type x -> fATOM "num_type";
-   (f_atom_string x);
-   print_string "\n"and fOMEGA_FEATURE = function
+| CT_int_encapsulator x -> fATOM "int_encapsulator" ++
+   (f_atom_string x) ++
+   str "\n"
+and fNUM_TYPE = function
+| CT_num_type x -> fATOM "num_type" ++
+   (f_atom_string x) ++
+   str "\n"
+and fOMEGA_FEATURE = function
 | CT_coerce_STRING_to_OMEGA_FEATURE x -> fSTRING x
 | CT_flag_action -> fNODE "flag_action" 0
 | CT_flag_system -> fNODE "flag_system" 0
@@ -1195,13 +1212,13 @@ and fORIENTATION = function
 | CT_rl -> fNODE "rl" 0
 and fPATTERN = function
 | CT_pattern_occ(x1, x2) ->
-   fINT_LIST x1;
-   fFORMULA x2;
+   fINT_LIST x1 ++
+   fFORMULA x2 ++
    fNODE "pattern_occ" 2
 and fPATTERN_NE_LIST = function
 | CT_pattern_ne_list(x,l) ->
-   fPATTERN x;
-   (List.iter fPATTERN l);
+   fPATTERN x ++
+   (List.fold_left (++) (mt()) (List.map fPATTERN l)) ++
    fNODE "pattern_ne_list" (1 + (List.length l))
 and fPATTERN_OPT = function
 | CT_coerce_NONE_to_PATTERN_OPT x -> fNONE x
@@ -1209,146 +1226,147 @@ and fPATTERN_OPT = function
 and fPREMISE = function
 | CT_coerce_TYPED_FORMULA_to_PREMISE x -> fTYPED_FORMULA x
 | CT_eval_result(x1, x2, x3) ->
-   fFORMULA x1;
-   fFORMULA x2;
-   fFORMULA x3;
+   fFORMULA x1 ++
+   fFORMULA x2 ++
+   fFORMULA x3 ++
    fNODE "eval_result" 3
 | CT_premise(x1, x2) ->
-   fID x1;
-   fFORMULA x2;
+   fID x1 ++
+   fFORMULA x2 ++
    fNODE "premise" 2
 and fPREMISES_LIST = function
 | CT_premises_list l ->
-   (List.iter fPREMISE l);
+   (List.fold_left (++) (mt()) (List.map fPREMISE l)) ++
    fNODE "premises_list" (List.length l)
 and fPREMISE_PATTERN = function
 | CT_premise_pattern(x1, x2) ->
-   fID_OPT x1;
-   fCONTEXT_PATTERN x2;
+   fID_OPT x1 ++
+   fCONTEXT_PATTERN x2 ++
    fNODE "premise_pattern" 2
 and fPROOF_SCRIPT = function
 | CT_proof_script l ->
-   (List.iter fCOMMAND l);
+   (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++
    fNODE "proof_script" (List.length l)
 and fRECCONSTR = function
 | CT_defrecconstr(x1, x2, x3) ->
-   fID_OPT x1;
-   fFORMULA x2;
-   fFORMULA_OPT x3;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
+   fFORMULA_OPT x3 ++
    fNODE "defrecconstr" 3
 | CT_defrecconstr_coercion(x1, x2, x3) ->
-   fID_OPT x1;
-   fFORMULA x2;
-   fFORMULA_OPT x3;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
+   fFORMULA_OPT x3 ++
    fNODE "defrecconstr_coercion" 3
 | CT_recconstr(x1, x2) ->
-   fID_OPT x1;
-   fFORMULA x2;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
    fNODE "recconstr" 2
 | CT_recconstr_coercion(x1, x2) ->
-   fID_OPT x1;
-   fFORMULA x2;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
    fNODE "recconstr_coercion" 2
 and fRECCONSTR_LIST = function
 | CT_recconstr_list l ->
-   (List.iter fRECCONSTR l);
+   (List.fold_left (++) (mt()) (List.map fRECCONSTR l)) ++
    fNODE "recconstr_list" (List.length l)
 and fREC_TACTIC_FUN = function
 | CT_rec_tactic_fun(x1, x2, x3) ->
-   fID x1;
-   fID_OPT_NE_LIST x2;
-   fTACTIC_COM x3;
+   fID x1 ++
+   fID_OPT_NE_LIST x2 ++
+   fTACTIC_COM x3 ++
    fNODE "rec_tactic_fun" 3
 and fREC_TACTIC_FUN_LIST = function
 | CT_rec_tactic_fun_list(x,l) ->
-   fREC_TACTIC_FUN x;
-   (List.iter fREC_TACTIC_FUN l);
+   fREC_TACTIC_FUN x ++
+   (List.fold_left (++) (mt()) (List.map fREC_TACTIC_FUN l)) ++
    fNODE "rec_tactic_fun_list" (1 + (List.length l))
 and fRED_COM = function
 | CT_cbv(x1, x2) ->
-   fCONVERSION_FLAG_LIST x1;
-   fCONV_SET x2;
+   fCONVERSION_FLAG_LIST x1 ++
+   fCONV_SET x2 ++
    fNODE "cbv" 2
 | CT_fold(x1) ->
-   fFORMULA_LIST x1;
+   fFORMULA_LIST x1 ++
    fNODE "fold" 1
 | CT_hnf -> fNODE "hnf" 0
 | CT_lazy(x1, x2) ->
-   fCONVERSION_FLAG_LIST x1;
-   fCONV_SET x2;
+   fCONVERSION_FLAG_LIST x1 ++
+   fCONV_SET x2 ++
    fNODE "lazy" 2
 | CT_pattern(x1) ->
-   fPATTERN_NE_LIST x1;
+   fPATTERN_NE_LIST x1 ++
    fNODE "pattern" 1
 | CT_red -> fNODE "red" 0
 | CT_cbvvm -> fNODE "vm_compute" 0
 | CT_simpl(x1) ->
-   fPATTERN_OPT x1;
+   fPATTERN_OPT x1 ++
    fNODE "simpl" 1
 | CT_unfold(x1) ->
-   fUNFOLD_NE_LIST 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;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
    fNODE "as_and_return" 2
 | CT_return(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "return" 1
 and fRULE = function
 | CT_rule(x1, x2) ->
-   fPREMISES_LIST x1;
-   fFORMULA x2;
+   fPREMISES_LIST x1 ++
+   fFORMULA x2 ++
    fNODE "rule" 2
 and fRULE_LIST = function
 | CT_rule_list l ->
-   (List.iter fRULE l);
+   (List.fold_left (++) (mt()) (List.map fRULE l)) ++
    fNODE "rule_list" (List.length l)
 and fSCHEME_SPEC = function
 | CT_scheme_spec(x1, x2, x3, x4) ->
-   fID x1;
-   fDEP x2;
-   fFORMULA x3;
-   fSORT_TYPE x4;
+   fID x1 ++
+   fDEP x2 ++
+   fFORMULA x3 ++
+   fSORT_TYPE x4 ++
    fNODE "scheme_spec" 4
 and fSCHEME_SPEC_LIST = function
 | CT_scheme_spec_list(x,l) ->
-   fSCHEME_SPEC x;
-   (List.iter fSCHEME_SPEC l);
+   fSCHEME_SPEC x ++
+   (List.fold_left (++) (mt()) (List.map fSCHEME_SPEC l)) ++
    fNODE "scheme_spec_list" (1 + (List.length l))
 and fSCOMMENT_CONTENT = function
 | CT_coerce_FORMULA_to_SCOMMENT_CONTENT x -> fFORMULA x
 | CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT x -> fID_OR_STRING x
 and fSCOMMENT_CONTENT_LIST = function
 | CT_scomment_content_list l ->
-   (List.iter fSCOMMENT_CONTENT l);
+   (List.fold_left (++) (mt()) (List.map fSCOMMENT_CONTENT l)) ++
    fNODE "scomment_content_list" (List.length l)
 and fSECTION_BEGIN = function
 | CT_section(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "section" 1
 and fSECTION_BODY = function
 | CT_section_body l ->
-   (List.iter fCOMMAND l);
+   (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++
    fNODE "section_body" (List.length l)
 and fSIGNED_INT = function
 | CT_coerce_INT_to_SIGNED_INT x -> fINT x
 | CT_minus(x1) ->
-   fINT x1;
+   fINT x1 ++
    fNODE "minus" 1
 and fSIGNED_INT_LIST = function
 | CT_signed_int_list l ->
-   (List.iter fSIGNED_INT l);
+   (List.fold_left (++) (mt()) (List.map fSIGNED_INT l)) ++
    fNODE "signed_int_list" (List.length l)
 and fSINGLE_OPTION_VALUE = function
 | CT_coerce_INT_to_SINGLE_OPTION_VALUE x -> fINT x
 | CT_coerce_STRING_to_SINGLE_OPTION_VALUE x -> fSTRING x
 and fSORT_TYPE = function
-| CT_sortc x -> fATOM "sortc";
-   (f_atom_string x);
-   print_string "\n"and fSPEC_LIST = function
+| CT_sortc x -> fATOM "sortc" ++
+   (f_atom_string x) ++
+   str "\n"
+and fSPEC_LIST = function
 | CT_coerce_BINDING_LIST_to_SPEC_LIST x -> fBINDING_LIST x
 | CT_coerce_FORMULA_LIST_to_SPEC_LIST x -> fFORMULA_LIST x
 and fSPEC_OPT = function
@@ -1360,12 +1378,13 @@ 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);
-   print_string "\n"and fSTRING_NE_LIST = function
+| CT_string x -> fATOM "string" ++
+   (f_atom_string x) ++
+   str "\n"
+and fSTRING_NE_LIST = function
 | CT_string_ne_list(x,l) ->
-   fSTRING x;
-   (List.iter fSTRING l);
+   fSTRING x ++
+   (List.fold_left (++) (mt()) (List.map fSTRING l)) ++
    fNODE "string_ne_list" (1 + (List.length l))
 and fSTRING_OPT = function
 | CT_coerce_NONE_to_STRING_OPT x -> fNONE x
@@ -1373,8 +1392,8 @@ and fSTRING_OPT = function
 and fTABLE = function
 | CT_coerce_ID_to_TABLE x -> fID x
 | CT_table(x1, x2) ->
-   fID x1;
-   fID x2;
+   fID x1 ++
+   fID x2 ++
    fNODE "table" 2
 and fTACTIC_ARG = function
 | CT_coerce_EVAL_CMD_to_TACTIC_ARG x -> fEVAL_CMD x
@@ -1384,429 +1403,429 @@ and fTACTIC_ARG = function
 | CT_void -> fNODE "void" 0
 and fTACTIC_ARG_LIST = function
 | CT_tactic_arg_list(x,l) ->
-   fTACTIC_ARG x;
-   (List.iter fTACTIC_ARG l);
+   fTACTIC_ARG x ++
+   (List.fold_left (++) (mt()) (List.map fTACTIC_ARG l)) ++
    fNODE "tactic_arg_list" (1 + (List.length l))
 and fTACTIC_COM = function
 | CT_abstract(x1, x2) ->
-   fID_OPT x1;
-   fTACTIC_COM x2;
+   fID_OPT x1 ++
+   fTACTIC_COM x2 ++
    fNODE "abstract" 2
 | CT_absurd(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "absurd" 1
 | CT_any_constructor(x1) ->
-   fTACTIC_OPT x1;
+   fTACTIC_OPT x1 ++
    fNODE "any_constructor" 1
 | CT_apply(x1, x2) ->
-   fFORMULA x1;
-   fSPEC_LIST x2;
+   fFORMULA x1 ++
+   fSPEC_LIST x2 ++
    fNODE "apply" 2
 | CT_assert(x1, x2) ->
-   fID_OPT x1;
-   fFORMULA x2;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
    fNODE "assert" 2
 | CT_assumption -> fNODE "assumption" 0
 | CT_auto(x1) ->
-   fINT_OPT x1;
+   fINT_OPT x1 ++
    fNODE "auto" 1
 | CT_auto_with(x1, x2) ->
-   fINT_OPT x1;
-   fID_NE_LIST_OR_STAR x2;
+   fINT_OPT x1 ++
+   fID_NE_LIST_OR_STAR x2 ++
    fNODE "auto_with" 2
 | CT_autorewrite(x1, x2) ->
-   fID_NE_LIST x1;
-   fTACTIC_OPT x2;
+   fID_NE_LIST x1 ++
+   fTACTIC_OPT x2 ++
    fNODE "autorewrite" 2
 | CT_autotdb(x1) ->
-   fINT_OPT x1;
+   fINT_OPT x1 ++
    fNODE "autotdb" 1
 | CT_case_type(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "case_type" 1
 | CT_casetac(x1, x2) ->
-   fFORMULA x1;
-   fSPEC_LIST x2;
+   fFORMULA x1 ++
+   fSPEC_LIST x2 ++
    fNODE "casetac" 2
 | CT_cdhyp(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "cdhyp" 1
 | CT_change(x1, x2) ->
-   fFORMULA x1;
-   fCLAUSE x2;
+   fFORMULA x1 ++
+   fCLAUSE x2 ++
    fNODE "change" 2
 | CT_change_local(x1, x2, x3) ->
-   fPATTERN x1;
-   fFORMULA x2;
-   fCLAUSE x3;
+   fPATTERN x1 ++
+   fFORMULA x2 ++
+   fCLAUSE x3 ++
    fNODE "change_local" 3
 | CT_clear(x1) ->
-   fID_NE_LIST x1;
+   fID_NE_LIST x1 ++
    fNODE "clear" 1
 | CT_clear_body(x1) ->
-   fID_NE_LIST x1;
+   fID_NE_LIST x1 ++
    fNODE "clear_body" 1
 | CT_cofixtactic(x1, x2) ->
-   fID_OPT x1;
-   fCOFIX_TAC_LIST x2;
+   fID_OPT x1 ++
+   fCOFIX_TAC_LIST x2 ++
    fNODE "cofixtactic" 2
 | CT_condrewrite_lr(x1, x2, x3, x4) ->
-   fTACTIC_COM x1;
-   fFORMULA x2;
-   fSPEC_LIST x3;
-   fID_OPT x4;
+   fTACTIC_COM x1 ++
+   fFORMULA x2 ++
+   fSPEC_LIST x3 ++
+   fID_OPT x4 ++
    fNODE "condrewrite_lr" 4
 | CT_condrewrite_rl(x1, x2, x3, x4) ->
-   fTACTIC_COM x1;
-   fFORMULA x2;
-   fSPEC_LIST x3;
-   fID_OPT x4;
+   fTACTIC_COM x1 ++
+   fFORMULA x2 ++
+   fSPEC_LIST x3 ++
+   fID_OPT x4 ++
    fNODE "condrewrite_rl" 4
 | CT_constructor(x1, x2) ->
-   fINT x1;
-   fSPEC_LIST x2;
+   fINT x1 ++
+   fSPEC_LIST x2 ++
    fNODE "constructor" 2
 | CT_contradiction -> fNODE "contradiction" 0
 | CT_contradiction_thm(x1, x2) ->
-   fFORMULA x1;
-   fSPEC_LIST x2;
+   fFORMULA x1 ++
+   fSPEC_LIST x2 ++
    fNODE "contradiction_thm" 2
 | CT_cut(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "cut" 1
 | CT_cutrewrite_lr(x1, x2) ->
-   fFORMULA x1;
-   fID_OPT x2;
+   fFORMULA x1 ++
+   fID_OPT x2 ++
    fNODE "cutrewrite_lr" 2
 | CT_cutrewrite_rl(x1, x2) ->
-   fFORMULA x1;
-   fID_OPT x2;
+   fFORMULA x1 ++
+   fID_OPT x2 ++
    fNODE "cutrewrite_rl" 2
 | CT_dauto(x1, x2) ->
-   fINT_OPT x1;
-   fINT_OPT x2;
+   fINT_OPT x1 ++
+   fINT_OPT x2 ++
    fNODE "dauto" 2
 | CT_dconcl -> fNODE "dconcl" 0
 | CT_decompose_list(x1, x2) ->
-   fID_NE_LIST x1;
-   fFORMULA x2;
+   fID_NE_LIST x1 ++
+   fFORMULA x2 ++
    fNODE "decompose_list" 2
 | CT_decompose_record(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "decompose_record" 1
 | CT_decompose_sum(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "decompose_sum" 1
 | CT_depinversion(x1, x2, x3, x4) ->
-   fINV_TYPE x1;
-   fID_OR_INT x2;
-   fINTRO_PATT_OPT x3;
-   fFORMULA_OPT x4;
+   fINV_TYPE x1 ++
+   fID_OR_INT x2 ++
+   fINTRO_PATT_OPT x3 ++
+   fFORMULA_OPT x4 ++
    fNODE "depinversion" 4
 | CT_deprewrite_lr(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "deprewrite_lr" 1
 | CT_deprewrite_rl(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "deprewrite_rl" 1
 | CT_destruct(x1) ->
-   fID_OR_INT x1;
+   fID_OR_INT x1 ++
    fNODE "destruct" 1
 | CT_dhyp(x1) ->
-   fID x1;
+   fID x1 ++
    fNODE "dhyp" 1
 | CT_discriminate_eq(x1) ->
-   fID_OR_INT_OPT x1;
+   fID_OR_INT_OPT x1 ++
    fNODE "discriminate_eq" 1
 | CT_do(x1, x2) ->
-   fID_OR_INT x1;
-   fTACTIC_COM x2;
+   fID_OR_INT x1 ++
+   fTACTIC_COM x2 ++
    fNODE "do" 2
 | CT_eapply(x1, x2) ->
-   fFORMULA x1;
-   fSPEC_LIST x2;
+   fFORMULA x1 ++
+   fSPEC_LIST x2 ++
    fNODE "eapply" 2
 | CT_eauto(x1, x2) ->
-   fID_OR_INT_OPT x1;
-   fID_OR_INT_OPT x2;
+   fID_OR_INT_OPT x1 ++
+   fID_OR_INT_OPT x2 ++
    fNODE "eauto" 2
 | CT_eauto_with(x1, x2, x3) ->
-   fID_OR_INT_OPT x1;
-   fID_OR_INT_OPT x2;
-   fID_NE_LIST_OR_STAR x3;
+   fID_OR_INT_OPT x1 ++
+   fID_OR_INT_OPT x2 ++
+   fID_NE_LIST_OR_STAR x3 ++
    fNODE "eauto_with" 3
 | CT_elim(x1, x2, x3) ->
-   fFORMULA x1;
-   fSPEC_LIST x2;
-   fUSING x3;
+   fFORMULA x1 ++
+   fSPEC_LIST x2 ++
+   fUSING x3 ++
    fNODE "elim" 3
 | CT_elim_type(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "elim_type" 1
 | CT_exact(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "exact" 1
 | CT_exact_no_check(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "exact_no_check" 1
 | CT_vm_cast_no_check(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "vm_cast_no_check" 1
 | CT_exists(x1) ->
-   fSPEC_LIST x1;
+   fSPEC_LIST x1 ++
    fNODE "exists" 1
 | CT_fail(x1, x2) ->
-   fID_OR_INT x1;
-   fSTRING_OPT x2;
+   fID_OR_INT x1 ++
+   fSTRING_OPT x2 ++
    fNODE "fail" 2
 | CT_first(x,l) ->
-   fTACTIC_COM x;
-   (List.iter fTACTIC_COM l);
+   fTACTIC_COM x ++
+   (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
    fNODE "first" (1 + (List.length l))
 | CT_firstorder(x1) ->
-   fTACTIC_OPT x1;
+   fTACTIC_OPT x1 ++
    fNODE "firstorder" 1
 | CT_firstorder_using(x1, x2) ->
-   fTACTIC_OPT x1;
-   fID_NE_LIST x2;
+   fTACTIC_OPT x1 ++
+   fID_NE_LIST x2 ++
    fNODE "firstorder_using" 2
 | CT_firstorder_with(x1, x2) ->
-   fTACTIC_OPT x1;
-   fID_NE_LIST x2;
+   fTACTIC_OPT x1 ++
+   fID_NE_LIST x2 ++
    fNODE "firstorder_with" 2
 | CT_fixtactic(x1, x2, x3) ->
-   fID_OPT x1;
-   fINT x2;
-   fFIX_TAC_LIST x3;
+   fID_OPT x1 ++
+   fINT x2 ++
+   fFIX_TAC_LIST x3 ++
    fNODE "fixtactic" 3
 | CT_formula_marker(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "formula_marker" 1
 | CT_fresh(x1) ->
-   fSTRING_OPT x1;
+   fSTRING_OPT x1 ++
    fNODE "fresh" 1
 | CT_generalize(x1) ->
-   fFORMULA_NE_LIST x1;
+   fFORMULA_NE_LIST x1 ++
    fNODE "generalize" 1
 | CT_generalize_dependent(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "generalize_dependent" 1
 | CT_idtac(x1) ->
-   fSTRING_OPT x1;
+   fSTRING_OPT x1 ++
    fNODE "idtac" 1
 | CT_induction(x1) ->
-   fID_OR_INT x1;
+   fID_OR_INT x1 ++
    fNODE "induction" 1
 | CT_info(x1) ->
-   fTACTIC_COM x1;
+   fTACTIC_COM x1 ++
    fNODE "info" 1
 | CT_injection_eq(x1) ->
-   fID_OR_INT_OPT x1;
+   fID_OR_INT_OPT x1 ++
    fNODE "injection_eq" 1
 | CT_instantiate(x1, x2, x3) ->
-   fINT x1;
-   fFORMULA x2;
-   fCLAUSE x3;
+   fINT x1 ++
+   fFORMULA x2 ++
+   fCLAUSE x3 ++
    fNODE "instantiate" 3
 | CT_intro(x1) ->
-   fID_OPT x1;
+   fID_OPT x1 ++
    fNODE "intro" 1
 | CT_intro_after(x1, x2) ->
-   fID_OPT x1;
-   fID x2;
+   fID_OPT x1 ++
+   fID x2 ++
    fNODE "intro_after" 2
 | CT_intros(x1) ->
-   fINTRO_PATT_LIST x1;
+   fINTRO_PATT_LIST x1 ++
    fNODE "intros" 1
 | CT_intros_until(x1) ->
-   fID_OR_INT x1;
+   fID_OR_INT x1 ++
    fNODE "intros_until" 1
 | CT_inversion(x1, x2, x3, x4) ->
-   fINV_TYPE x1;
-   fID_OR_INT x2;
-   fINTRO_PATT_OPT x3;
-   fID_LIST x4;
+   fINV_TYPE x1 ++
+   fID_OR_INT x2 ++
+   fINTRO_PATT_OPT x3 ++
+   fID_LIST x4 ++
    fNODE "inversion" 4
 | CT_left(x1) ->
-   fSPEC_LIST x1;
+   fSPEC_LIST x1 ++
    fNODE "left" 1
 | CT_let_ltac(x1, x2) ->
-   fLET_CLAUSES x1;
-   fLET_VALUE x2;
+   fLET_CLAUSES x1 ++
+   fLET_VALUE x2 ++
    fNODE "let_ltac" 2
 | CT_lettac(x1, x2, x3) ->
-   fID_OPT x1;
-   fFORMULA x2;
-   fCLAUSE x3;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
+   fCLAUSE x3 ++
    fNODE "lettac" 3
 | CT_match_context(x,l) ->
-   fCONTEXT_RULE x;
-   (List.iter fCONTEXT_RULE l);
+   fCONTEXT_RULE x ++
+   (List.fold_left (++) (mt()) (List.map fCONTEXT_RULE l)) ++
    fNODE "match_context" (1 + (List.length l))
 | CT_match_context_reverse(x,l) ->
-   fCONTEXT_RULE x;
-   (List.iter fCONTEXT_RULE l);
+   fCONTEXT_RULE x ++
+   (List.fold_left (++) (mt()) (List.map fCONTEXT_RULE l)) ++
    fNODE "match_context_reverse" (1 + (List.length l))
 | CT_match_tac(x1, x2) ->
-   fTACTIC_COM x1;
-   fMATCH_TAC_RULES x2;
+   fTACTIC_COM x1 ++
+   fMATCH_TAC_RULES x2 ++
    fNODE "match_tac" 2
 | CT_move_after(x1, x2) ->
-   fID x1;
-   fID x2;
+   fID x1 ++
+   fID x2 ++
    fNODE "move_after" 2
 | CT_new_destruct(x1, x2, x3) ->
-   (List.iter fFORMULA_OR_INT x1); (* Julien F. Est-ce correct? *)
-   fUSING x2;
-   fINTRO_PATT_OPT x3;
+   (List.fold_left (++) (mt()) (List.map fFORMULA_OR_INT x1)) ++ (* Julien F. Est-ce correct? *)
+   fUSING x2 ++
+   fINTRO_PATT_OPT x3 ++
    fNODE "new_destruct" 3
 | CT_new_induction(x1, x2, x3) ->
-   (List.iter fFORMULA_OR_INT x1); (* Pierre C. Est-ce correct? *)
-   fUSING x2;
-   fINTRO_PATT_OPT x3;
+   (List.fold_left (++) (mt()) (List.map fFORMULA_OR_INT x1)) ++ (* Pierre C. Est-ce correct? *)
+   fUSING x2 ++
+   fINTRO_PATT_OPT x3 ++
    fNODE "new_induction" 3
 | CT_omega -> fNODE "omega" 0
 | CT_orelse(x1, x2) ->
-   fTACTIC_COM x1;
-   fTACTIC_COM x2;
+   fTACTIC_COM x1 ++
+   fTACTIC_COM x2 ++
    fNODE "orelse" 2
 | CT_parallel(x,l) ->
-   fTACTIC_COM x;
-   (List.iter fTACTIC_COM l);
+   fTACTIC_COM x ++
+   (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
    fNODE "parallel" (1 + (List.length l))
 | CT_pose(x1, x2) ->
-   fID_OPT x1;
-   fFORMULA x2;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
    fNODE "pose" 2
 | CT_progress(x1) ->
-   fTACTIC_COM x1;
+   fTACTIC_COM x1 ++
    fNODE "progress" 1
 | CT_prolog(x1, x2) ->
-   fFORMULA_LIST x1;
-   fINT x2;
+   fFORMULA_LIST x1 ++
+   fINT x2 ++
    fNODE "prolog" 2
 | CT_rec_tactic_in(x1, x2) ->
-   fREC_TACTIC_FUN_LIST x1;
-   fTACTIC_COM x2;
+   fREC_TACTIC_FUN_LIST x1 ++
+   fTACTIC_COM x2 ++
    fNODE "rec_tactic_in" 2
 | CT_reduce(x1, x2) ->
-   fRED_COM x1;
-   fCLAUSE x2;
+   fRED_COM x1 ++
+   fCLAUSE x2 ++
    fNODE "reduce" 2
 | CT_refine(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "refine" 1
 | CT_reflexivity -> fNODE "reflexivity" 0
 | CT_rename(x1, x2) ->
-   fID x1;
-   fID x2;
+   fID x1 ++
+   fID x2 ++
    fNODE "rename" 2
 | CT_repeat(x1) ->
-   fTACTIC_COM x1;
+   fTACTIC_COM x1 ++
    fNODE "repeat" 1
 | CT_replace_with(x1, x2,x3,x4) ->
-   fFORMULA x1;
-   fFORMULA x2;
-   fCLAUSE x3;
-   fTACTIC_OPT x4;
+   fFORMULA x1 ++
+   fFORMULA x2 ++
+   fCLAUSE x3 ++
+   fTACTIC_OPT x4 ++
    fNODE "replace_with" 4
 | CT_rewrite_lr(x1, x2, x3) ->
-   fFORMULA x1;
-   fSPEC_LIST x2;
-   fCLAUSE x3;
+   fFORMULA x1 ++
+   fSPEC_LIST x2 ++
+   fCLAUSE x3 ++
    fNODE "rewrite_lr" 3
 | CT_rewrite_rl(x1, x2, x3) ->
-   fFORMULA x1;
-   fSPEC_LIST x2;
-   fCLAUSE x3;
+   fFORMULA x1 ++
+   fSPEC_LIST x2 ++
+   fCLAUSE x3 ++
    fNODE "rewrite_rl" 3
 | CT_right(x1) ->
-   fSPEC_LIST x1;
+   fSPEC_LIST x1 ++
    fNODE "right" 1
 | CT_ring(x1) ->
-   fFORMULA_LIST x1;
+   fFORMULA_LIST x1 ++
    fNODE "ring" 1
 | CT_simple_user_tac(x1, x2) ->
-   fID x1;
-   fTACTIC_ARG_LIST x2;
+   fID x1 ++
+   fTACTIC_ARG_LIST x2 ++
    fNODE "simple_user_tac" 2
 | CT_simplify_eq(x1) ->
-   fID_OR_INT_OPT x1;
+   fID_OR_INT_OPT x1 ++
    fNODE "simplify_eq" 1
 | CT_specialize(x1, x2, x3) ->
-   fINT_OPT x1;
-   fFORMULA x2;
-   fSPEC_LIST x3;
+   fINT_OPT x1 ++
+   fFORMULA x2 ++
+   fSPEC_LIST x3 ++
    fNODE "specialize" 3
 | CT_split(x1) ->
-   fSPEC_LIST x1;
+   fSPEC_LIST x1 ++
    fNODE "split" 1
 | CT_subst(x1) ->
-   fID_LIST x1;
+   fID_LIST x1 ++
    fNODE "subst" 1
 | CT_superauto(x1, x2, x3, x4) ->
-   fINT_OPT x1;
-   fID_LIST x2;
-   fDESTRUCTING x3;
-   fUSINGTDB x4;
+   fINT_OPT x1 ++
+   fID_LIST x2 ++
+   fDESTRUCTING x3 ++
+   fUSINGTDB x4 ++
    fNODE "superauto" 4
 | CT_symmetry(x1) ->
-   fCLAUSE x1;
+   fCLAUSE x1 ++
    fNODE "symmetry" 1
 | CT_tac_double(x1, x2) ->
-   fID_OR_INT x1;
-   fID_OR_INT x2;
+   fID_OR_INT x1 ++
+   fID_OR_INT x2 ++
    fNODE "tac_double" 2
 | CT_tacsolve(x,l) ->
-   fTACTIC_COM x;
-   (List.iter fTACTIC_COM l);
+   fTACTIC_COM x ++
+   (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
    fNODE "tacsolve" (1 + (List.length l))
 | CT_tactic_fun(x1, x2) ->
-   fID_OPT_NE_LIST x1;
-   fTACTIC_COM x2;
+   fID_OPT_NE_LIST x1 ++
+   fTACTIC_COM x2 ++
    fNODE "tactic_fun" 2
 | CT_then(x,l) ->
-   fTACTIC_COM x;
-   (List.iter fTACTIC_COM l);
+   fTACTIC_COM x ++
+   (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
    fNODE "then" (1 + (List.length l))
 | CT_transitivity(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "transitivity" 1
 | CT_trivial -> fNODE "trivial" 0
 | CT_trivial_with(x1) ->
-   fID_NE_LIST_OR_STAR x1;
+   fID_NE_LIST_OR_STAR x1 ++
    fNODE "trivial_with" 1
 | CT_truecut(x1, x2) ->
-   fID_OPT x1;
-   fFORMULA x2;
+   fID_OPT x1 ++
+   fFORMULA x2 ++
    fNODE "truecut" 2
 | CT_try(x1) ->
-   fTACTIC_COM x1;
+   fTACTIC_COM x1 ++
    fNODE "try" 1
 | CT_use(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "use" 1
 | CT_use_inversion(x1, x2, x3) ->
-   fID_OR_INT x1;
-   fFORMULA x2;
-   fID_LIST x3;
+   fID_OR_INT x1 ++
+   fFORMULA x2 ++
+   fID_LIST x3 ++
    fNODE "use_inversion" 3
 | CT_user_tac(x1, x2) ->
-   fID x1;
-   fTARG_LIST x2;
+   fID x1 ++
+   fTARG_LIST x2 ++
    fNODE "user_tac" 2
 and fTACTIC_OPT = function
 | CT_coerce_NONE_to_TACTIC_OPT x -> fNONE x
 | CT_coerce_TACTIC_COM_to_TACTIC_OPT x -> fTACTIC_COM x
 and fTAC_DEF = function
 | CT_tac_def(x1, x2) ->
-   fID x1;
-   fTACTIC_COM x2;
+   fID x1 ++
+   fTACTIC_COM x2 ++
    fNODE "tac_def" 2
 and fTAC_DEF_NE_LIST = function
 | CT_tac_def_ne_list(x,l) ->
-   fTAC_DEF x;
-   (List.iter fTAC_DEF l);
+   fTAC_DEF x ++
+   (List.fold_left (++) (mt()) (List.map fTAC_DEF l)) ++
    fNODE "tac_def_ne_list" (1 + (List.length l))
 and fTARG = function
 | CT_coerce_BINDING_to_TARG x -> fBINDING x
@@ -1824,81 +1843,83 @@ and fTARG = function
 | CT_coerce_UNFOLD_NE_LIST_to_TARG x -> fUNFOLD_NE_LIST x
 and fTARG_LIST = function
 | CT_targ_list l ->
-   (List.iter fTARG l);
+   (List.fold_left (++) (mt()) (List.map fTARG l)) ++
    fNODE "targ_list" (List.length l)
 and fTERM_CHANGE = function
 | CT_check_term(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "check_term" 1
 | CT_inst_term(x1, x2) ->
-   fID x1;
-   fFORMULA x2;
+   fID x1 ++
+   fFORMULA x2 ++
    fNODE "inst_term" 2
 and fTEXT = function
 | CT_coerce_ID_to_TEXT x -> fID x
 | CT_text_formula(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "text_formula" 1
 | CT_text_h l ->
-   (List.iter fTEXT l);
+   (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
    fNODE "text_h" (List.length l)
 | CT_text_hv l ->
-   (List.iter fTEXT l);
+   (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
    fNODE "text_hv" (List.length l)
 | CT_text_op l ->
-   (List.iter fTEXT l);
+   (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
    fNODE "text_op" (List.length l)
 | CT_text_path(x1) ->
-   fSIGNED_INT_LIST x1;
+   fSIGNED_INT_LIST x1 ++
    fNODE "text_path" 1
 | CT_text_v l ->
-   (List.iter fTEXT l);
+   (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
    fNODE "text_v" (List.length l)
 and fTHEOREM_GOAL = function
 | CT_goal(x1) ->
-   fFORMULA x1;
+   fFORMULA x1 ++
    fNODE "goal" 1
 | CT_theorem_goal(x1, x2, x3, x4) ->
-   fDEFN_OR_THM x1;
-   fID x2;
-   fBINDER_LIST x3;
-   fFORMULA x4;
+   fDEFN_OR_THM x1 ++
+   fID x2 ++
+   fBINDER_LIST x3 ++
+   fFORMULA x4 ++
    fNODE "theorem_goal" 4
 and fTHM = function
-| CT_thm x -> fATOM "thm";
-   (f_atom_string x);
-   print_string "\n"and fTHM_OPT = function
+| CT_thm x -> fATOM "thm" ++
+   (f_atom_string x) ++
+   str "\n"
+and fTHM_OPT = function
 | CT_coerce_NONE_to_THM_OPT x -> fNONE x
 | CT_coerce_THM_to_THM_OPT x -> fTHM x
 and fTYPED_FORMULA = function
 | CT_typed_formula(x1, x2) ->
-   fFORMULA x1;
-   fFORMULA x2;
+   fFORMULA x1 ++
+   fFORMULA x2 ++
    fNODE "typed_formula" 2
 and fUNFOLD = function
 | CT_coerce_ID_to_UNFOLD x -> fID x
 | CT_unfold_occ(x1, x2) ->
-   fID x1;
-   fINT_NE_LIST x2;
+   fID x1 ++
+   fINT_NE_LIST x2 ++
    fNODE "unfold_occ" 2
 and fUNFOLD_NE_LIST = function
 | CT_unfold_ne_list(x,l) ->
-   fUNFOLD x;
-   (List.iter fUNFOLD l);
+   fUNFOLD x ++
+   (List.fold_left (++) (mt()) (List.map fUNFOLD l)) ++
    fNODE "unfold_ne_list" (1 + (List.length l))
 and fUSING = function
 | CT_coerce_NONE_to_USING x -> fNONE x
 | CT_using(x1, x2) ->
-   fFORMULA x1;
-   fSPEC_LIST x2;
+   fFORMULA x1 ++
+   fSPEC_LIST x2 ++
    fNODE "using" 2
 and fUSINGTDB = function
 | CT_coerce_NONE_to_USINGTDB x -> fNONE x
 | CT_usingtdb -> fNODE "usingtdb" 0
 and fVAR = function
-| CT_var x -> fATOM "var";
-   (f_atom_string x);
-   print_string "\n"and fVARG = function
+| CT_var x -> fATOM "var" ++
+   (f_atom_string x) ++
+   str "\n"
+and fVARG = function
 | CT_coerce_AST_to_VARG x -> fAST x
 | CT_coerce_AST_LIST_to_VARG x -> fAST_LIST x
 | CT_coerce_BINDER_to_VARG x -> fBINDER x
@@ -1916,7 +1937,7 @@ and fVAR = function
 | CT_coerce_VARG_LIST_to_VARG x -> fVARG_LIST x
 and fVARG_LIST = function
 | CT_varg_list l ->
-   (List.iter fVARG l);
+   (List.fold_left (++) (mt()) (List.map fVARG l)) ++
    fNODE "varg_list" (List.length l)
 and fVERBOSE_OPT = function
 | CT_coerce_NONE_to_VERBOSE_OPT x -> fNONE x
diff --git a/contrib/interface/vtp.mli b/contrib/interface/vtp.mli
index fe30b317..d7bd8db5 100644
--- a/contrib/interface/vtp.mli
+++ b/contrib/interface/vtp.mli
@@ -1,15 +1,16 @@
 open Ascent;;
+open Pp;;
 
-val fCOMMAND_LIST : ct_COMMAND_LIST -> unit;;
-val fCOMMAND : ct_COMMAND -> unit;;
-val fTACTIC_COM : ct_TACTIC_COM -> unit;;
-val fFORMULA : ct_FORMULA -> unit;;
-val fID : ct_ID -> unit;;
-val fSTRING : ct_STRING -> unit;;
-val fINT : ct_INT -> unit;;
-val fRULE_LIST : ct_RULE_LIST -> unit;;
-val fRULE : ct_RULE -> unit;;
-val fSIGNED_INT_LIST : ct_SIGNED_INT_LIST -> unit;;
-val fPREMISES_LIST : ct_PREMISES_LIST -> unit;;
-val fID_LIST : ct_ID_LIST -> unit;;
-val fTEXT : ct_TEXT -> unit;;
\ No newline at end of file
+val fCOMMAND_LIST : ct_COMMAND_LIST -> std_ppcmds;;
+val fCOMMAND : ct_COMMAND -> std_ppcmds;;
+val fTACTIC_COM : ct_TACTIC_COM -> std_ppcmds;;
+val fFORMULA : ct_FORMULA -> std_ppcmds;;
+val fID : ct_ID -> std_ppcmds;;
+val fSTRING : ct_STRING -> std_ppcmds;;
+val fINT : ct_INT -> std_ppcmds;;
+val fRULE_LIST : ct_RULE_LIST -> std_ppcmds;;
+val fRULE : ct_RULE -> std_ppcmds;;
+val fSIGNED_INT_LIST : ct_SIGNED_INT_LIST -> std_ppcmds;;
+val fPREMISES_LIST : ct_PREMISES_LIST -> std_ppcmds;;
+val fID_LIST : ct_ID_LIST -> std_ppcmds;;
+val fTEXT : ct_TEXT -> std_ppcmds;;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index df03a579..7d1f57fe 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -15,12 +15,6 @@ open Libnames;;
 open Goptions;;
 
 
-let in_coq_ref = ref false;;
-
-let declare_in_coq () = in_coq_ref:=true;;
-
-let in_coq () = !in_coq_ref;;
-
 (* // Verify whether this is dead code, as of coq version 7 *)
 (* The following three sentences have been added to cope with a change 
 of strategy from the Coq team in the way rules construct ast's.  The
@@ -203,6 +197,10 @@ let xlate_int_or_var_opt_to_int_opt = function
   | Some (ArgVar _) -> xlate_error "int_or_var: TODO"
   | None ->  CT_coerce_NONE_to_INT_OPT CT_none
 
+let apply_or_by_notation f = function
+  | AN x -> f x
+  | ByNotation _ -> xlate_error "TODO: ByNotation"
+
 let tac_qualid_to_ct_ID ref = 
   CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
 
@@ -307,14 +305,10 @@ let make_fix_struct (n,bl) =
   let names = names_of_local_assums bl in
   let nn = List.length names in
   if nn = 1 || n = None then ctv_ID_OPT_NONE
-  else 
-    let n = out_some n in 
-    if n < nn then xlate_id_opt(List.nth names n)
-    else xlate_error "unexpected result of parsing for Fixpoint";;
-
+  else ctf_ID_OPT_SOME(CT_ident (string_of_id (snd (Option.get n))));;
 
 let rec xlate_binder = function
-    (l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
+    (l,k,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
 and xlate_return_info = function
 | (Some Anonymous, None) | (None, None) ->
    CT_coerce_NONE_to_RETURN_INFO CT_none
@@ -327,7 +321,7 @@ and xlate_formula_opt =
     | Some e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e)
 
 and  xlate_binder_l = function
-    LocalRawAssum(l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
+    LocalRawAssum(l,_,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
   | LocalRawDef(n,v) -> CT_coerce_DEF_to_BINDER(CT_def(xlate_id_opt n,
 						       xlate_formula v))
 and 
@@ -336,7 +330,7 @@ and
   | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a, 
                                      List.map xlate_match_pattern l)
 and  translate_one_equation = function
-    (_,[lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
+    (_,[_,lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
   | _ -> xlate_error "TODO: disjunctive multiple patterns"
 and 
   xlate_binder_ne_list = function
@@ -379,8 +373,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		 (xlate_formula f, List.map xlate_formula_expl l'))
    | CApp(_, (_,f), l) -> 
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
-   | CCases (_, _, [], _) -> assert false
-   | CCases (_, ret_type, tm::tml, eqns)->
+   | CCases (_, _, _, [], _) -> assert false
+   | CCases (_, _, ret_type, tm::tml, eqns)->
        CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
 					   List.map xlate_matched_formula tml),
 		xlate_formula_opt ret_type,
@@ -418,23 +412,16 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
        CT_coerce_ID_to_FORMULA(CT_metaid (string_of_id s))
    | CPatVar (_, (true, s)) ->
        xlate_error "Second order variable not supported"
-   | CEvar (_, _) -> xlate_error "CEvar not supported"
+   | CEvar _ -> xlate_error "CEvar not supported"
    | CCoFix (_, (_, id), lm::lmi) -> 
-     let strip_mutcorec (fid, bl,arf, ardef) =
+     let strip_mutcorec ((_, fid), bl,arf, ardef) =
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
                       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, ro), bl, arf, ardef) =
-        let (struct_arg,bl,arf,ardef) =
-	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
-	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
-         if bl = [] then
-	   let n = out_some n in 
-           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
-           (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
-         else (make_fix_struct (n, bl),bl,arf,ardef) in
+     let strip_mutrec ((_, fid), (n, ro), bl, arf, ardef) =
+        let struct_arg = make_fix_struct (n, bl) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match xlate_binder_list bl with
@@ -461,7 +448,7 @@ and xlate_matched_formula = function
       CT_coerce_FORMULA_to_MATCHED_FORMULA(xlate_formula f)
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
-  | (a, Some (_,ExplByPos i)) -> 
+  | (a, Some (_,ExplByPos (i, _))) -> 
       xlate_error "explicitation of implicit by rank not supported"
   | (a, Some (_,ExplByName i)) ->
       CT_labelled_arg(CT_ident (string_of_id i), xlate_formula a)
@@ -477,24 +464,31 @@ let (xlate_ident_or_metaid:
     AI (_, x) -> xlate_ident x
   | MetaId(_, x) -> CT_metaid x;;
 
+let nums_of_occs (b,nums) =
+  if b then nums
+  else List.map (function ArgArg x -> ArgArg (-x) | y -> y) nums
+
 let xlate_hyp = function
   | AI (_,id) -> xlate_ident id
   | MetaId _ -> xlate_error "MetaId should occur only in quotations"
 
 let xlate_hyp_location =
  function
-  | (nums, AI (_,id)), InHypTypeOnly ->
-      CT_intype(xlate_ident id, nums_or_var_to_int_list nums)
-  | (nums, AI (_,id)), InHypValueOnly ->
-      CT_invalue(xlate_ident id, nums_or_var_to_int_list nums)
-  | ([], AI (_,id)), InHyp ->
+  | (occs, AI (_,id)), InHypTypeOnly ->
+      CT_intype(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
+  | (occs, AI (_,id)), InHypValueOnly ->
+      CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
+  | (occs, AI (_,id)), InHyp when occs = all_occurrences_expr ->
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_coerce_ID_to_UNFOLD (xlate_ident id))
-  | (a::l, AI (_,id)), InHyp ->
+  | ((_,a::l as occs), AI (_,id)), InHyp ->
+      let nums = nums_of_occs occs in
+      let a = List.hd nums and l = List.tl nums in
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_unfold_occ (xlate_ident id, 
 			CT_int_ne_list(num_or_var_to_int a, 
                                        nums_or_var_to_int_list_aux l)))
+  | (_, AI (_,id)), InHyp -> xlate_error "Unused" (* (true,]) *)
   | (_, MetaId _),_ -> 
       xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
 
@@ -507,7 +501,7 @@ let xlate_clause cls =
       | Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in
   CT_clause
     (hyps_info, 
-     if cls.onconcl then 
+     if cls.concl_occs <> no_occurrences_expr then 
        CT_coerce_STAR_to_STAR_OPT CT_star
      else
        CT_coerce_NONE_to_STAR_OPT CT_none)
@@ -606,14 +600,15 @@ let strip_targ_intropatt =
     | _ -> xlate_error "strip_targ_intropatt";;
 
 let get_flag r =
-  let conv_flags, red_ids = 
+  let conv_flags, red_ids =
+    let csts = List.map (apply_or_by_notation tac_qualid_to_ct_ID) r.rConst in
     if r.rDelta then
-      [CT_delta], CT_unfbut (List.map tac_qualid_to_ct_ID r.rConst)
+      [CT_delta], CT_unfbut csts
     else
       (if r.rConst = []
       then (* probably useless: just for compatibility *) []
       else [CT_delta]),
-      CT_unf (List.map tac_qualid_to_ct_ID r.rConst) in
+      CT_unf csts in
   let conv_flags = if r.rBeta then CT_beta::conv_flags else conv_flags in
   let conv_flags = if r.rIota then CT_iota::conv_flags else conv_flags in
   let conv_flags = if r.rZeta then CT_zeta::conv_flags else conv_flags in
@@ -633,6 +628,8 @@ let rec xlate_intro_pattern =
   | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
   | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
+  | IntroFresh _ -> xlate_error "TODO: IntroFresh"
+  | IntroRewrite _ -> xlate_error "TODO: IntroRewrite"
 
 let compute_INV_TYPE = function
    FullInversionClear -> CT_inv_clear
@@ -663,7 +660,8 @@ let xlate_largs_to_id_opt largs =
     | _ -> assert false;;
 
 let xlate_int_or_constr = function
-    ElimOnConstr a -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a)
+    ElimOnConstr (a,NoBindings) -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a)
+  | ElimOnConstr _ -> xlate_error "TODO: ElimOnConstr with bindings"
   | ElimOnIdent(_,i) ->
       CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
       	(CT_coerce_ID_to_ID_OR_INT(xlate_ident i))
@@ -676,9 +674,13 @@ let xlate_using = function
   | Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);;
 
 let xlate_one_unfold_block = function
-    ([],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_or_var_to_int_ne_list n nums)
+    ((true,[]),qid) -> 
+      CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid)
+  | (((_,_::_) as occs), qid) ->
+      let l = nums_of_occs occs in
+      CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid, 
+                    nums_or_var_to_int_ne_list (List.hd l) (List.tl l))
+  | ((false,[]), qid) -> xlate_error "Unused"
 ;;
 
 let xlate_with_names = function
@@ -739,7 +741,8 @@ and xlate_red_tactic =
   | CbvVm -> CT_cbvvm
   | Hnf -> CT_hnf
   | Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
-  | Simpl (Some (l,c)) -> 
+  | Simpl (Some (occs,c)) -> 
+      let l = nums_of_occs occs in
       CT_simpl 
 	(CT_coerce_PATTERN_to_PATTERN_OPT
 	   (CT_pattern_occ
@@ -758,9 +761,9 @@ and xlate_red_tactic =
   | Fold formula_list -> 
       CT_fold(CT_formula_list(List.map xlate_formula formula_list))
   | Pattern l ->
-     let pat_list = List.map (fun (nums,c) ->
+     let pat_list = List.map (fun (occs,c) ->
           CT_pattern_occ
-           (CT_int_list (nums_or_var_to_int_list_aux nums),
+           (CT_int_list (nums_or_var_to_int_list_aux (nums_of_occs occs)),
             xlate_formula c)) l in
      (match pat_list with
       | first :: others -> CT_pattern (CT_pattern_ne_list (first, others))
@@ -770,21 +773,23 @@ and xlate_red_tactic =
 and xlate_local_rec_tac = function 
  (* TODO LATER: local recursive tactics and global ones should be handled in
     the same manner *)
-  | ((_,x),(argl,tac)) ->
+  | ((_,x),Tacexp (TacFun (argl,tac))) ->
       let fst, rest = xlate_largs_to_id_opt argl in
 	CT_rec_tactic_fun(xlate_ident x,
 			  CT_id_opt_ne_list(fst, rest),
 			  xlate_tactic tac)
+  | _ -> xlate_error "TODO: more general argument of 'let rec in'"
 
 and xlate_tactic =
  function
    | TacFun (largs, t) ->
        let fst, rest =  xlate_largs_to_id_opt largs in
        CT_tactic_fun (CT_id_opt_ne_list(fst, rest), xlate_tactic t)
-   | TacThen (t1,t2) -> 
+   | TacThen (t1,[||],t2,[||]) -> 
        (match xlate_tactic t1 with
             CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2])
 	  | t -> CT_then (t,[xlate_tactic t2]))
+   | TacThen _ -> xlate_error "TacThen generalization TODO"
    | TacThens(t1,[]) -> assert false
    | TacThens(t1,t::l) ->
        let ct = xlate_tactic t in
@@ -831,36 +836,31 @@ and xlate_tactic =
    | TacMatchContext (false,true,rule1::rules) ->
          CT_match_context_reverse(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
-   | TacLetIn (l, t) ->
+   | TacLetIn (false, l, t) ->
        let cvt_clause =
          function
-             ((_,s),None,ConstrMayEval v) ->
+             ((_,s),ConstrMayEval v) ->
                  CT_let_clause(xlate_ident s,
 			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_DEF_BODY_to_LET_VALUE
                                (formula_to_def_body v))
-           | ((_,s),None,Tacexp t) -> 
+           | ((_,s),Tacexp t) -> 
                  CT_let_clause(xlate_ident s,
 			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
                                (xlate_tactic t))
-           | ((_,s),None,t) -> 
+           | ((_,s),t) -> 
                  CT_let_clause(xlate_ident s,
 			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
-                               (xlate_call_or_tacarg t))
-           | ((_,s),Some c,t) -> 
-	       CT_let_clause(xlate_ident s,
-			     CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic c),
-                               CT_coerce_TACTIC_COM_to_LET_VALUE
-				 (xlate_call_or_tacarg t)) in
+                               (xlate_call_or_tacarg t)) in
          let cl_l = List.map cvt_clause l in
          (match cl_l with
             | [] -> assert false 
             | fst::others ->
                 CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t))
-   | TacLetRecIn([], _) -> xlate_error "recursive definition with no definition"
-   | TacLetRecIn(f1::l, t) -> 
+   | TacLetIn(true, [], _) -> xlate_error "recursive definition with no definition"
+   | TacLetIn(true, 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)
@@ -917,6 +917,7 @@ and xlate_tac =
     | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
     | TacChange (Some(l,c), f, b) -> 
 	(* TODO LATER: combine with other constructions of pattern_occ *)
+	let l = nums_of_occs l in
 	CT_change_local(
 	  CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l), 
 			 xlate_formula c),
@@ -946,18 +947,22 @@ and xlate_tac =
 	xlate_error "TODO: injection as"
     | TacFix (idopt, n) ->
      CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list [])
-    | TacMutualFix (id, n, fixtac_list) ->
+    | TacMutualFix (false, id, n, fixtac_list) ->
      let f (id,n,c) = CT_fixtac (xlate_ident id, CT_int n, xlate_formula c) in
      CT_fixtactic
       (ctf_ID_OPT_SOME (xlate_ident id), CT_int n,
       CT_fix_tac_list (List.map f fixtac_list))
+    | TacMutualFix (true, id, n, fixtac_list) ->
+        xlate_error "TODO: non user-visible fix"
     | TacCofix idopt ->
        CT_cofixtactic (xlate_ident_opt idopt, CT_cofix_tac_list [])
-    | TacMutualCofix (id, cofixtac_list) ->
+    | TacMutualCofix (false, id, cofixtac_list) ->
      let f (id,c) = CT_cofixtac (xlate_ident id, xlate_formula c) in
      CT_cofixtactic
       (CT_coerce_ID_to_ID_OPT (xlate_ident id),
       CT_cofix_tac_list (List.map f cofixtac_list))
+    | TacMutualCofix (true, id, cofixtac_list) ->
+        xlate_error "TODO: non user-visible cofix"
     | TacIntrosUntil (NamedHyp id) -> 
 	CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
     | TacIntrosUntil (AnonHyp n) -> 
@@ -975,10 +980,12 @@ and xlate_tac =
     | TacIntroMove (Some id, None) ->
      CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
     | TacIntroMove (None, None) ->  CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
-    | TacLeft bindl -> CT_left (xlate_bindings bindl)
-    | TacRight bindl -> CT_right (xlate_bindings bindl)
-    | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl)
-    | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
+    | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl)
+    | TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
+    | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl)
+    | TacSplit (false,true,bindl) -> CT_exists (xlate_bindings bindl)
+    | TacSplit _ | TacRight _ | TacLeft _ -> 
+	xlate_error "TODO: esplit, eright, etc"
     | TacExtend (_,"replace", [c1; c2;cl;tac_opt]) ->
 	let c1 = xlate_formula (out_gen rawwit_constr c1) in
 	let c2 = xlate_formula (out_gen rawwit_constr c2) in
@@ -991,7 +998,7 @@ and xlate_tac =
 	  let cl_as_xlate_arg = 
 	    {cl_as_clause with 
 	       Tacexpr.onhyps = 
-		option_map 
+		Option.map 
 		  (fun l -> 
 		     List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l
 		  )
@@ -1009,12 +1016,15 @@ and xlate_tac =
 		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
 	in 
 	CT_replace_with (c1, c2,cl,tac_opt)
-    | TacRewrite(b,cbindl,cl) -> 
+    | TacRewrite(false,[b,Precisely 1,cbindl],cl,None) -> 
      let cl = xlate_clause cl 
      and c = xlate_formula (fst cbindl) 
      and bindl = xlate_bindings (snd cbindl) in
      if b then CT_rewrite_lr (c, bindl, cl)
      else CT_rewrite_rl (c, bindl, cl)
+    | TacRewrite(_,_,_,Some _) -> xlate_error "TODO: rewrite by"
+    | TacRewrite(false,_,cl,_) -> xlate_error "TODO: rewrite of several hyps at once"
+    | TacRewrite(true,_,cl,_) -> xlate_error "TODO: erewrite"
     | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
      let t = out_gen rawwit_main_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
@@ -1127,10 +1137,9 @@ and xlate_tac =
       (match out_gen rawwit_int_or_var n with
 	| ArgVar _ -> xlate_error ""
 	| ArgArg n -> CT_prolog (CT_formula_list cl, CT_int  n))
-    | TacExtend (_,"eapply", [cbindl]) ->
-     let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
-     let c = xlate_formula c and bindl = xlate_bindings bindl in
-     CT_eapply (c, bindl)
+    (* eapply now represented by TacApply (true,cbindl) 
+    | TacExtend (_,"eapply", [cbindl]) -> 
+*)
     | TacTrivial ([],Some []) -> CT_trivial
     | TacTrivial ([],None) -> 
 	CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
@@ -1141,25 +1150,36 @@ and xlate_tac =
 	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
-    | TacApply (c,bindl) ->
+    | TacApply (true,false,(c,bindl)) ->
      CT_apply (xlate_formula c, xlate_bindings bindl)
-    | TacConstructor (n_or_meta, bindl) ->
+    | TacApply (true,true,(c,bindl)) ->
+     CT_eapply (xlate_formula c, xlate_bindings bindl)
+    | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply"
+    | TacConstructor (false,n_or_meta, bindl) ->
 	let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
 	in CT_constructor (CT_int n, xlate_bindings bindl)
+    | TacConstructor _ -> xlate_error "TODO: econstructor"
     | TacSpecialize (nopt, (c,sl)) ->
      CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl)
     | TacGeneralize [] -> xlate_error ""
-    | TacGeneralize (first :: cl) ->
+    | TacGeneralize ((((true,[]),first),Anonymous) :: cl)
+	when List.for_all (fun ((o,_),na) -> o = all_occurrences_expr
+	  & na = Anonymous) cl ->
      CT_generalize
-      (CT_formula_ne_list (xlate_formula first, List.map xlate_formula cl))
+      (CT_formula_ne_list (xlate_formula first, 
+                           List.map (fun ((_,c),_) -> xlate_formula c) cl))
+    | TacGeneralize _ -> xlate_error "TODO: Generalize at and as"
     | TacGeneralizeDep c ->
 	CT_generalize_dependent (xlate_formula c)
     | TacElimType c -> CT_elim_type (xlate_formula c)
     | TacCaseType c -> CT_case_type (xlate_formula c)
-    | TacElim ((c1,sl), u) ->
+    | TacElim (false,(c1,sl), u) ->
      CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u)
-    | TacCase (c1,sl) ->
+    | TacCase (false,(c1,sl)) ->
      CT_casetac (xlate_formula c1, xlate_bindings sl)
+    | TacElim (true,_,_) | TacCase (true,_)
+    | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) ->
+	xlate_error "TODO: eelim, ecase, edestruct, einduction"
     | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
     | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
     | TacCut c -> CT_cut (xlate_formula c)
@@ -1167,8 +1187,8 @@ and xlate_tac =
     | TacDecompose ([],c) ->
 	xlate_error "Decompose : empty list of identifiers?"
     | TacDecompose (id::l,c) ->
-	let id' = tac_qualid_to_ct_ID id in
-	let l' = List.map tac_qualid_to_ct_ID l in
+	let id' = apply_or_by_notation tac_qualid_to_ct_ID id in
+	let l' = List.map (apply_or_by_notation tac_qualid_to_ct_ID) l in
         CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c)
     | TacDecomposeAnd c -> CT_decompose_record (xlate_formula c)
     | TacDecomposeOr c -> CT_decompose_sum(xlate_formula c)
@@ -1178,6 +1198,7 @@ and xlate_tac =
        let idl' = List.map xlate_hyp idl in
        CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
     | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
+    | TacRevert _ -> xlate_error "TODO: revert"
     | (*For translating tactics/Inv.v *)
       TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
 	CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
@@ -1192,30 +1213,36 @@ and xlate_tac =
 	  CT_use_inversion (id, xlate_formula c,
 	    CT_id_list (List.map xlate_hyp idlist))
     | TacExtend (_,"omega", []) -> CT_omega
-    | TacRename (id1, id2) -> CT_rename(xlate_hyp id1, xlate_hyp id2)
+    | TacRename [id1, id2] -> CT_rename(xlate_hyp id1, xlate_hyp id2)
+    | TacRename _ -> xlate_error "TODO: add support for n-ary rename"
     | TacClearBody([]) -> assert false
     | TacClearBody(a::l) -> 
 	CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
-    | TacDAuto (a, b) ->
+    | TacDAuto (a, b, []) ->
 	CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
-    | TacNewDestruct(a,b,c) ->
-	CT_new_destruct (* Julien F. : est-ce correct *)
+    | TacDAuto (a, b, _) ->
+	xlate_error "TODO: dauto using"
+    | TacNewDestruct(false,a,b,c,None) ->
+	CT_new_destruct
 	  (List.map  xlate_int_or_constr a, xlate_using b, 
 	   xlate_with_names c)
-    | TacNewInduction(a,b,c) ->
-	CT_new_induction (* Pierre C. : est-ce correct *)
+    | TacNewInduction(false,a,b,c,None) ->
+	CT_new_induction
 	  (List.map xlate_int_or_constr a, xlate_using b,
 	   xlate_with_names c)
+    | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in"
+    | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in"
     (*| TacInstantiate (a, b, cl) -> 
         CT_instantiate(CT_int a, xlate_formula b,
 		       assert false) *)
-    | TacLetTac (na, c, cl) when cl = nowhere -> 
+    | TacLetTac (na, c, cl, true) when cl = nowhere -> 
         CT_pose(xlate_id_opt_aux na, xlate_formula c)
-    | TacLetTac (na, c, cl) ->
+    | TacLetTac (na, c, cl, true) ->
         CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
 		     but the structures are different *)
 		  xlate_clause cl)
+    | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
     | TacAssert (None, IntroIdentifier id, c) -> 
         CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
     | TacAssert (None, IntroAnonymous, c) -> 
@@ -1226,16 +1253,18 @@ and xlate_tac =
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
-    | TacAnyConstructor(Some tac) -> 
+    | TacAnyConstructor(false,Some tac) -> 
 	CT_any_constructor
 	(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
-    | TacAnyConstructor(None) -> 
+    | TacAnyConstructor(false,None) -> 
 	CT_any_constructor(CT_coerce_NONE_to_TACTIC_OPT CT_none)
+    | TacAnyConstructor _ -> xlate_error "TODO: econstructor"
     | TacExtend(_, "ring", [args]) -> 
 	CT_ring
 	  (CT_formula_list
 	     (List.map xlate_formula
 		(out_gen (wit_list0 rawwit_constr) args)))
+    | TacExtend (_, "f_equal", _) -> xlate_error "TODO: f_equal"
     | TacExtend (_,id, l) ->
 	print_endline ("Extratactics : "^ id);
      CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
@@ -1299,7 +1328,7 @@ and coerce_genarg_to_TARG x =
 					 (snd (out_gen
 					    (rawwit_open_constr_gen b) x))))
   | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
-      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let n = Option.get (Pcoq.tactic_genarg_level s) in
       let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_COM_to_TARG t
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
@@ -1392,7 +1421,7 @@ let coerce_genarg_to_VARG x =
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
   | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
-      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let n = Option.get (Pcoq.tactic_genarg_level s) in
       let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
   | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
@@ -1563,7 +1592,9 @@ let rec xlate_module_type = function
 	   | CWith_Module((_, idl), (_, qid)) ->
 	       CT_module_type_with_mod(mty1,
 				       CT_id_list (List.map xlate_ident idl), 
-				       CT_ident (xlate_qualid qid)));;
+				       CT_ident (xlate_qualid qid)))
+  | CMTEapply (_,_) -> xlate_error "TODO: Funsig application";;
+
 
 let xlate_module_binder_list (l:module_binder list) =
   CT_module_binder_list
@@ -1596,8 +1627,8 @@ let rec xlate_vernac =
    | VernacDeclareTacticDefinition (true, tacs) ->
        (match List.map 
 	 (function
-	      ((_, id), body) ->
-		CT_tac_def(CT_ident (string_of_id id), xlate_tactic body))
+	      (id, _, body) ->
+		CT_tac_def(reference_to_ct_ID id, xlate_tactic body))
 	 tacs with
 	     [] -> assert false
 	   | fst::tacs1 ->
@@ -1714,7 +1745,7 @@ let rec xlate_vernac =
 		      CT_id_ne_list(n1, names), dblist)
 	| HintsExtern (n, c, t) ->
 	    CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
-        | HintsResolve l | HintsImmediate l -> 
+        | HintsImmediate l -> 
 	 let f1, formulas = match List.map xlate_formula l with
 	     a :: tl -> a, tl
 	   | _  -> failwith "" in
@@ -1731,6 +1762,23 @@ let rec xlate_vernac =
 		  HintsResolve _ -> CT_hints_resolve(l', dblist)
 		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
 		| _ -> assert false)
+        | HintsResolve l -> 
+	 let f1, formulas = match List.map xlate_formula (List.map snd l) with
+	     a :: tl -> a, tl
+	   | _  -> failwith "" in
+	 let l' = CT_formula_ne_list(f1, formulas) in
+	   if local then
+             (match h with 
+		  HintsResolve _ ->
+		    CT_local_hints_resolve(l', dblist)
+	       	| HintsImmediate _ ->
+		    CT_local_hints_immediate(l', dblist)
+	       	| _ -> assert false)
+	   else
+	     (match h with
+		  HintsResolve _ -> CT_hints_resolve(l', dblist)
+		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
+		| _ -> assert false)
         | HintsUnfold l -> 
 	 let n1, names = match List.map loc_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
@@ -1766,13 +1814,11 @@ let rec xlate_vernac =
        ctf_ID_OPT_SOME (xlate_ident s))
   | VernacEndProof Admitted ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Admitted"), ctv_ID_OPT_NONE)
-  | VernacSetOpacity (false, id :: idl) ->
-            CT_transparent(CT_id_ne_list(loc_qualid_to_ct_ID id,
-                   List.map loc_qualid_to_ct_ID idl))
-  | VernacSetOpacity (true, id :: idl)
-            -> CT_opaque (CT_id_ne_list(loc_qualid_to_ct_ID id,
-                   List.map loc_qualid_to_ct_ID idl))
-  | VernacSetOpacity (_, []) -> xlate_error "Shouldn't occur"
+  | VernacSetOpacity (_,l) ->
+      CT_strategy(CT_level_list
+        (List.map (fun (l,q) ->
+          (level_to_ct_LEVEL l,
+           CT_id_list(List.map loc_qualid_to_ct_ID q))) l))
   | VernacUndo n -> CT_undo (CT_coerce_INT_to_INT_OPT (CT_int n))
   | VernacShow (ShowGoal nopt) -> CT_show_goal (xlate_int_opt nopt)
   | VernacShow ShowNode -> CT_show_node
@@ -1799,7 +1845,7 @@ let rec xlate_vernac =
 	| PrintOpaqueName id -> CT_print_opaqueid (loc_qualid_to_ct_ID id)
 	| PrintSectionContext id -> CT_print_section (loc_qualid_to_ct_ID id)
 	| PrintModules -> CT_print_modules
-	| PrintGrammar (phylum, name) -> CT_print_grammar CT_grammar_none
+	| PrintGrammar name -> CT_print_grammar CT_grammar_none
 	| PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star)
 	| PrintHintDbName id -> 
 	    CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id))
@@ -1819,6 +1865,12 @@ let rec xlate_vernac =
 	    CT_print_path (xlate_class id1, xlate_class id2)
 	| PrintCanonicalConversions ->
 	    xlate_error "TODO: Print Canonical Structures"
+	| PrintAssumptions _ -> 
+	    xlate_error "TODO: Print Needed Assumptions"
+	| PrintInstances _ -> 
+	    xlate_error "TODO: Print Instances"
+	| PrintTypeClasses -> 
+	    xlate_error "TODO: Print TypeClasses"
 	| PrintInspect n -> CT_inspect (CT_int n)
 	| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
 	| PrintSetoids -> CT_print_setoids
@@ -1837,12 +1889,14 @@ let rec xlate_vernac =
   | VernacBeginSection (_,id) ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
-  | VernacStartTheoremProof (k, (_,s), (bl,c), _, _) ->
+  | VernacStartTheoremProof (k, [Some (_,s), (bl,c)], _, _) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND(
 	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
            xlate_binder_list bl, xlate_formula c))
+  | VernacStartTheoremProof _ ->
+      xlate_error "TODO: Mutually dependent theorems"
   | VernacSuspend -> CT_suspend
-  | VernacResume idopt -> CT_resume (xlate_ident_opt (option_map snd idopt))
+  | VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt))
   | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND
 	(CT_theorem_goal
@@ -1853,8 +1907,9 @@ let rec xlate_vernac =
 	(xlate_defn kind, xlate_ident s, xlate_binder_list bl,
 	   cvt_optional_eval_for_definition c red_option,
            xlate_formula_opt typ_opt)
-  | VernacAssumption (kind, b) ->
-      CT_variable (xlate_var kind, cvt_vernac_binders b)
+  | VernacAssumption (kind,inline ,b) ->xlate_error "TODO: Parameter Inline"
+      (*inline : bool -> automatic delta reduction at fonctor application*)
+     (* CT_variable (xlate_var kind, cvt_vernac_binders b)*)
   | VernacCheckMayEval (None, numopt, c) ->
       CT_check (xlate_formula c)
   | VernacSearch (s,x) ->
@@ -1884,7 +1939,7 @@ let rec xlate_vernac =
       (_, (add_coercion, (_,s)), binders, c1,
        rec_constructor_or_none, field_list) ->
       let record_constructor =
-        xlate_ident_opt (option_map snd rec_constructor_or_none) in
+        xlate_ident_opt (Option.map snd rec_constructor_or_none) in
       CT_record
        ((if add_coercion then CT_coercion_atm else
           CT_coerce_NONE_to_COERCION_OPT(CT_none)),
@@ -1902,15 +1957,8 @@ let rec xlate_vernac =
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
    | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
    | VernacFixpoint ((lm :: lmi),boxed) ->
-      let strip_mutrec ((fid, (n, ro), bl, arf, ardef), _ntn) =
-        let (struct_arg,bl,arf,ardef) =
-	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
-	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
-         if bl = [] then
-	   let n = out_some n in 
-           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
-           (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
-         else (make_fix_struct (n, bl),bl,arf,ardef) in
+      let strip_mutrec (((_,fid), (n, ro), bl, arf, ardef), _ntn) =
+        let struct_arg = make_fix_struct (n, bl) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match xlate_binder_list bl with
@@ -1922,26 +1970,35 @@ let rec xlate_vernac =
 	  (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
    | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
    | VernacCoFixpoint ((lm :: lmi),boxed) ->
-      let strip_mutcorec ((fid, bl, arf, ardef), _ntn) =
+      let strip_mutcorec (((_,fid), bl, arf, ardef), _ntn) =
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
                       xlate_formula arf, xlate_formula ardef) in
         CT_cofix_decl
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
    | VernacScheme [] -> xlate_error "induction scheme"
    | VernacScheme (lm :: lmi) ->
-      let strip_ind ((_,id), depstr, inde, sort) =
+      let strip_ind = function
+      | (Some (_,id), InductionScheme (depstr, inde, sort)) ->
            CT_scheme_spec
             (xlate_ident id, xlate_dep depstr, 
 	    CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
-	     xlate_sort sort) in
+	     xlate_sort sort)
+      | (None, InductionScheme (depstr, inde, sort)) ->
+           CT_scheme_spec
+            (xlate_ident (id_of_string ""), xlate_dep depstr,
+            CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
+             xlate_sort sort)
+      | (_, EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in
         CT_ind_scheme
 	  (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
-   | VernacSyntacticDefinition (id, c, false, _) ->
+   | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme"
+   | VernacSyntacticDefinition ((_,id), ([],c), false, _) ->
        CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None)
-   | VernacSyntacticDefinition (id, c, true, _) ->
-       xlate_error "TODO: Local abbreviations"
+   | VernacSyntacticDefinition ((_,id), _, _, _) ->
+       xlate_error"TODO: Local abbreviations and abbreviations with parameters"
   (* Modules and Module Types *)
-  | VernacDeclareModuleType((_, id), bl, mty_o)  -> 
+   | VernacInclude (_) -> xlate_error "TODO : Include "
+   | VernacDeclareModuleType((_, id), bl, mty_o)  -> 
       CT_module_type_decl(xlate_ident id,
 			  xlate_module_binder_list bl,
 			  match mty_o with
@@ -2051,6 +2108,12 @@ let rec xlate_vernac =
        | Local -> CT_local in
       CT_coercion (local_opt, id_opt, xlate_ident id1,
         xlate_class id2, xlate_class id3)
+
+    (* Type Classes *) 
+   | VernacDeclareInstance _|VernacContext _|
+	 VernacInstance (_, _, _, _, _)|VernacClass (_, _, _, _, _) ->
+	   xlate_error "TODO: Type Classes commands"
+
   | VernacResetName id -> CT_reset (xlate_ident (snd id))
   | VernacResetInitial -> CT_restore_state (CT_ident "Initial")
   | VernacExtend (s, l) ->
@@ -2073,10 +2136,10 @@ let rec xlate_vernac =
 	       CT_coerce_ID_LIST_to_ID_LIST_OPT
 	       (CT_id_list
 	       (List.map
-		  (function ExplByPos x
+		  (function ExplByPos (x,_), _, _
 		       -> xlate_error
 			   "explication argument by rank is obsolete"
-		     | ExplByName id -> CT_ident (string_of_id id)) l)))
+		     | ExplByName id, _, _ -> CT_ident (string_of_id id)) l)))
   | VernacDeclareImplicits(false, id, opt_positions) ->
       xlate_error "TODO: Implicit Arguments Global"
   | VernacReserve((_,a)::l, f) ->
@@ -2096,13 +2159,15 @@ let rec xlate_vernac =
       let table1 = 
 	match table with
 	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
+	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
 	CT_set_option(table1)
   | VernacSetOption (table, v) -> 
       let table1 = 
 	match table with
 	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
+	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
       let value =
 	match v with
 	  | BoolValue _ -> assert false
@@ -2115,7 +2180,8 @@ let rec xlate_vernac =
       let table1 = 
 	match table with
 	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
+	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
 	CT_unset_option(table1)
   | VernacAddOption (table, l) ->
       let values =
@@ -2130,7 +2196,8 @@ let rec xlate_vernac =
       let table1 = 
 	match table with
 	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
+	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" 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,
@@ -2140,13 +2207,17 @@ let rec xlate_vernac =
 				 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 _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
     VernacSolveExistential (_, _)|VernacCanonical _ |
-     VernacTacticNotation _)
-    -> xlate_error "TODO: vernac";;
+     VernacTacticNotation _ | VernacUndoTo _ | VernacRemoveName _)
+    -> xlate_error "TODO: vernac"
+and level_to_ct_LEVEL = function
+    Conv_oracle.Opaque -> CT_Opaque
+  | Conv_oracle.Level n -> CT_Level (CT_int n)
+  | Conv_oracle.Expand -> CT_Expand;;
+
 
 let rec xlate_vernac_list =
  function
diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli
index bedb4ac8..2e2b95fe 100644
--- a/contrib/interface/xlate.mli
+++ b/contrib/interface/xlate.mli
@@ -6,4 +6,3 @@ val xlate_formula : Topconstr.constr_expr -> ct_FORMULA;;
 val xlate_ident : Names.identifier -> ct_ID;;
 val xlate_vernac_list : Vernacexpr.vernac_expr -> ct_COMMAND_LIST;;
 
-val declare_in_coq : (unit -> unit);;