Adding files for the production of textual explanations as used in pcoq.

dependence files are updated accordingly.

Modifications in other files to cope with a few errors in the translation for
the parser (mostly around records, coercions, and the search-pattern command).


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

12 files changed, 2203 insertions, 108 deletions

diff --git a/.depend b/.depend
index 8b7bc1691..39166699b 100644
--- a/.depend
+++ b/.depend
@@ -265,6 +265,14 @@ contrib/interface/debug_tac.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
 contrib/interface/name_to_ast.cmi: parsing/coqast.cmi library/nametab.cmi 
 contrib/interface/pbp.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
     proofs/tacmach.cmi 
+contrib/interface/showproof.cmi: contrib/interface/ascent.cmi \
+    parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \
+    kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/inductive.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    kernel/reduction.cmi contrib/interface/showproof_ct.cmo kernel/sign.cmi \
+    lib/stamps.cmi kernel/term.cmi contrib/interface/translate.cmi \
+    pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi 
 contrib/interface/translate.cmi: contrib/interface/ascent.cmi \
     kernel/environ.cmi kernel/evd.cmi proofs/proof_type.cmi kernel/term.cmi 
 contrib/interface/vtp.cmi: contrib/interface/ascent.cmi 
@@ -800,18 +808,18 @@ proofs/evar_refiner.cmx: parsing/astterm.cmx kernel/environ.cmx \
     proofs/evar_refiner.cmi 
 proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
     pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi \
-    kernel/inductive.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi kernel/typeops.cmi pretyping/typing.cmi \
-    lib/util.cmi proofs/logic.cmi 
+    kernel/inductive.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    kernel/reduction.cmi pretyping/retyping.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \
+    pretyping/typing.cmi lib/util.cmi proofs/logic.cmi 
 proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
     pretyping/evarutil.cmx kernel/evd.cmx library/global.cmx \
-    kernel/inductive.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
-    pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \
-    lib/util.cmx proofs/logic.cmi 
+    kernel/inductive.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+    parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    kernel/reduction.cmx pretyping/retyping.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \
+    pretyping/typing.cmx lib/util.cmx proofs/logic.cmi 
 proofs/pfedit.cmo: parsing/astterm.cmi kernel/declarations.cmi \
     library/declare.cmi lib/edit.cmi kernel/environ.cmi kernel/evd.cmi \
     library/lib.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
@@ -1469,27 +1477,27 @@ contrib/correctness/prename.cmx: toplevel/himsg.cmx kernel/names.cmx \
 contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
     parsing/coqast.cmi library/declare.cmi lib/dyn.cmi kernel/evd.cmi \
     parsing/g_zsyntax.cmi library/global.cmi toplevel/himsg.cmi \
-    kernel/names.cmi contrib/correctness/past.cmi parsing/pcoq.cmi \
-    contrib/correctness/pdb.cmi contrib/correctness/peffect.cmi \
-    contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi \
-    contrib/correctness/pmonad.cmi lib/pp.cmi contrib/correctness/prename.cmi \
-    contrib/correctness/ptactic.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/ptyping.cmi contrib/correctness/putil.cmi \
-    kernel/reduction.cmi proofs/tacinterp.cmi kernel/term.cmi \
-    parsing/termast.cmi lib/util.cmi toplevel/vernac.cmi \
+    kernel/names.cmi lib/options.cmi contrib/correctness/past.cmi \
+    parsing/pcoq.cmi contrib/correctness/pdb.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi lib/pp.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptactic.cmi \
+    contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmi \
+    contrib/correctness/putil.cmi kernel/reduction.cmi proofs/tacinterp.cmi \
+    kernel/term.cmi parsing/termast.cmi lib/util.cmi toplevel/vernac.cmi \
     toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \
     contrib/correctness/psyntax.cmi 
 contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
     parsing/coqast.cmx library/declare.cmx lib/dyn.cmx kernel/evd.cmx \
     parsing/g_zsyntax.cmx library/global.cmx toplevel/himsg.cmx \
-    kernel/names.cmx contrib/correctness/past.cmi parsing/pcoq.cmx \
-    contrib/correctness/pdb.cmx contrib/correctness/peffect.cmx \
-    contrib/correctness/penv.cmx contrib/correctness/pmisc.cmx \
-    contrib/correctness/pmonad.cmx lib/pp.cmx contrib/correctness/prename.cmx \
-    contrib/correctness/ptactic.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/ptyping.cmx contrib/correctness/putil.cmx \
-    kernel/reduction.cmx proofs/tacinterp.cmx kernel/term.cmx \
-    parsing/termast.cmx lib/util.cmx toplevel/vernac.cmx \
+    kernel/names.cmx lib/options.cmx contrib/correctness/past.cmi \
+    parsing/pcoq.cmx contrib/correctness/pdb.cmx \
+    contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx lib/pp.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptactic.cmx \
+    contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmx \
+    contrib/correctness/putil.cmx kernel/reduction.cmx proofs/tacinterp.cmx \
+    kernel/term.cmx parsing/termast.cmx lib/util.cmx toplevel/vernac.cmx \
     toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
     contrib/correctness/psyntax.cmi 
 contrib/correctness/ptactic.cmo: toplevel/command.cmi library/declare.cmi \
@@ -1627,6 +1635,7 @@ contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     pretyping/pretyping.cmi parsing/printer.cmi proofs/proof_trees.cmi \
     proofs/proof_type.cmi toplevel/protectedtoplevel.cmi \
     pretyping/rawterm.cmi kernel/reduction.cmi parsing/search.cmi \
+    contrib/interface/showproof.cmi contrib/interface/showproof_ct.cmo \
     proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
     kernel/term.cmi parsing/termast.cmi contrib/interface/translate.cmi \
     lib/util.cmi toplevel/vernac.cmi toplevel/vernacentries.cmi \
@@ -1645,6 +1654,7 @@ contrib/interface/centaur.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
     pretyping/pretyping.cmx parsing/printer.cmx proofs/proof_trees.cmx \
     proofs/proof_type.cmx toplevel/protectedtoplevel.cmx \
     pretyping/rawterm.cmx kernel/reduction.cmx parsing/search.cmx \
+    contrib/interface/showproof.cmx contrib/interface/showproof_ct.cmx \
     proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
     kernel/term.cmx parsing/termast.cmx contrib/interface/translate.cmx \
     lib/util.cmx toplevel/vernac.cmx toplevel/vernacentries.cmx \
@@ -1728,6 +1738,32 @@ contrib/interface/pbp.cmx: parsing/coqast.cmx parsing/coqlib.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     contrib/interface/pbp.cmi 
+contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \
+    proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \
+    kernel/environ.cmi kernel/evd.cmi library/global.cmi kernel/inductive.cmi \
+    kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+    contrib/interface/showproof_ct.cmo kernel/sign.cmi lib/stamps.cmi \
+    proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \
+    contrib/interface/translate.cmi pretyping/typing.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi contrib/interface/showproof.cmi 
+contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \
+    proofs/clenv.cmx parsing/coqast.cmx kernel/declarations.cmx \
+    kernel/environ.cmx kernel/evd.cmx library/global.cmx kernel/inductive.cmx \
+    kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+    contrib/interface/showproof_ct.cmx kernel/sign.cmx lib/stamps.cmx \
+    proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \
+    contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx contrib/interface/showproof.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+    parsing/printer.cmi contrib/interface/translate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+    parsing/printer.cmx contrib/interface/translate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     parsing/coqast.cmi kernel/environ.cmi pretyping/evarutil.cmi \
     kernel/evd.cmi library/libobject.cmi library/library.cmi kernel/names.cmi \
diff --git a/Makefile b/Makefile
index 67f50a152..beccd83fd 100644
--- a/Makefile
+++ b/Makefile
@@ -158,6 +158,7 @@ INTERFACE=contrib/interface/vtp.cmo contrib/interface/xlate.cmo \
 	contrib/interface/dad.cmo \
 	contrib/interface/history.cmo \
 	contrib/interface/name_to_ast.cmo contrib/interface/debug_tac.cmo \
+	contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo \
 	contrib/interface/centaur.cmo
 
 PARSERREQUIRES=lib/pp_control.cmo lib/pp.cmo \
@@ -219,6 +220,7 @@ COQC=bin/coqc
 COQTOPBYTE=bin/coqtop.byte
 COQTOPOPT=bin/coqtop.opt
 BESTCOQTOP=bin/coqtop.$(BEST)
+COQINTERFACE=bin/coq-interface bin/parser
 
 COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) 
 
@@ -282,7 +284,7 @@ toplevel: $(TOPLEVEL)
 bin/coq-interface: $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE)
 	$(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@ $(INTERFACE)
 
-bin/parser: contrib/interface/parse.cmo contrib/interface/line_parser.cmo $(PARSERREQUIRES) contrib/interface/xlate.cmo
+bin/parser: contrib/interface/parse.cmo contrib/interface/line_parser.cmo $(PARSERREQUIRES) contrib/interface/xlate.cmo contrib/interface/vtp.cmo
 	$(OCAMLC) -cclib -lunix -custom $(INCLUDES) -o $@ $(CMA) \
 	$(PARSERREQUIRES) \
 	line_parser.cmo vtp.cmo xlate.cmo parse.cmo
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 07487e82b..d6eaf0c6d 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -118,6 +118,8 @@ and ct_COMMAND =
   | CT_resume of ct_ID_OPT
   | CT_save of ct_THM_OPT * ct_ID_OPT
   | CT_search of ct_ID * ct_IN_OR_OUT_MODULES
+  | CT_search_pattern of ct_FORMULA * ct_IN_OR_OUT_MODULES
+  | CT_search_rewrite of ct_FORMULA * ct_IN_OR_OUT_MODULES
   | CT_section_end of ct_ID
   | CT_section_struct of ct_SECTION_BEGIN * ct_SECTION_BODY * ct_COMMAND
   | CT_set_natural of ct_ID
@@ -507,6 +509,14 @@ and ct_TARG =
   | CT_coerce_UNFOLD_NE_LIST_to_TARG of ct_UNFOLD_NE_LIST
 and ct_TARG_LIST =
     CT_targ_list of ct_TARG list
+and ct_TEXT =
+    CT_coerce_ID_to_TEXT of ct_ID
+  | CT_text_formula of ct_FORMULA
+  | CT_text_h of ct_TEXT list
+  | CT_text_hv of ct_TEXT list
+  | CT_text_op of ct_TEXT list
+  | CT_text_path of ct_SIGNED_INT_LIST
+  | CT_text_v of ct_TEXT list
 and ct_THEOREM_GOAL =
     CT_goal of ct_FORMULA
   | CT_theorem_goal of ct_DEFN_OR_THM * ct_ID * ct_FORMULA
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index 24e3db2b0..79fd23b07 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -38,9 +38,11 @@ open Debug_tac;;
 open Search;;
 open Astterm;;
 open Nametab;;
+open Showproof;;
+open Showproof_ct;;
 
 
-let text_proof_flag = ref false;;
+let text_proof_flag = ref "en";;
 
 let current_proof_name = ref "";;
 
@@ -150,6 +152,7 @@ type vtp_tree =
   | 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 = 
@@ -160,6 +163,7 @@ let print_tree t =
   | 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";;
 
@@ -201,23 +205,24 @@ let print_past_goal index =
      output_results  (ctf_PathGoalMessage ())
        (Some (P_r (translate_goal pf.goal)))
  with
- | Invalid_argument s -> error "No focused proof (No proof-editing in progress)"
+   | Invalid_argument s ->
+      ((try traverse_to [] with _ -> ());
+       error "No focused proof (No proof-editing in progress)")
+   | e -> (try traverse_to [] with _ -> ()); raise e
 ;;
 
 let show_nth n =
   try
     let pf = proof_of_pftreestate (get_pftreestate()) in
-    if (!text_proof_flag) then
-      errorlabstrm "debug" [< 'sTR "text printing unplugged" >]
-(*
+    if (!text_proof_flag<>"off") then
+(*      errorlabstrm "debug" [< 'sTR "text printing unplugged" >]*)
        (if n=0
 	   then output_results (ctf_TextMessage !global_request_id)
-                               (Some (P_t (show_proof [])))
+                               (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_t (show_proof path))))
-*)
+                          (Some (P_text (show_proof !text_proof_flag path))))
     else
       output_results (ctf_GoalReqIdMessage !global_request_id)
       (let goal = List.nth (fst (frontier pf))
@@ -445,8 +450,9 @@ let command_changes = [
    (function
      |  [VARG_AST (Id(_,x))] ->
 	 (match x with
-	   "on" -> (function () -> text_proof_flag := true)
-	 | "off" -> (function () -> text_proof_flag := false)
+	   "fr" -> (function () -> text_proof_flag := "fr")
+	 | "en" -> (function () -> text_proof_flag := "en")
+	 | "off" -> (function () -> text_proof_flag := "off")
 	 | s -> errorlabstrm "TEXT_MODE" (make_error_stream 
 					    ("Unexpected flag " ^ s)))
      | _ -> errorlabstrm "TEXT_MODE" 
@@ -566,58 +572,6 @@ let command_changes = [
 		 [< 'sTR "not available in Centaur mode" >])
      | _ -> errorlabstrm "EndSilent" (make_error_stream "EndSilent")));
   
-  ("SaveNamed", 
-   (function
-     | [] ->
-	 (function () -> traverse_to []; save_named false)
-     | _ -> errorlabstrm "SaveNamed" (make_error_stream "SaveNamed")));
-  
-  ("DefinedNamed", 
-   (function
-     | [] ->
-	 (function () -> traverse_to []; save_named false)
-     | _ -> errorlabstrm "DefinedNamed" (make_error_stream "DefinedNamed")));
-  
-  ("DefinedAnonymous", 
-   (function
-     | (VARG_IDENTIFIER id) :: [] ->
-	 (function () ->
-	   traverse_to [];
-	   save_anonymous_thm true (string_of_id id))
-     | _ ->
-	 errorlabstrm "DefinedAnonymous"
-	   (make_error_stream "DefinedAnonymous")));
-  
-    ("SaveAnonymous", 
-   (function
-     | (VARG_IDENTIFIER id) :: [] ->
-	 (function () ->
-	   traverse_to [];
-	   save_anonymous_thm true (string_of_id id))
-     | _ ->
-	 errorlabstrm "SaveAnonymous"
-	   (make_error_stream "SaveAnonymous")));
-  
-  ("SaveAnonymousThm", 
-   (function
-     | (VARG_IDENTIFIER id) :: [] ->
-	 (function () ->
-	   traverse_to [];
-	   save_anonymous_thm true (string_of_id id))
-     | _ ->
-	 errorlabstrm "SaveAnonymousThm"
-	   (make_error_stream "SaveAnonymousThm")));
-  
-  ("SaveAnonymousRmk", 
-   (function
-     | (VARG_IDENTIFIER id) :: [] ->
-	 (function
-	     () -> traverse_to [];
-	       save_anonymous_remark true (string_of_id id))
-     | _ ->
-	 errorlabstrm "SaveAnonymousRmk"
-	   (make_error_stream "SaveAnonymousRmk")));
-  
   ("ABORT", 
    (function
      | (VARG_IDENTIFIER id) :: [] ->
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 7648e7922..bdda47e38 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -223,10 +223,9 @@ let parse_string_action reqid phylum char_stream string_list =
 
 
 let quiet_parse_string_action char_stream =
- try 
-   let _ = 
-     Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream) in
-   ()
+ try let _ = 
+         Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream) in
+     ()
  with
  | _ -> flush_until_end_of_stream char_stream; ();;
 
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
new file mode 100644
index 000000000..ad6544a0b
--- /dev/null
+++ b/contrib/interface/showproof.ml
@@ -0,0 +1,1824 @@
+(*
+#use "/cygdrive/D/Tools/coq-7avril/dev/base_include";;
+open Coqast;;
+*)
+open Environ
+open Evd
+open Names
+open Stamps
+open Term
+open Util
+open Proof_type
+open Coqast
+open Pfedit
+open Translate
+open Term
+open Reduction
+open Clenv
+open Astterm
+open Typing
+open Inductive
+open Vernacinterp
+open Declarations
+open Showproof_ct
+open Proof_trees
+open Sign
+open Pp
+open Printer
+(*****************************************************************************)
+(*
+   Arbre de preuve maison:
+   
+*)
+
+(* hypotheses *)
+
+type nhyp = {hyp_name : identifier;
+             hyp_type : Term.constr;
+             hyp_full_type: Term.constr}
+;;
+
+type ntactic = Coqast.t list
+;;
+
+type nproof =
+    Notproved
+  | Proof of ntactic * (ntree list)
+
+and ngoal=
+     {newhyp : nhyp list;
+      t_concl : Term.constr;
+      t_full_concl: Term.constr;
+      t_full_env: Sign.named_context}
+and ntree=
+      {t_info:string;
+	t_goal:ngoal;
+       	t_proof : nproof}
+;;
+
+
+let hyps {t_info=info;
+	 t_goal={newhyp=lh;t_concl=g;t_full_concl=gf;t_full_env=ge};
+	 t_proof=p} = lh
+;;
+
+let concl {t_info=info;
+	 t_goal={newhyp=lh;t_concl=g;t_full_concl=gf;t_full_env=ge};
+	 t_proof=p} = g
+;;
+
+let proof {t_info=info;
+	 t_goal={newhyp=lh;t_concl=g;t_full_concl=gf;t_full_env=ge};
+	 t_proof=p} = p
+;;
+let g_env {t_info=info;
+	 t_goal={newhyp=lh;t_concl=g;t_full_concl=gf;t_full_env=ge};
+	 t_proof=p} = ge
+;;
+let sub_ntrees t =
+  match (proof t) with
+    Notproved -> []
+  | Proof (_,l) -> l
+;;
+
+let tactic t =
+  match (proof t) with
+    Notproved -> failwith "no tactic applied"
+  | Proof (t,_) -> t
+;;
+
+
+(* 
+un arbre est clos s'il ne contient pas de sous-but non prouves,
+ou bien s'il a un cousin gauche qui n'est pas clos 
+ce qui fait qu'on a au plus un sous-but non clos, le premier sous-but.
+*)
+let update_closed nt =
+  let found_not_closed=ref false in
+  let rec update {t_info=b; t_goal=g; t_proof =p} =
+    if !found_not_closed
+    then  {t_info="to_prove"; t_goal=g; t_proof =p}
+    else
+      match p with
+      	Notproved -> found_not_closed:=true;
+	  {t_info="not_proved"; t_goal=g; t_proof =p}
+      | Proof(tac,lt) ->
+	  let lt1=List.map update lt in
+	  let b=ref "proved" in
+	  (List.iter
+	     (fun x ->
+	       if x.t_info ="not_proved" then b:="not_proved") lt1;
+	   {t_info=(!b);
+	     t_goal=g;
+             t_proof=Proof(tac,lt1)})
+  in update nt
+    ;;
+    
+      
+(*
+    type complet avec les hypotheses.
+*)
+
+let long_type_hyp lh t=
+   let t=ref t in
+   List.iter (fun (n,th) ->
+         let Name ni = n in
+         t:= mkProd(n,th,subst_term (mkVar ni) !t))
+       (List.rev lh);
+   !t
+;;
+
+(* let long_type_hyp x y = y;; *)
+
+(* Expansion des tactikelles *)
+
+let seq_to_lnhyp sign sign' cl =
+      let lh= ref (List.map (fun (x,c,t) -> (Name x, t)) sign) in
+      let nh=List.map (fun (id,c,ty) -> 
+             {hyp_name=id;
+              hyp_type=ty;
+              hyp_full_type=
+                let res= long_type_hyp !lh ty in
+                lh:=(!lh)@[(Name id,ty)];
+                res})
+              sign'
+      in
+      {newhyp=nh;
+       t_concl=cl;
+       t_full_concl=long_type_hyp !lh cl;
+       t_full_env = sign@sign'}
+;;
+
+
+let rule_is_complex r =
+   match r with
+      Tactic ("Interp",_) -> true
+   |  Tactic ("Auto", _) -> true
+   |  Tactic ("Symmetry", _) -> true 
+    |_ -> false
+;;
+
+let ast_of_constr = Termast.ast_of_constr true (Global.env()) ;;
+
+let rule_to_ntactic r =
+   let rast =
+     (match r with
+       Tactic (s,l) ->
+	 Ast.ope (s,(List.map ast_of_cvt_arg l))
+     | Prim {name=Refine;hypspecs=_; newids=_; params=_; terms=[h]} ->
+	 Ast.ope ("Exact",
+		  [Node ((0,0), "COMMAND", [ast_of_constr h])])
+     | _ -> Ast.ope ("Intros",[])) in
+   if rule_is_complex r
+   then (match rast with
+           Node(_,_,[Node(_,_,[Node(_,_,x)])]) ->x)
+   else [rast ]
+;;
+
+
+let term_of_command x =
+  match x with
+    Node(_,_,y::_) -> y
+  | _ -> x
+;;
+
+(* Attribue les preuves de la liste l aux sous-buts non-prouvés de nt  *)
+
+
+let fill_unproved nt l =
+  let lnt = ref l in
+  let rec fill nt =
+    let {t_goal=g;t_proof=p}=nt in
+       match p with
+        Notproved -> let p=List.hd (!lnt) in
+                     lnt:=List.tl (!lnt);
+                     {t_info="to_prove";t_goal=g;t_proof=p}
+       |Proof(tac,lt) ->
+          {t_info="to_prove";t_goal=g;
+           t_proof=Proof(tac,List.map fill lt)}
+  in fill nt
+;;
+(* Differences entre signatures *)
+
+let new_sign osign sign =
+    let res=ref [] in
+    List.iter (fun (id,c,ty) ->
+		   try (let  ty1= (lookup_id_type id osign) in
+			())
+		   with Not_found -> res:=(id,c,ty)::(!res))
+              sign;
+    !res
+;;
+
+let old_sign osign sign =
+    let res=ref [] in
+    List.iter (fun (id,c,ty) ->
+		   try (let  ty1= (lookup_id_type id osign) in
+			if ty1 = ty then res:=(id,c,ty)::(!res))
+		   with Not_found -> ())
+              sign;
+    !res
+;;
+
+(* convertit l'arbre de preuve courant en ntree *)
+let  to_nproof sigma osign pf =
+  let rec to_nproof_rec sigma osign pf =
+    let {evar_hyps=sign;evar_concl=cl;evar_info=info} = pf.goal in
+    let nsign = new_sign osign sign in 
+    let oldsign = old_sign osign sign in 
+    match pf.ref with
+      
+      None -> {t_info="to_prove";
+	      	t_goal=(seq_to_lnhyp oldsign nsign cl);
+              	t_proof=Notproved}
+    | Some(r,spfl) ->
+      	if rule_is_complex r
+      	then (
+	  let p1=(match pf.subproof with
+            Some x -> to_nproof_rec sigma sign x) in
+          let ntree= fill_unproved p1 
+              (List.map (fun x -> (to_nproof_rec sigma sign x).t_proof)
+		 spfl) in
+	  match r with
+	    Tactic ("Auto",_) ->
+	      if spfl=[]
+	      then
+	      	{t_info="to_prove";
+	    	  t_goal= {newhyp=[];
+			    t_concl=concl ntree;
+			    t_full_concl=ntree.t_goal.t_full_concl;
+			    t_full_env=ntree.t_goal.t_full_env};
+		  t_proof= Proof ([Node ((0,0), "InfoAuto",[])], [ntree])}
+	      else ntree
+	  | _ -> ntree
+	      )
+      	else
+	  {t_info="to_prove";
+	    t_goal=(seq_to_lnhyp oldsign nsign cl);
+       	    t_proof=(Proof (rule_to_ntactic r,
+			      List.map (fun x -> to_nproof_rec sigma sign x) spfl))}
+  in update_closed (to_nproof_rec sigma osign pf)
+    ;;
+
+(* 
+  recupere l'arbre de preuve courant.
+*)
+
+let get_nproof () =
+  to_nproof (Global.env()) []
+            (Tacmach.proof_of_pftreestate (get_pftreestate()))
+;;
+
+    
+(*****************************************************************************)
+(*
+   Pprinter
+*)
+
+let pr_void () = sphs "";;
+
+let list_rem l = match l with [] -> [] |x::l1->l1;;
+
+(* liste de chaines *)
+let prls l = 
+   let res = ref (sps (List.hd l)) in
+   List.iter (fun s -> 
+     res:= sphv [ !res; spb; sps s]) (list_rem l);
+   !res
+;;
+
+let prphrases f l = 
+   spv (List.map (fun s -> sphv [f s; sps ","]) l)
+;;
+
+(* indentation *)
+let spi = spnb 3;;
+
+(* en colonne *)
+let prl f l = 
+   if l=[] then spe else spv (List.map f l);;
+(*en colonne,  avec indentation *)
+let prli f l =  
+   if l=[] then spe else sph [spi; spv (List.map f l)];;
+
+(* 
+  Langues.
+*)
+
+let rand l =
+  List.nth l (Random.int (List.length l))
+;;
+
+type natural_languages = French | English;;
+let natural_language = ref French;;
+
+(*****************************************************************************)
+(*
+   Les liens html pour proof-by-pointing
+*)
+
+(* le path du but en cours. *)
+
+let path=ref[1];;
+
+let ftag_apply =ref (fun (n:string) t -> spt t);;
+
+let ftag_case =ref (fun n -> sps n);;
+
+let ftag_elim =ref (fun n ->  sps n);;
+
+let ftag_hypt =ref (fun h t -> sphypt (translate_path !path) h t);;
+
+let ftag_hyp =ref (fun h t -> sphyp (translate_path !path) h t);;
+
+let ftag_uselemma =ref (fun h t ->
+  let intro = match !natural_language with
+    French -> "par"
+  | English -> "by"
+  in
+  spuselemma intro h t);;
+
+let ftag_toprove =ref (fun t -> sptoprove (translate_path !path) t);;
+
+let tag_apply = !ftag_apply;;
+
+let tag_case = !ftag_case;;
+
+let tag_elim = !ftag_elim;;
+
+let tag_uselemma = !ftag_uselemma;;
+
+let tag_hyp = !ftag_hyp;;
+
+let tag_hypt = !ftag_hypt;;
+
+let tag_toprove = !ftag_toprove;;
+
+(*****************************************************************************)
+
+(* pluriel *)
+let txtn n s =
+  if n=1 then s
+  else match s with
+    |"un" -> "des"
+    |"a" -> ""
+    |"an" -> ""
+    |"une" -> "des"
+    |"Soit" -> "Soient"
+    | s -> s^"s"
+;;
+
+let _et () =  match !natural_language with
+    French -> sps "et"
+| English -> sps "and"
+;;
+
+let name_count = ref 0;;
+let new_name () =
+  name_count:=(!name_count)+1;
+  string_of_int !name_count
+;;
+
+let enumerate f ln =
+  match ln with
+    [] -> []
+  | [x] -> [f x]
+  |ln -> 
+  let rec enum_rec f ln = 
+     (match ln with 
+       [x;y] -> [f x; spb; sph [_et ();spb;f y]]
+      |x::l -> [sph [(f x);sps ","];spb]@(enum_rec f l))
+  in enum_rec f ln
+;;
+
+
+let constr_of_ast = Astterm.interp_constr Evd.empty (Global.env());;
+let sp_tac tac =
+   try spt (constr_of_ast (term_of_command tac))
+   with _ -> (* let Node(_,t,_) = tac in *)
+             spe (* sps ("error in sp_tac " ^ t) *)
+;;
+
+let soit_A_une_proposition nh ln t=  match !natural_language with
+    French ->
+      sphv ([sps (txtn nh "Soit");spb]@(enumerate (fun x -> tag_hyp x t) ln)
+            @[spb; prls [txtn nh "une";txtn nh "proposition"]])
+| English ->
+      sphv ([sps "Let";spb]@(enumerate (fun x -> tag_hyp x t) ln)
+            @[spb; prls ["be"; txtn nh "a";txtn nh "proposition"]])
+;;
+
+let on_a ()=  match !natural_language with
+  French -> rand ["on a "]
+| English ->rand ["we have "]
+;;
+
+let bon_a ()=  match !natural_language with
+  French -> rand ["On a "]
+| English ->rand ["We have "]
+;;
+
+let soit_X_un_element_de_T nh ln t =  match !natural_language with
+  French ->
+    sphv ([sps (txtn nh "Soit");spb]@(enumerate (fun x -> tag_hyp x t) ln)
+          @[spb; prls [txtn nh "un";txtn nh "élément";"de"]]
+          @[spb; spt t])
+| English ->
+    sphv ([sps (txtn nh "Let");spb]@(enumerate (fun x -> tag_hyp x t) ln)
+          @[spb; prls ["be";txtn nh "an";txtn nh "element";"of"]]
+          @[spb; spt t])
+;;
+
+let soit_F_une_fonction_de_type_T nh ln t =  match !natural_language with
+  French ->
+    sphv ([sps (txtn nh "Soit");spb]@(enumerate (fun x -> tag_hyp x t) ln)
+          @[spb; prls [txtn nh "une";txtn nh "fonction";"de";"type"]]
+          @[spb; spt t])
+| English ->
+    sphv ([sps (txtn nh "Let");spb]@(enumerate (fun x -> tag_hyp x t) ln)
+          @[spb; prls ["be";txtn nh "a";txtn nh "function";"of";"type"]]
+          @[spb; spt t])
+;;
+
+
+let telle_que nh =  match !natural_language with
+    French -> [prls [" ";txtn nh "telle";"que";" "]]
+| English -> [prls [" "; "such";"that";" "]]
+;;
+
+let tel_que nh =  match !natural_language with
+    French -> [prls [" ";txtn nh "tel";"que";" "]]
+| English -> [prls [" ";"such";"that";" "]]
+;;
+
+let supposons () =  match !natural_language with
+    French -> "Supposons "
+|  English -> "Suppose "
+;;
+
+let cas () =  match !natural_language with
+    French -> "Cas"
+|  English -> "Case"
+;;
+
+let donnons_une_proposition () =  match !natural_language with
+    French -> sph[ (prls ["Donnons";"une";"proposition"])]
+|  English -> sph[ (prls ["Let us give";"a";"proposition"])]
+;;
+
+let montrons g =  match !natural_language with
+    French -> sph[ sps (rand ["Prouvons";"Montrons";"Démontrons"]);
+		   spb; spt g; sps ". "]
+|  English -> sph[ sps (rand ["Let us";"Now"]);spb;
+		   sps (rand ["prove";"show"]);
+		   spb; spt g; sps ". "]
+;;
+
+let calculons_un_element_de g =  match !natural_language with
+    French -> sph[ (prls ["Calculons";"un";"élément";"de"]);
+		   spb; spt g; sps ". "]
+|  English -> sph[ (prls ["Let us";"compute";"an";"element";"of"]);
+		   spb; spt g; sps ". "]
+;;
+
+let calculons_une_fonction_de_type g =  match !natural_language with
+    French -> sphv [ (prls ["Calculons";"une";"fonction";"de";"type"]);
+                spb; spt g; sps ". "]
+|  English -> sphv [ (prls ["Let";"us";"compute";"a";"function";"of";"type"]);
+                spb; spt g; sps ". "];;
+
+let en_simplifiant_on_obtient g =  match !natural_language with
+    French ->
+      sphv [ (prls [rand ["Après simplification,"; "En simplifiant,"];
+		     rand ["on doit";"il reste à"];
+		     rand ["prouver";"montrer";"démontrer"]]);
+		     spb; spt g; sps ". "]
+|  English ->
+      sphv [ (prls [rand ["After simplification,"; "Simplifying,"];
+		     rand ["we must";"it remains to"];
+		     rand ["prove";"show"]]);
+		     spb; spt g; sps ". "] ;;
+
+let on_obtient g =  match !natural_language with
+  French -> sph[ (prls [rand ["on doit";"il reste à"];
+			 rand ["prouver";"montrer";"démontrer"]]);
+                 spb; spt g; sps ". "]
+|  English ->sph[ (prls [rand ["we must";"it remains to"];
+		     rand ["prove";"show"]]);
+                  spb; spt g; sps ". "]
+;;
+
+let reste_a_montrer g =  match !natural_language with
+    French -> sph[ (prls ["Reste";"à";
+			   rand ["prouver";"montrer";"démontrer"]]);
+                spb; spt g; sps ". "]
+|  English -> sph[ (prls ["It remains";"to";
+			   rand ["prove";"show"]]);
+                spb; spt g; sps ". "] 
+;;
+
+let discutons_avec_A type_arg  =  match !natural_language with
+    French -> sphv [sps "Discutons"; spb; sps "avec"; spb;
+				   spt type_arg; sps ":"] 
+|  English -> sphv [sps "Let us discuss"; spb; sps "with"; spb;
+				   spt type_arg; sps ":"] 
+;;
+
+let utilisons_A arg1  =  match !natural_language with
+    French -> sphv [sps (rand ["Utilisons";"Avec";"A l'aide de"]);
+		     spb; spt arg1; sps ":"] 
+|  English -> sphv [sps (rand ["Let us use";"With";"With the help of"]);
+		     spb; spt arg1; sps ":"] 
+;;
+
+let selon_les_valeurs_de_A arg1  =  match !natural_language with
+    French -> sphv [  (prls ["Selon";"les";"valeurs";"de"]);
+                      spb; spt arg1; sps ":"] 
+|  English -> sphv [  (prls ["According";"values";"of"]);
+                      spb; spt arg1; sps ":"] 
+;;
+
+let de_A_on_a arg1  =  match !natural_language with
+    French -> sphv [  sps (rand ["De";"Avec";"Grâce à"]); spb; spt arg1; spb;
+		      sps (rand ["on a:";"on déduit:";"on obtient:"])]
+|  English -> sphv [  sps (rand ["From";"With";"Thanks to"]); spb;
+		     spt arg1; spb;
+		      sps (rand ["we have:";"we deduce:";"we obtain:"])]
+;;
+
+
+let procedons_par_recurrence_sur_A arg1  =  match !natural_language with
+    French ->  sphv [  (prls ["Procédons";"par";"récurrence";"sur"]);
+			  spb; spt arg1; sps ":"]
+|  English -> sphv [  (prls ["By";"induction";"on"]);
+			  spb; spt arg1; sps ":"]
+;;
+
+
+let calculons_la_fonction_F_de_type_T_par_recurrence_sur_son_argument_A 
+  nfun tfun narg =  match !natural_language with
+    French ->  sphv [  
+                    sphv [ prls ["Calculons";"la";"fonction"];
+                     spb; sps (string_of_id nfun);spb;
+                     prls ["de";"type"];
+                     spb; spt tfun;spb;
+                     prls ["par";"récurrence";"sur";"son";"argument"];
+                     spb; sps (string_of_int narg); sps ":"]
+                 ]
+|  English ->  sphv [  
+                    sphv [ prls ["Let us compute";"the";"function"];
+                     spb; sps (string_of_id nfun);spb;
+                     prls ["of";"type"];
+                     spb; spt tfun;spb;
+                     prls ["by";"induction";"on";"its";"argument"];
+                     spb; sps (string_of_int narg); sps ":"]
+                 ]
+
+;;
+let pour_montrer_G_la_valeur_recherchee_est_A g arg1  =
+  match !natural_language with
+    French ->  sph [sps "Pour";spb;sps "montrer"; spt g; spb;
+		     sps ","; spb; sps "choisissons";spb;
+		     spt arg1;sps ". " ]
+|  English ->  sph [sps "In order to";spb;sps "show"; spt g; spb;
+		     sps ","; spb; sps "let us choose";spb;
+		     spt arg1;sps ". " ]
+;;
+
+let on_se_sert_de_A   arg1  =  match !natural_language with
+    French ->  sph [sps "On se sert de";spb ;spt arg1;sps ":" ]
+|  English ->  sph [sps "We use";spb ;spt arg1;sps ":" ]
+;;
+
+
+let d_ou_A g  =  match !natural_language with
+    French ->  sph [spi; sps "d'où";spb ;spt g;sps ". " ]
+|  English -> sph [spi; sps "then";spb ;spt g;sps ". " ]
+;;
+
+
+let coq_le_demontre_seul ()  =  match !natural_language with
+    French ->   rand [prls ["Coq";"le";"démontre"; "seul."];
+		       sps "Fastoche.";
+		     sps "Trop cool"]
+|  English -> 	rand [prls ["Coq";"shows";"it"; "alone."];
+		       sps "Fingers in the nose."]	      
+;;
+
+let de_A_on_deduit_donc_B arg g  =  match !natural_language with
+    French -> sph
+             [  sps "De"; spb; spt arg; spb; sps "on";spb;
+                sps "déduit";spb; sps "donc";spb;  spt g ]
+|  English -> sph
+             [  sps "From"; spb; spt arg; spb; sps "we";spb;
+                sps "deduce";spb; sps "then";spb;  spt g ]
+;;
+
+let _A_est_immediat_par_B g arg  =  match !natural_language with
+    French -> sph [  spt g;  spb; (prls ["est";"immédiat";"par"]);
+                     spb;  spt arg ] 
+|  English -> sph [  spt g;  spb; (prls ["is";"immediate";"from"]);
+                     spb;  spt arg ] 
+;;
+
+let le_resultat_est arg  =  match !natural_language with
+    French -> sph [  (prls ["le";"résultat";"est"]);
+                    spb; spt arg ] 
+|  English -> sph [  (prls ["the";"result";"is"]);
+                    spb; spt arg ];;
+
+let on_applique_la_tactique tactic tac =  match !natural_language with
+  French -> sphv 
+      [ sps "on applique";spb;sps "la tactique"; spb;tactic;spb;tac]
+|  English -> sphv 
+      [ sps "we apply";spb;sps "the tactic"; spb;tactic;spb;tac]
+;;
+
+let de_A_il_vient_B arg g  =  match !natural_language with
+    French -> sph
+             [  sps "De"; spb; spt arg; spb; 
+               sps "il";spb; sps "vient";spb; spt g; sps ". " ] 
+|  English -> sph
+             [  sps "From"; spb; spt arg; spb; 
+               sps "it";spb; sps "comes";spb; spt g; sps ". " ] 
+;;
+
+let ce_qui_est_trivial ()  =  match !natural_language with
+    French -> sps "Trivial."
+|  English -> sps "Trivial."
+;;
+
+let en_utilisant_l_egalite_A arg  =  match !natural_language with
+    French -> sphv [  sps "En"; spb;sps "utilisant"; spb;
+                   sps "l'egalite"; spb; spt arg; sps ","
+                  ]
+|  English -> sphv [  sps "Using"; spb;
+                   sps "the equality"; spb; spt arg; sps ","
+                  ]
+;;
+
+let simplifions_H_T hyp thyp =  match !natural_language with
+    French -> sphv [sps"En simplifiant";spb;sps hyp;spb;sps "on obtient:";
+		     spb;spt thyp;sps "."]
+|  English ->  sphv [sps"Simplifying";spb;sps hyp;spb;sps "we get:";
+		     spb;spt thyp;sps "."]
+;;
+
+let grace_a_A_il_suffit_de_montrer_LA arg lg=
+  match !natural_language with
+    French -> sphv ([sps (rand ["Grâce à";"Avec";"A l'aide de"]);spb;
+		      spt arg;sps ",";spb;
+		     sps "il suffit";spb; sps "de"; spb;
+		      sps (rand["prouver";"montrer";"démontrer"]); spb]
+		     @[spv (enumerate (fun x->x) lg)])
+|  English -> sphv ([sps (rand ["Thanks to";"With"]);spb;
+		      spt arg;sps ",";spb;
+		     sps "it suffices";spb; sps "to"; spb;
+		      sps (rand["prove";"show"]); spb]
+		     @[spv (enumerate (fun x->x) lg)])
+;;
+let reste_a_montrer_LA lg=
+  match !natural_language with
+    French -> sphv ([ sps "Il reste";spb; sps "à"; spb;
+		      sps (rand["prouver";"montrer";"démontrer"]); spb]
+		     @[spv (enumerate (fun x->x) lg)])
+|  English -> sphv ([ sps "It remains";spb; sps "to"; spb;
+		      sps (rand["prove";"show"]); spb]
+		     @[spv (enumerate (fun x->x) lg)])
+;;
+(*****************************************************************************)
+(*
+  Traduction des hypothèses.
+*)
+
+type n_sort=
+      Nprop
+    | Nformula
+    | Ntype
+    | Nfunction
+;;
+
+   
+let sort_of_type t ts =
+   let t=(strip_outer_cast t) in
+   if is_Prop t
+   then Nprop
+   else 
+       match ts with
+         Prop(Null) -> Nformula
+        |_ -> (match (kind_of_term t) with
+                IsProd(_,_,_) -> Nfunction
+               |_ -> Ntype)
+;;
+
+let adrel (x,t) e =
+    match x with 
+      Name(xid) -> Environ.push_rel (x,None,t) e
+    | Anonymous -> Environ.push_rel (x,None,t) e
+
+let rec nsortrec vl x = 
+     match (kind_of_term x) with
+     IsProd(n,t,c)->
+        let vl = (adrel (n,t) vl) in nsortrec vl c
+   | IsLambda(n,t,c) ->
+        let vl = (adrel (n,t) vl) in nsortrec vl c
+   | IsApp(f,args) -> nsortrec vl f
+   | IsSort(Prop(Null)) -> Prop(Null)
+   | IsSort(c) -> c
+   | IsMutInd(ind) ->
+          let dmi = lookup_mind_specif ind vl in
+          (mis_sort dmi)
+   | IsMutConstruct(c) ->
+          nsortrec vl (mkMutInd (inductive_of_constructor c))
+   | IsMutCase(_,x,t,a) 
+        -> nsortrec vl x
+   | IsCast(x,t)-> nsortrec vl t
+   | IsConst((c,_))  -> nsortrec vl (lookup_constant c vl).const_type
+   | _ -> nsortrec vl (type_of vl Evd.empty x)
+;;
+let nsort x =
+    nsortrec  (Global.env()) (strip_outer_cast x)
+;;
+
+let sort_of_hyp h = 
+  (sort_of_type h.hyp_type (nsort h.hyp_full_type))
+;;
+
+(* grouper les hypotheses successives de meme type, ou logiques.
+   donne une liste de liste *)
+let rec group_lhyp lh =
+    match lh with
+     [] -> []
+    |[h] -> [[h]]
+    |h::lh -> let (h1::lh1)::lh2 = group_lhyp lh in
+        if h.hyp_type=h1.hyp_type
+          || ((sort_of_hyp h)=(sort_of_hyp h1) && (sort_of_hyp h1)=Nformula)
+        then (h::(h1::lh1))::lh2
+        else [h]::((h1::lh1)::lh2)
+;;
+	
+(* ln noms des hypotheses, lt leurs types *)
+let natural_ghyp (sort,ln,lt) intro =
+  let t=List.hd lt in
+  let nh=List.length ln in
+  let ns=List.hd ln in
+  match sort with
+    Nprop -> soit_A_une_proposition nh ln t
+  | Ntype -> soit_X_un_element_de_T nh ln t
+  | Nfunction -> soit_F_une_fonction_de_type_T nh ln t
+  | Nformula -> 
+      sphv ((sps intro)::(enumerate (fun (n,t) -> tag_hypt n t)
+			    (List.combine ln lt)))
+;;
+
+(* Cas d'une hypothese *)
+let natural_hyp h = 
+   let ns= string_of_id h.hyp_name in
+   let t=h.hyp_type in
+   let ts= (nsort h.hyp_full_type) in
+   natural_ghyp ((sort_of_type t ts),[ns],[t]) (supposons ())
+;;
+
+let rec pr_ghyp lh intro=
+     match lh with
+       [] -> []
+     | [(sort,ln,t)]->
+         (match sort with
+           Nformula -> [natural_ghyp(sort,ln,t) intro; sps ". "]
+         | _ -> [natural_ghyp(sort,ln,t) ""; sps ". "])
+     | (sort,ln,t)::lh  ->
+       let hp= 
+        ([natural_ghyp(sort,ln,t) intro]
+         @(match lh with
+           [] -> [sps ". "]
+          |(sort1,ln1,t1)::lh1  ->
+             match sort1 with
+               Nformula -> 
+                 (let nh=List.length ln in
+                     match sort with
+                   Nprop -> telle_que nh 
+                  |Nfunction -> telle_que nh 
+                  |Ntype -> tel_que nh 
+                  |Nformula -> [sps ". "])
+             | _ -> [sps ". "])) in
+        (sphv hp)::(pr_ghyp lh "")
+;;
+
+(* traduction d'une liste d'hypotheses groupees. *)
+let prnatural_ghyp llh intro=
+  if llh=[]
+  then spe
+  else
+    sphv (pr_ghyp (List.map
+		     (fun lh ->
+		       let h=(List.hd lh) in
+		       let sh = sort_of_hyp h in
+		       let lhname = (List.map (fun h ->
+			 string_of_id h.hyp_name) lh) in
+		       let lhtype = (List.map (fun h -> h.hyp_type) lh) in
+		       (sh,lhname,lhtype))
+		     llh) intro)
+;;
+
+
+(*****************************************************************************)
+(*
+    Liste des hypotheses.
+*)
+type type_info_subgoals_hyp=
+    All_subgoals_hyp
+  | Reduce_hyp
+  | No_subgoals_hyp
+  | Case_subgoals_hyp of string (* word for introduction *)
+	* Term.constr (* variable *)
+        * string (* constructor *)
+        * int (* arity *)
+        * int (* number of constructors *)
+  | Case_prop_subgoals_hyp of string (* word for introduction *)
+	* Term.constr (* variable *)
+        * int (* index of constructor *)
+        * int (* arity *)
+        * int (* number of constructors *)
+  | Elim_subgoals_hyp of Term.constr (* variable *)
+        * string (* constructor *)
+        * int (* arity *)
+        * (string list) (* rec hyp *)
+        * int (* number of constructors *)
+  | Elim_prop_subgoals_hyp of Term.constr (* variable *)
+        * int (* index of constructor *)
+        * int (* arity *)
+        * (string list) (* rec hyp *)
+        * int (* number of constructors *)
+;;
+let rec nrem l n =
+  if n<=0 then l else nrem (list_rem l) (n-1)
+;;
+
+let rec nhd l n =
+  if n<=0 then [] else (List.hd l)::(nhd (list_rem l) (n-1))
+;;
+
+let par_hypothese_de_recurrence () =  match !natural_language with
+    French -> sphv [(prls ["par";"hypothèse";"de";"récurrence";","])]
+| English -> sphv [(prls ["by";"induction";"hypothesis";","])]
+;;
+
+let  natural_lhyp lh hi =
+  match hi with
+    All_subgoals_hyp -> 
+        ( match lh with
+          [] -> spe
+        |_-> prnatural_ghyp (group_lhyp lh) (supposons ()))
+  | Reduce_hyp ->
+      (match lh with
+	[h] -> simplifions_H_T (string_of_id h.hyp_name) h.hyp_type
+      |	_-> spe)
+  | No_subgoals_hyp -> spe
+  |Case_subgoals_hyp (sintro,var,c,a,ncase) -> (* sintro pas encore utilisee *)
+      let s=ref c in
+      for i=1 to a do
+        let nh=(List.nth lh (i-1)) in
+        s:=(!s)^" "^(string_of_id nh.hyp_name);
+      done;
+      if a>0 then s:="("^(!s)^")";
+      sphv [  (if ncase>1
+                     then sph[ sps ("-"^(cas ()));spb]
+                     else spe);
+                    (* spt var;sps "="; *) sps !s; sps ":";
+           (prphrases (natural_hyp) (nrem lh a))]
+  |Case_prop_subgoals_hyp (sintro,var,c,a,ncase) ->
+      prnatural_ghyp (group_lhyp lh) sintro
+  |Elim_subgoals_hyp (var,c,a,lhci,ncase) ->
+      let nlh = List.length lh in
+      let nlhci = List.length lhci in
+      let lh0 = ref [] in
+      for i=1 to (nlh-nlhci) do
+         lh0:=(!lh0)@[List.nth lh (i-1)];
+      done;
+      let lh=nrem lh (nlh-nlhci) in
+      let s=ref c in
+      let lh1=ref [] in
+      for i=1 to nlhci do
+        let targ=(List.nth lhci (i-1))in
+        let nh=(List.nth lh (i-1)) in
+        if targ="arg" || targ="argrec" 
+        then
+            (s:=(!s)^" "^(string_of_id nh.hyp_name);
+	     lh0:=(!lh0)@[nh])
+        else lh1:=(!lh1)@[nh];
+      done;
+      let introhyprec=
+          (if (!lh1)=[] then spe 
+           else   par_hypothese_de_recurrence () )
+      in          
+      if a>0 then s:="("^(!s)^")";
+      spv [sphv [(if ncase>1
+                     then sph[ sps ("-"^(cas ()));spb]
+                     else spe);
+                     sps !s; sps ":"]; 
+           prnatural_ghyp (group_lhyp !lh0) (supposons ());
+           introhyprec;
+           prl (natural_hyp) !lh1]
+  |Elim_prop_subgoals_hyp (var,c,a,lhci,ncase) ->
+      sphv [  (if ncase>1
+                     then sph[ sps ("-"^(cas ()));spb;sps (string_of_int c);
+                             sps ":";spb]
+                     else spe);
+           (prphrases (natural_hyp) lh )]
+
+;;
+
+(*****************************************************************************)
+(*
+    Analyse des tactiques.
+*)
+
+let name_tactic tac =
+      match tac with
+        (Node(_,"Interp",
+		(Node(_,_,
+		      (Node(_,t,_))::_))::_))::_  -> t
+       |(Node(_,t,_))::_ -> t
+;;
+
+let arg1_tactic tac =
+  match tac with
+    (Node(_,"Interp",
+		(Node(_,_,
+		      (Node(_,_,x::_))::_))::_))::_ ->x
+  | (Node(_,_,x::_))::_ -> x
+  | x::_ -> x
+;;
+
+let arg2_tactic tac =
+   match tac with
+     (Node(_,"Interp",
+		(Node(_,_,
+		      (Node(_,_,_::x::_))::_))::_))::_ -> x
+    | (Node(_,_,_::x::_))::_ -> x
+;;
+
+type nat_tactic =
+    Split of (Coqast.t list)
+  | Generalize of (Coqast.t list)
+  | Reduce of string*(Coqast.t list)
+  | Other of string*(Coqast.t list)
+;;
+
+let analyse_tac tac =
+  match tac with
+    [Node (_, "Split", [Node (_, "BINDINGS", [])])]
+      -> Split []
+  | [Node (_, "Split",[Node(_, "BINDINGS",[Node(_, "BINDING",
+	[Node (_, "COMMAND", x)])])])] 
+     -> Split x
+  | [Node (_, "Generalize", [Node (_, "COMMAND", x)])] 
+     ->Generalize x
+  | [Node (_, "Reduce", [Node (_, "REDEXP", [Node (_, mode, _)]);
+             Node (_, "CLAUSE", lhyp)])] 
+     -> Reduce(mode,lhyp)
+  | [Node (_, x,la)] -> Other (x,la)
+;;
+
+      
+
+
+
+
+let id_of_command x = let Node(_,_,Node(_,_,y::_)::_) = x in y
+;;
+type type_info_subgoals =
+    {ihsg: type_info_subgoals_hyp;
+     isgintro : string}
+;;
+
+let rec show_goal lh ig g gs =
+  match ig with
+    "intros" ->
+      if lh = []
+      then spe
+      else show_goal lh "standard" g gs 
+  |"standard" ->
+      (match (sort_of_type g gs) with
+        Nprop -> donnons_une_proposition ()
+      | Nformula -> montrons g
+      | Ntype -> calculons_un_element_de g
+      | Nfunction ->calculons_une_fonction_de_type g)
+  | "apply" -> show_goal lh "" g gs
+  | "simpl" ->en_simplifiant_on_obtient g
+  | "rewrite" -> on_obtient g 
+  | "equality" -> reste_a_montrer g
+  | "trivial_equality" -> reste_a_montrer g
+  | "" -> spe
+  |_ -> sph[ sps "A faire ..."; spb; spt g; sps ". " ]
+;;
+
+let show_goal2 lh {ihsg=hi;isgintro=ig} g gs s =
+  if ig="" && lh = []
+  then spe
+  else sphv [  show_goal lh ig g gs; sps s]
+;;
+
+let imaginez_une_preuve_de () =  match !natural_language with
+    French -> "Imaginez une preuve de"
+| English -> "Imagine a proof of"
+;;
+
+let donnez_un_element_de () =  match !natural_language with
+    French -> "Donnez un element de"
+| English -> "Give an element of";;
+
+let intro_not_proved_goal gs =
+   match gs with
+     Prop(Null) -> imaginez_une_preuve_de ()
+    |_ -> donnez_un_element_de ()
+;;
+
+let first_name_hyp_of_ntree {t_goal={newhyp=lh}}=
+  let {hyp_name=n}::_=lh in n
+;;
+
+let rec find_type x t=
+    match (kind_of_term (strip_outer_cast t)) with
+      IsProd(y,ty,t) ->
+	(match y with
+	  Name y -> 
+            if x=(string_of_id y) then ty
+            else find_type x t
+	| _ -> find_type x t)
+;;
+
+(***********************************************************************
+Traitement des égalités
+*)
+(*
+let is_equality e =
+   match  (kind_of_term e) with
+     IsAppL args ->
+       (match (kind_of_term args.(0)) with
+	 IsConst (c,_) ->
+	   (match (string_of_sp c) with
+	     "Equal" -> true
+           | "eq" -> true
+	   | "eqT" -> true
+	   | "identityT" -> true
+	   | _ -> false)
+       | _ -> false)
+   | _ -> false
+;;
+*)
+
+let is_equality e =
+  let e= (strip_outer_cast e) in
+   match  (kind_of_term e) with
+     IsApp (f,args) -> (Array.length args) >= 3
+   | _ -> false
+;;
+
+let terms_of_equality e =
+  let e= (strip_outer_cast e) in
+  match  (kind_of_term e) with
+     IsApp (f,args) -> (args.(1) , args.(2))
+;;
+
+let eq_term = eq_constr;;
+
+let equalities_ntree ig ntree =
+  let rec equalities_ntree ig ntree =
+  if not (is_equality (concl ntree)) 
+  then []
+  else
+    match (proof ntree) with
+      Notproved ->  [(ig,ntree)]
+    | Proof (tac,ltree) ->
+	if List.mem (name_tactic tac)
+	    ["ERewriteLR";"ERewriteRL"; "ERewriteLRocc";"ERewriteRLocc";
+	      "ERewriteParallel";"ERewriteNormal"; "Reduce";
+	      "RewriteLR";"RewriteRL";
+	      "Replace";"Symmetry";"Reflexivity";
+	      "Exact";"Intros";"Intro";"Auto"]
+      	then (match ltree with
+          [] ->  [(ig,ntree)]
+	| t::_ -> let res=(equalities_ntree ig t) in
+	          if eq_term (concl ntree) (concl t)
+		  then res
+		  else (ig,ntree)::res)
+	else  [(ig,ntree)]
+  in 
+  equalities_ntree ig ntree 
+;;
+
+let remove_seq_of_terms l =
+  let rec remove_seq_of_terms l =    match l with
+    a::b::l -> if (eq_term (fst a) (fst b))
+    then remove_seq_of_terms (b::l)
+    else a::(remove_seq_of_terms (b::l))
+  | _ -> l
+  in remove_seq_of_terms l
+;;
+
+let  list_to_eq l o=
+  let switch = fun h h' -> (if o then h else h') in
+   match l with
+      [a] -> spt (fst a) 
+   |  (a,h)::(b,h')::l ->
+       let rec list_to_eq h l =
+	 match l with
+	   [] -> []
+	 |  (b,h')::l ->
+	     (sph [sps "="; spb; spt b; spb;tag_uselemma (switch h h') spe])
+             :: (list_to_eq (switch h' h) l)
+       in sph [spt a;  spb;
+		 spv ((sph [sps "="; spb; spt b; spb; 
+			     tag_uselemma (switch h h') spe])
+		      ::(list_to_eq (switch h' h) l))]
+;;
+
+let stde = Global.env;;
+
+let dbize env = Astterm.interp_constr Evd.empty env;;
+
+(**********************************************************************)
+let rec natural_ntree ig ntree =
+  let  {t_info=info;
+	 t_goal={newhyp=lh;t_concl=g;t_full_concl=gf;t_full_env=ge};
+	 t_proof=p} = ntree in
+    let leq = List.rev (equalities_ntree ig ntree)  in
+    if List.length leq > 1
+    then (* Several equalities to treate ... *)
+      (
+       print_string("Several equalities to treate ...\n");
+      let l1 = ref [] in
+      let l2 = ref [] in
+      List.iter
+	(fun (_,ntree) ->
+	 let lemma =  match (proof ntree) with
+	   Proof (tac,ltree) ->
+	     (try (sph [spt (dbize (gLOB ge)
+				(term_of_command (arg1_tactic tac)));
+			  (match ltree with
+			    [] ->spe
+			  | [_] -> spe
+			  | _::l -> sphv[sps ": ";
+					  prli (natural_ntree 
+					    {ihsg=All_subgoals_hyp;
+					      isgintro="standard"})
+                            		    l])])
+	      with _ -> sps "simplification"  )
+	 | Notproved -> spe
+	 in
+ 	  let (t1,t2)= terms_of_equality (concl ntree) in
+	  l2:=(t2,lemma)::(!l2);
+	  l1:=(t1,lemma)::(!l1))
+	leq;
+      l1:=remove_seq_of_terms !l1;
+      l2:=remove_seq_of_terms !l2;
+      l2:=List.rev !l2;
+      let ltext=ref [] in
+      if List.length !l1 > 1
+      then (ltext:=(!ltext)@[list_to_eq !l1 true];
+	    if List.length !l2 > 1 then
+	      (ltext:=(!ltext)@[_et()];
+	       ltext:=(!ltext)@[list_to_eq !l2 false]))
+      else if List.length !l2 > 1 then ltext:=(!ltext)@[list_to_eq !l2 false];
+      if !ltext<>[] then ltext:=[sps (bon_a ()); spv !ltext];
+      let (ig,ntree)=(List.hd leq) in
+      spv [(natural_lhyp lh ig.ihsg);
+	    (show_goal2 lh ig g (nsort gf) "");
+	    sph !ltext;
+	    
+	    natural_ntree {ihsg=All_subgoals_hyp;
+                            isgintro=
+			    let  (t1,t2)= terms_of_equality (concl ntree) in
+			    if eq_term t1 t2
+			    then "trivial_equality"
+			    else "equality"}
+	      ntree]
+      	)
+    else
+    let ntext =
+      let gs=nsort gf in
+      match p with
+   	Notproved ->  spv [ (natural_lhyp lh ig.ihsg);
+                            sph [spi; sps (intro_not_proved_goal gs); spb; 
+                                  tag_toprove g  ]
+			  ]
+      | Proof (tac,ltree) -> 
+	 (let tactic= name_tactic tac in
+          let ntext = 
+	  (match tactic with
+(* Pas besoin de l'argument éventuel de la tactique *)
+	    "Intros" -> natural_intros ig lh g gs ltree
+	  | "Intro" -> natural_intros ig lh g gs ltree
+	  | "Idtac" -> natural_ntree ig (List.hd ltree)
+	  | "Fix" -> natural_fix ig lh g gs (arg2_tactic tac) ltree
+	  | "Split" -> natural_split ig lh g gs ge tac ltree
+	  | "Generalize" -> natural_generalize ig lh g gs ge tac ltree
+	  | "Right" -> natural_right ig lh g gs ltree
+	  | "Left" -> natural_left ig lh g gs ltree
+	  | (* "Simpl" *)"Reduce"  -> natural_reduce ig lh g gs ge tac ltree
+	  | "InfoAuto" -> natural_infoauto ig lh g gs ltree
+	  | "Auto" -> natural_auto ig lh g gs ltree
+	  | "EAuto" -> natural_auto ig lh g gs ltree
+	  | "Trivial" -> natural_trivial ig lh g gs ltree
+	  | "Assumption" -> natural_trivial ig lh g gs ltree
+	  | "Clear" -> natural_clear ig lh g gs ltree
+(* Besoin de l'argument de la tactique *)
+	  | "Induction" -> 
+              let arg1=(term_of_command (arg1_tactic tac)) in
+              natural_induction ig lh g gs ge  arg1 ltree false
+	  | "InductionIntro" -> 
+              let arg1=(term_of_command (arg1_tactic tac)) in
+              natural_induction ig lh g gs ge arg1 ltree true
+          | _ ->
+	  let arg1=(term_of_command (arg1_tactic tac)) in
+          let arg1=dbize (gLOB ge) arg1 in
+          (match tactic with
+	    "Apply" -> natural_apply ig lh g gs arg1 ltree
+	  | "Exact" -> natural_exact ig lh g gs arg1 ltree
+	  | "Cut" -> natural_cut ig lh g gs arg1 ltree
+	  | "CutIntro" -> natural_cutintro ig lh g gs arg1 ltree
+	  | "Case" -> natural_case ig lh g gs ge arg1 ltree false
+	  | "CaseIntro" -> natural_case ig lh g gs ge arg1 ltree true
+	  | "Elim" -> natural_elim ig lh g gs ge arg1 ltree false
+	  | "ElimIntro" -> natural_elim ig lh g gs ge arg1 ltree true
+	  | "RewriteRL" -> natural_rewrite ig lh g gs arg1 ltree
+	  | "RewriteLR" -> natural_rewrite ig lh g gs arg1 ltree
+	  | "ERewriteRL" -> natural_rewrite ig lh g gs arg1 ltree
+	  | "ERewriteLR" -> natural_rewrite ig lh g gs arg1 ltree
+	  |_ -> natural_generic ig lh g gs (sps tactic) (prl sp_tac tac) ltree)
+         )
+         in
+          ntext (* spwithtac ntext tactic*)
+          )
+
+    in   
+         if info<>"not_proved"
+         then spshrink info ntext
+         else ntext
+and  natural_generic  ig lh g gs tactic tac ltree =
+  spv
+    [ (natural_lhyp lh ig.ihsg);
+      (show_goal2 lh ig g gs "");
+      on_applique_la_tactique tactic tac ;
+      (prli(natural_ntree  
+	      {ihsg=All_subgoals_hyp;
+		isgintro="standard"})
+         ltree)
+    ]
+and natural_clear ig lh g gs ltree = natural_ntree ig (List.hd ltree)
+(*
+    spv
+    [ (natural_lhyp lh ig.ihsg);
+      (show_goal2 lh ig g gs "");
+      (prl (natural_ntree ig) ltree)
+    ]
+*)
+and natural_intros ig lh g gs ltree =
+  spv
+         [  (natural_lhyp lh ig.ihsg);
+            (show_goal2 lh ig g gs "");
+            (prl (natural_ntree  
+                {ihsg=All_subgoals_hyp;
+                 isgintro="intros"})
+                            ltree)
+        ]
+and natural_apply ig lh g gs arg ltree =
+  let lg = List.map concl ltree in
+  match lg with
+    [] ->
+      spv
+        [ (natural_lhyp lh ig.ihsg);
+	  de_A_il_vient_B arg g  
+        ]
+  | [sg]->
+      spv
+        [ (natural_lhyp lh ig.ihsg);
+          (show_goal2 lh
+	     {ihsg=ig.ihsg; isgintro= if ig.isgintro<>"apply"
+	                              then "standard"
+	                              else ""}
+	     g gs "");
+          grace_a_A_il_suffit_de_montrer_LA arg [spt sg];
+	  sph [spi ; natural_ntree 
+		  {ihsg=All_subgoals_hyp;
+		    isgintro="apply"} (List.hd ltree)]
+	]       
+  | _ ->
+      let ln = List.map (fun _ -> new_name()) lg in
+      spv
+        [ (natural_lhyp lh ig.ihsg);
+          (show_goal2 lh
+	     {ihsg=ig.ihsg; isgintro= if ig.isgintro<>"apply"
+	                              then "standard"
+			              else ""}
+	     g gs "");
+          grace_a_A_il_suffit_de_montrer_LA arg
+	    (List.map2 (fun g n -> sph [sps ("("^n^")"); spb; spt g])
+	       lg ln);
+	  sph [spi; spv (List.map2
+			   (fun x n -> sph [sps ("("^n^"):"); spb;
+					     natural_ntree 
+					       {ihsg=All_subgoals_hyp;
+						 isgintro="apply"} x])
+			   ltree ln)]
+        ]
+and natural_rem_goals ltree =
+  let lg = List.map concl ltree in
+  match lg with
+    [] -> spe
+  | [sg]->
+      spv
+        [ reste_a_montrer_LA [spt sg];
+	  sph [spi ; natural_ntree 
+		  {ihsg=All_subgoals_hyp;
+		    isgintro="apply"} (List.hd ltree)]
+	]       
+  | _ ->
+      let ln = List.map (fun _ -> new_name()) lg in
+      spv
+        [   reste_a_montrer_LA 
+	    (List.map2 (fun g n -> sph [sps ("("^n^")"); spb; spt g])
+	       lg ln);
+	  sph [spi; spv (List.map2
+			   (fun x n -> sph [sps ("("^n^"):"); spb;
+					     natural_ntree 
+					       {ihsg=All_subgoals_hyp;
+						 isgintro="apply"} x])
+			   ltree ln)]
+        ]
+and natural_exact ig lh g gs arg ltree =
+spv
+         [  
+             (natural_lhyp lh ig.ihsg);
+             (let {ihsg=pi;isgintro=ig}= ig in
+               (show_goal2 lh {ihsg=pi;isgintro=""}
+                   g gs ""));
+             (match gs with
+               Prop(Null) -> _A_est_immediat_par_B g arg
+              |_ -> le_resultat_est arg)
+
+        ]
+and natural_cut ig lh g gs arg ltree =
+  spv
+         [  (natural_lhyp lh ig.ihsg);
+             (show_goal2 lh ig g gs "");
+             (prli(natural_ntree  
+                    {ihsg=All_subgoals_hyp;isgintro="standard"})
+                            (List.rev ltree));
+             de_A_on_deduit_donc_B arg g
+        ]
+and natural_cutintro ig lh g gs arg ltree =
+  spv
+         [  (natural_lhyp lh ig.ihsg);
+             (show_goal2 lh ig g gs "");
+             sph [spi;
+                    (natural_ntree  
+                       {ihsg=All_subgoals_hyp;isgintro=""}
+                       (List.nth ltree 1))];
+             sph [spi;
+                    (natural_ntree  
+                       {ihsg=No_subgoals_hyp;isgintro=""}
+                       (List.nth ltree 0))]
+        ]
+and whd_betadeltaiota x = whd_betaiotaevar (Global.env()) Evd.empty x
+and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c)
+and prod_head t =
+  match (kind_of_term (strip_outer_cast t)) with 
+     IsProd(_,_,c) -> prod_head c
+(*    |IsApp(f,a) -> f *)
+    | _ -> t
+and string_of_sp sp = string_of_id (basename sp)
+and  constr_of_mind dmi i = (string_of_id (mis_consnames dmi).(i-1))
+and arity_of_constr_of_mind indf i =
+     (get_constructors indf).(i-1).cs_nargs
+and gLOB ge = Global.env_of_context ge  (* (Global.env()) *)
+
+and natural_case ig lh g gs ge arg1 ltree with_intros =
+ let env= (gLOB ge) in
+ let targ1 = prod_head (type_of env Evd.empty arg1) in
+ let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
+ let ncti= Array.length(get_constructors indf) in
+ let IndFamily(dmi,_) = indf in
+ let ti =(string_of_id (mis_typename dmi)) in
+ let type_arg= targ1 (* List.nth targ (mis_index dmi)*)  in
+ if  ncti<>1
+(* Zéro ou Plusieurs constructeurs *)
+ then (   
+   spv
+         [  (natural_lhyp lh ig.ihsg);
+             (show_goal2 lh ig g gs "");
+             (match (nsort targ1) with
+               Prop(Null) ->
+		 (match ti with
+		   "or" ->  discutons_avec_A type_arg
+                 | _ -> utilisons_A arg1)
+             |_ -> selon_les_valeurs_de_A arg1);
+            (let ci=ref 0 in
+             (prli
+                 (fun treearg -> ci:=!ci+1;
+                      let nci=(constr_of_mind dmi !ci) in
+                      let aci=if with_intros
+			      then (arity_of_constr_of_mind indf !ci)
+		              else 0 in
+                      let ici= (!ci) in
+                    sph[ (natural_ntree  
+                          {ihsg=
+                             (match (nsort targ1) with
+                                Prop(Null) ->
+                                   Case_prop_subgoals_hyp (supposons (),arg1,ici,aci,
+                                     (List.length ltree))
+                               |_-> Case_subgoals_hyp ("",arg1,nci,aci,
+                                                (List.length ltree)));
+                           isgintro= if with_intros then "" else "standard"}
+                          treearg)
+                    ])
+                  (nrem ltree ((List.length ltree)- ncti))));
+	    (sph [spi; (natural_rem_goals
+			  (nhd ltree ((List.length ltree)- ncti)))])
+         ] )
+(* Cas d'un seul constructeur *)
+     else (  
+
+     spv
+     [ (natural_lhyp lh ig.ihsg);
+       (show_goal2 lh ig g gs "");
+       de_A_on_a arg1;
+       (let treearg=List.hd ltree in
+       let nci=(constr_of_mind dmi 1) in
+       let aci=
+	 if with_intros
+         then (arity_of_constr_of_mind indf 1)
+	 else 0 in
+       let ici= 1 in
+       sph[ (natural_ntree  
+               {ihsg=
+                 (match (nsort targ1) with
+                   Prop(Null) ->
+                     Case_prop_subgoals_hyp ("",arg1,1,aci,
+					     (List.length ltree))
+                 |_-> Case_subgoals_hyp ("",arg1,nci,aci,
+                                         (List.length ltree)));
+                 isgintro=""}
+               treearg)
+          ]);
+       (sph [spi; (natural_rem_goals
+		     (nhd ltree ((List.length ltree)- 1)))])
+     ] 
+     )
+(*    with _ ->natural_generic ig lh g gs (sps "Case")  (spt arg1) ltree *)
+
+(*****************************************************************************)
+(*
+   Elim
+*)
+and prod_list_var t =
+   match (kind_of_term (strip_outer_cast t)) with 
+      IsProd(_,t,c) -> t::(prod_list_var c)
+     |_ -> []
+and  hd_is_mind t ti =
+    try (let IndType (indf,targ) = find_rectype (Global.env()) Evd.empty t in
+	     let ncti= Array.length(get_constructors indf) in
+	     let IndFamily(dmi,_) = indf in
+	     (string_of_id (mis_typename dmi)) = ti)
+    with _ -> false
+and mind_ind_info_hyp_constr indf c =
+  let IndFamily(dmi,_) = indf in
+  let p= mis_nparams dmi in
+  let a=arity_of_constr_of_mind indf c in
+  let lp=ref (get_constructors indf).(c).cs_args in
+  let lr=ref [] in
+  let ti = (string_of_id (mis_typename dmi)) in
+  for i=1 to a do
+     match !lp with
+     ((_,_,t)::lp1)->
+       if hd_is_mind t ti
+       then (lr:=(!lr)@["argrec";"hyprec"]; lp:=List.tl lp1)
+       else (lr:=(!lr)@["arg"];lp:=lp1)
+     |  _ -> raise (Failure "mind_ind_info_hyp_constr")
+  done;
+  !lr
+(*
+ mind_ind_info_hyp_constr "le" 2;;
+donne  ["arg"; "argrec"] 
+mind_ind_info_hyp_constr "le" 1;;
+donne []
+ mind_ind_info_hyp_constr "nat" 2;;
+donne ["argrec"]
+*)
+
+and natural_elim ig lh g gs ge arg1 ltree with_intros=
+ let env= (gLOB ge) in
+ let targ1 = prod_head (type_of env Evd.empty arg1) in
+ let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
+ let ncti= Array.length(get_constructors indf) in
+ let IndFamily(dmi,_) = indf in
+ let ti =(string_of_id (mis_typename dmi)) in
+ let type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
+  spv
+         [  (natural_lhyp lh ig.ihsg);
+             (show_goal2 lh ig g gs "");
+             (match (nsort targ1) with
+               Prop(Null) -> utilisons_A arg1
+	     |_ ->procedons_par_recurrence_sur_A arg1);
+            (let ci=ref 0 in
+             (prli
+                 (fun treearg -> ci:=!ci+1;
+                      let nci=(constr_of_mind dmi !ci) in
+                      let aci=(arity_of_constr_of_mind indf !ci) in
+                      let hci=
+			if with_intros
+			then mind_ind_info_hyp_constr indf  !ci
+		      	else [] in
+                      let ici= (!ci) in
+                    sph[ (natural_ntree  
+                          {ihsg=
+                             (match (nsort targ1) with
+                                Prop(Null) ->
+                                   Elim_prop_subgoals_hyp (arg1,ici,aci,hci,
+                                     (List.length ltree))
+                               |_-> Elim_subgoals_hyp (arg1,nci,aci,hci,
+                                                (List.length ltree)));
+                           isgintro= ""}
+                          treearg)
+                    ])
+                  (nhd ltree ncti)));
+	    (sph [spi; (natural_rem_goals (nrem ltree ncti))])
+        ]
+(* )
+  with _ ->natural_generic ig lh g gs (sps "Elim")  (spt arg1) ltree *)
+
+(*****************************************************************************)
+(*
+   InductionIntro n
+*) 
+and natural_induction ig lh g gs ge arg1 ltree with_intros=
+ let env = (gLOB (g_env (List.hd ltree))) in
+ let arg1=dbize env arg1 in
+ let IsVar(arg2)= (kind_of_term arg1) in
+ let targ1 = prod_head (type_of env Evd.empty arg1) in
+ let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
+ let ncti= Array.length(get_constructors indf) in
+ let IndFamily(dmi,_) = indf in
+ let ti =(string_of_id (mis_typename dmi)) in
+ let type_arg= targ1(*List.nth targ (mis_index dmi)*) in
+
+ let lh1= hyps (List.hd ltree) in (* la liste des hyp jusqu'a n *)
+ (* on les enleve des hypotheses des sous-buts *)
+ let ltree = List.map
+     (fun {t_info=info;
+	    t_goal={newhyp=lh;t_concl=g;t_full_concl=gf;t_full_env=ge};
+	    t_proof=p} ->
+	  {t_info=info;
+	    t_goal={newhyp=(nrem lh (List.length lh1));
+		     t_concl=g;t_full_concl=gf;t_full_env=ge};
+	    t_proof=p}) ltree in
+ spv
+   [  (natural_lhyp lh ig.ihsg);
+             (show_goal2 lh ig g gs "");
+	   (natural_lhyp lh1 All_subgoals_hyp);
+             (match (print_string "targ1------------\n";(nsort targ1)) with
+               Prop(Null) -> utilisons_A arg1
+	     |_ -> procedons_par_recurrence_sur_A arg1);
+            (let ci=ref 0 in
+             (prli
+                 (fun treearg -> ci:=!ci+1;
+                      let nci=(constr_of_mind dmi !ci) in
+                      let aci=(arity_of_constr_of_mind indf !ci) in
+                      let hci= 
+			if with_intros
+			then mind_ind_info_hyp_constr indf  !ci
+		      	else [] in
+                      let ici= (!ci) in
+                    sph[ (natural_ntree  
+                          {ihsg=
+                             (match (nsort targ1) with
+                                Prop(Null) ->
+                                   Elim_prop_subgoals_hyp (arg1,ici,aci,hci,
+                                     (List.length ltree))
+                               |_-> Elim_subgoals_hyp (arg1,nci,aci,hci,
+                                                (List.length ltree)));
+                           isgintro= "standard"}
+                          treearg)
+                    ])
+                  ltree))
+        ]
+(***********************************************************************)
+(* Points fixes *)
+
+and natural_fix ig lh g gs arg ltree =
+  let Num(_,narg)=arg in
+  let {t_info=info;
+	t_goal={newhyp=lh1;t_concl=g1;t_full_concl=gf1;
+                   t_full_env=ge1};t_proof=p1}=(List.hd ltree) in
+  let {hyp_name=nfun;hyp_type=tfun}::lh2 = lh1 in
+  let ltree=[{t_info=info;
+	       t_goal={newhyp=lh2;t_concl=g1;t_full_concl=gf1;
+                          t_full_env=ge1};
+	       t_proof=p1}] in
+  spv
+         [  (natural_lhyp lh ig.ihsg);
+             calculons_la_fonction_F_de_type_T_par_recurrence_sur_son_argument_A  nfun tfun narg;
+             (prli(natural_ntree  
+                   {ihsg=All_subgoals_hyp;isgintro=""})
+                            ltree)
+        ]
+and natural_reduce ig lh g gs ge tac ltree =
+  let Reduce (mode,la) = analyse_tac tac in
+  match la with
+    [] -> 
+      spv
+        [  (natural_lhyp lh ig.ihsg);
+          (show_goal2 lh ig g gs ""); 
+          (prl (natural_ntree 
+		  {ihsg=All_subgoals_hyp;isgintro="simpl"})
+             ltree)
+        ]
+  | [Nvar (_,hyp)] ->
+      spv
+        [  (natural_lhyp lh ig.ihsg);
+          (show_goal2 lh ig g gs ""); 
+          (prl (natural_ntree 
+		  {ihsg=Reduce_hyp;isgintro=""})
+             ltree)
+        ]
+and natural_split ig lh g gs ge tac ltree =
+  let Split la = analyse_tac tac in
+  match la with
+    [arg] -> 
+      let env= (gLOB ge) in
+      let arg1= dbize env arg in
+      spv
+      	[ (natural_lhyp lh ig.ihsg);
+          (show_goal2 lh ig g gs ""); 
+	  pour_montrer_G_la_valeur_recherchee_est_A  g arg1;
+          (prl (natural_ntree 
+		  {ihsg=All_subgoals_hyp;isgintro="standard"})
+             ltree)
+        ]
+  | [] ->
+      spv
+        [ (natural_lhyp lh ig.ihsg);
+          (prli(natural_ntree  
+                  {ihsg=All_subgoals_hyp;isgintro="standard"})
+             ltree)
+        ]
+and natural_generalize ig lh g gs ge tac ltree =
+  let Generalize la = analyse_tac tac in
+  match la with
+    [arg] ->
+      let env= (gLOB ge) in
+      let arg1= dbize env arg in
+      let type_arg=type_of_ast ge arg in
+      spv
+      	[ (natural_lhyp lh ig.ihsg);
+          (show_goal2 lh ig g gs ""); 
+	  on_se_sert_de_A   arg1;
+          (prl (natural_ntree 
+		  {ihsg=All_subgoals_hyp;isgintro=""})
+             ltree)
+        ]
+and natural_right ig lh g gs ltree =
+  spv
+         [ (natural_lhyp lh ig.ihsg);
+            (prli(natural_ntree  
+                {ihsg=All_subgoals_hyp;isgintro="standard"})
+                            ltree); 
+            d_ou_A g  
+        ]
+and natural_left ig lh g gs ltree =
+  spv
+         [ (natural_lhyp lh ig.ihsg);
+            (prli(natural_ntree  
+                {ihsg=All_subgoals_hyp;isgintro="standard"})
+                            ltree); 
+             d_ou_A g  
+        ]
+and natural_auto ig lh g gs ltree =
+  match ig.isgintro with
+   "trivial_equality" -> spe
+  | _ -> 
+      if ltree=[]
+      then sphv [(natural_lhyp lh ig.ihsg);
+		  (show_goal2 lh ig g gs "");
+		  coq_le_demontre_seul ()]
+      else spv [(natural_lhyp lh ig.ihsg);
+		 (show_goal2 lh ig g gs "");
+		 (prli (natural_ntree {ihsg=All_subgoals_hyp;isgintro=""}
+			  )
+                    ltree)]
+and natural_infoauto ig lh g gs ltree =
+ match ig.isgintro with
+   "trivial_equality" ->
+     spshrink "trivial_equality"
+       (natural_ntree {ihsg=All_subgoals_hyp;isgintro="standard"}
+		 (List.hd ltree))
+  | _ ->   sphv [(natural_lhyp lh ig.ihsg);
+	 (show_goal2 lh ig g gs "");
+	 coq_le_demontre_seul ();
+       spshrink "auto"
+		    (sph [spi;
+		       (natural_ntree
+			  {ihsg=All_subgoals_hyp;isgintro=""}
+			  (List.hd ltree))])]
+and natural_trivial ig lh g gs ltree =
+  if ltree=[]
+  then sphv [(natural_lhyp lh ig.ihsg);
+	      (show_goal2 lh ig g gs "");
+	      ce_qui_est_trivial () ]
+  else spv [(natural_lhyp lh ig.ihsg);
+	     (show_goal2 lh ig g gs ". ");
+            (prli(natural_ntree  
+                      {ihsg=All_subgoals_hyp;isgintro="standard"})
+                            ltree)]
+and natural_rewrite ig lh g gs arg ltree =
+  spv
+         [  (natural_lhyp lh ig.ihsg);
+             (show_goal2 lh ig g gs "");
+             en_utilisant_l_egalite_A arg;
+            (prli(natural_ntree  
+                 {ihsg=All_subgoals_hyp;isgintro="rewrite"})
+                            ltree)
+        ]
+;;
+
+let natural_ntree_path ig g =
+  Random.init(0);
+        natural_ntree ig g
+;;
+
+let show_proof lang gpath =
+  (match lang with
+     "fr" -> natural_language:=French
+    |"en" -> natural_language:=English
+    | _ -> natural_language:=English);
+  path:=List.rev gpath;
+  name_count:=0;
+  let ntree=(get_nproof ()) in
+  let {t_info=i;t_goal=g;t_proof=p} =ntree in
+  root_of_text_proof
+    (sph [(natural_ntree_path {ihsg=All_subgoals_hyp;
+				isgintro="standard"}
+	                      {t_info="not_proved";t_goal=g;t_proof=p});
+           spr])
+    ;;
+
+let show_nproof path =
+  pP (sp_print (sph [spi; show_proof "fr" path]));;
+
+vinterp_add "ShowNaturalProof"
+	    (fun _ ->
+		 (fun () ->show_nproof[];()));;
+
+(***********************************************************************
+debug sous cygwin:
+
+PATH=/usr/local/bin:/usr/bin:$PATH
+COQTOP=d:/Tools/coq-7avril
+CAMLLIB=/usr/local/lib/ocaml
+CAMLP4LIB=/usr/local/lib/camlp4
+export CAMLLIB
+export COQTOP
+export CAMLP4LIB 
+cd d:/Tools/pcoq/src/text
+d:/Tools/coq-7avril/bin/coqtop.byte.exe -I /cygdrive/D/Tools/pcoq/src/abs_syntax  -I /cygdrive/D/Tools/pcoq/src/text -I /cygdrive/D/Tools/pcoq/src/coq -I /cygdrive/D/Tools/pcoq/src/pbp -I /cygdrive/D/Tools/pcoq/src/dad -I /cygdrive/D/Tools/pcoq/src/history
+
+ 
+ 
+Lemma l1: (A, B : Prop) A \/ B -> B ->  A.
+Intros.
+Elim H.
+Auto.
+Qed.
+ 
+
+Drop.
+
+#use "/cygdrive/D/Tools/coq-7avril/dev/base_include";;
+#load "xlate.cmo";;
+#load "translate.cmo";;
+#load "showproof_ct.cmo";;
+#load "showproof.cmo";;
+#load "pbp.cmo";;
+#load "debug_tac.cmo";;
+#load "name_to_ast.cmo";;
+#load "paths.cmo";;
+#load "dad.cmo";;
+#load "vtp.cmo";;
+#load "history.cmo";;
+#load "centaur.cmo";;
+Xlate.set_xlate_mut_stuff Centaur.globcv;;
+Xlate.declare_in_coq();;
+
+#use "showproof.ml";;
+
+let pproof x = pP (sp_print x);;
+Pp_control.set_depth_boxes 100;;
+#install_printer  pproof;;
+
+ep();;
+let bidon = ref (constr_of_string "O");; 
+
+#trace to_nproof;;
+***********************************************************************)
+let ep()=show_proof "fr" [];;
diff --git a/contrib/interface/showproof.mli b/contrib/interface/showproof.mli
new file mode 100755
index 000000000..22c3b7c4e
--- /dev/null
+++ b/contrib/interface/showproof.mli
@@ -0,0 +1,25 @@
+open Environ
+open Evd
+open Names
+open Stamps
+open Term
+open Util
+open Proof_type
+open Coqast
+open Pfedit
+open Translate
+open Term
+open Reduction
+open Clenv
+open Astterm
+open Typing
+open Inductive
+open Vernacinterp
+open Declarations
+open Showproof_ct
+open Proof_trees
+open Sign
+open Pp
+open Printer
+
+val show_proof : string -> int list -> Ascent.ct_TEXT;;
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
new file mode 100644
index 000000000..e3bca2243
--- /dev/null
+++ b/contrib/interface/showproof_ct.ml
@@ -0,0 +1,185 @@
+(*****************************************************************************)
+(*
+   Vers Ctcoq
+*)
+
+open Esyntax
+open Metasyntax
+open Printer
+open Pp
+open Translate
+open Ascent
+open Vtp
+open Xlate
+
+let ct_text x = CT_coerce_ID_to_TEXT (CT_ident x);;
+
+let sps s =
+  ct_text s
+    ;;
+
+
+let sphs s =
+  ct_text s
+    ;;
+
+let spe = sphs "";;
+let spb = sps " ";;
+let spr = sps "Retour chariot pour Show proof";;
+
+let spnb n = 
+   let s = ref "" in
+   for i=1 to n do s:=(!s)^" "; done; sps !s
+;;
+
+
+let rec spclean l =
+  match l with 
+    [] -> []
+   |x::l -> if x=spe then (spclean l) else x::(spclean l)
+;;
+
+
+let spnb n = 
+   let s = ref "" in
+   for i=1 to n do s:=(!s)^" "; done; sps !s
+;;
+
+let ct_FORMULA_constr = Hashtbl.create 50;;
+
+let stde()  = (Global.env())
+
+;;
+
+let spt t =
+   let f = (translate_constr (stde()) t) in
+   Hashtbl.add ct_FORMULA_constr f t;
+   CT_text_formula f
+;;
+
+
+
+let root_of_text_proof t=
+  CT_text_op [ct_text "root_of_text_proof";
+              t]
+    ;;
+    
+let spshrink info t =
+  CT_text_op [ct_text "shrink";
+	      CT_text_op [ct_text info;
+                          t]]
+;;
+			 
+let spuselemma intro x y =
+  CT_text_op [ct_text "uselemma";
+              ct_text intro;
+	      x;y]
+;;
+
+let sptoprove p t =
+  CT_text_op [ct_text "to_prove";
+	      CT_text_path p;
+              ct_text "goal";
+	      (spt t)]
+;;
+let sphyp p h t =
+  CT_text_op [ct_text "hyp";
+	      CT_text_path p;
+	      ct_text h;
+              (spt t)]
+;;
+let sphypt p h t =
+  CT_text_op [ct_text "hyp_with_type";
+	      CT_text_path p;
+	      ct_text h;
+              (spt t)]
+;;
+
+let spwithtac x t =
+    CT_text_op [ct_text "with_tactic";
+                ct_text t;
+                x]
+;;
+
+
+let spv l =
+   let l= spclean l in
+   CT_text_v l
+;;
+     
+let sph l =
+   let l= spclean l in
+   CT_text_h l
+;;
+
+
+let sphv l =
+   let l= spclean l in
+   CT_text_hv l
+;;
+
+let rec prlist_with_sep f g l =
+    match l with 
+      [] -> hOV 0 [< >]
+     |x::l1 -> hOV 0 [< (g x); (f ()); (prlist_with_sep f g l1)>]
+;;
+   
+let rec sp_print x = 
+   match x with
+     CT_coerce_ID_to_TEXT (CT_ident s)
+     -> (match s with
+       "\n" -> [< 'fNL >]
+     | "Retour chariot pour Show proof" -> [< 'fNL >]
+     |_ -> [< 'sTR s >])
+   | CT_text_formula  f -> [< prterm (Hashtbl.find ct_FORMULA_constr f) >]
+  |  CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
+	      CT_text_path (CT_signed_int_list p);
+              CT_coerce_ID_to_TEXT (CT_ident "goal");
+	      g] ->
+      let p=(List.map (fun y -> match y with
+	                 (CT_coerce_INT_to_SIGNED_INT
+			      (CT_int x)) -> x
+		       | _ -> raise (Failure "sp_print")) p) in
+      h 0 [<  'sTR "<b>"; sp_print g; 'sTR "</b>">]
+ |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "uselemma");
+              CT_coerce_ID_to_TEXT (CT_ident intro);
+	      l;g] ->
+      h 0 [< 'sTR ("<i>("^intro^" "); sp_print l; 'sTR ")</i>"; sp_print g>]
+ |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp");
+	      CT_text_path (CT_signed_int_list p);
+	      CT_coerce_ID_to_TEXT (CT_ident hyp);
+              g]  ->
+      let p=(List.map (fun y -> match y with
+	                  (CT_coerce_INT_to_SIGNED_INT
+			      (CT_int x)) -> x
+		       | _ -> raise (Failure "sp_print")) p) in
+            h 0 [< 'sTR hyp>]
+
+  |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp_with_type");
+	      CT_text_path (CT_signed_int_list p);
+	      CT_coerce_ID_to_TEXT (CT_ident hyp);
+              g]  ->
+      let p=(List.map (fun y -> match y with
+                         (CT_coerce_INT_to_SIGNED_INT
+			      (CT_int x)) -> x
+		       | _ -> raise (Failure "sp_print")) p) in
+      h 0 [< sp_print g; 'sPC; 'sTR "<i>("; 'sTR hyp;'sTR ")</i>">]   
+
+  | CT_text_h l ->
+      h 0 [< prlist_with_sep (fun () -> [< >])
+		(fun y -> sp_print y) l>]
+  | CT_text_v l ->
+      v 0 [< prlist_with_sep (fun () -> [< >])
+		(fun y -> sp_print y) l>]
+  | CT_text_hv l ->
+      h 0 [< prlist_with_sep (fun () -> [<>])
+		(fun y -> sp_print y) l>]
+  | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "shrink");
+	      CT_text_op [CT_coerce_ID_to_TEXT (CT_ident info); t]]  ->
+                   h 0 [< 'sTR ("("^info^": "); sp_print t ;'sTR ")" >]
+  | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "root_of_text_proof");
+              t]->
+                    sp_print t 
+  | _ -> [< 'sTR "..." >]
+;;
+  
diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli
index 41c33d5a3..46d785f4b 100644
--- a/contrib/interface/translate.mli
+++ b/contrib/interface/translate.mli
@@ -6,3 +6,4 @@ open Term;;
 
 val translate_goal : goal -> ct_RULE;;
 val translate_constr : env -> constr -> ct_FORMULA;;
+val translate_path : int list -> ct_SIGNED_INT_LIST;;
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 79d4d68ad..e35b9d3bc 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -336,6 +336,14 @@ and fCOMMAND = function
    fID x1;
    fIN_OR_OUT_MODULES x2;
    fNODE "search" 2
+| CT_search_pattern(x1, x2) ->
+   fFORMULA x1;
+   fIN_OR_OUT_MODULES x2;
+   fNODE "search_pattern" 2
+| CT_search_rewrite(x1, x2) ->
+   fFORMULA x1;
+   fIN_OR_OUT_MODULES x2;
+   fNODE "search_rewrite" 2
 | CT_section_end(x1) ->
    fID x1;
    fNODE "section_end" 1
@@ -1216,6 +1224,26 @@ and fTARG_LIST = function
 | CT_targ_list l ->
    (List.iter fTARG l);
    fNODE "targ_list" (List.length l)
+and fTEXT = function
+| CT_coerce_ID_to_TEXT x -> fID x
+| CT_text_formula(x1) ->
+   fFORMULA x1;
+   fNODE "text_formula" 1
+| CT_text_h l ->
+   (List.iter fTEXT l);
+   fNODE "text_h" (List.length l)
+| CT_text_hv l ->
+   (List.iter fTEXT l);
+   fNODE "text_hv" (List.length l)
+| CT_text_op l ->
+   (List.iter fTEXT l);
+   fNODE "text_op" (List.length l)
+| CT_text_path(x1) ->
+   fSIGNED_INT_LIST x1;
+   fNODE "text_path" 1
+| CT_text_v l ->
+   (List.iter fTEXT l);
+   fNODE "text_v" (List.length l)
 and fTHEOREM_GOAL = function
 | CT_goal(x1) ->
    fFORMULA x1;
diff --git a/contrib/interface/vtp.mli b/contrib/interface/vtp.mli
index 6fe256ab2..fe30b317a 100644
--- a/contrib/interface/vtp.mli
+++ b/contrib/interface/vtp.mli
@@ -12,3 +12,4 @@ 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
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 326079633..a616d2190 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -189,6 +189,7 @@ let coerce_iVARG_to_FORMULA =
  function
     | Varg_constr x -> x
     | Varg_sorttype x -> CT_coerce_SORT_TYPE_to_FORMULA x
+    | Varg_ident id -> CT_coerce_ID_to_FORMULA id
     | _ -> xlate_error "coerce_iVARG_to_FORMULA: unexpected argument";;
 
 let coerce_iVARG_to_ID =
@@ -1287,8 +1288,8 @@ and xlate_tac =
      CT_reduce (id, l)
     | "Apply", ((Targ_command c) :: (bindl :: [])) ->
      CT_apply (c, strip_targ_spec_list bindl)
-    | "Constructor", ((Targ_int n) :: bindl) ->
-     CT_constructor (n, filter_binding_or_command_list bindl)
+    | "Constructor", ((Targ_int n) :: (bindl :: [])) ->
+     CT_constructor (n, strip_targ_spec_list bindl)
     | "Specialize",
         ((Targ_int n) :: ((Targ_command c) :: ((Targ_spec_list sl) :: []))) ->
      CT_specialize (CT_coerce_INT_to_INT_OPT n, c, sl)
@@ -1466,11 +1467,12 @@ let build_constructors l =
 let build_record_field_list l =
  let build_record_field =
   function
-     | Varg_varglist ((Varg_string (CT_string "")) ::
-                       ((Varg_ident id) :: (c :: []))) ->
+     | Varg_varglist ((Varg_string (CT_string "")) ::((Varg_string assum) ::
+                       ((Varg_ident id) :: (c :: [])))) ->
       CT_coerce_CONSTR_to_RECCONSTR (CT_constr (id, coerce_iVARG_to_FORMULA c))
-     | Varg_varglist ((Varg_string (CT_string "COERCION")) ::
-                       ((Varg_ident id) :: (c :: []))) ->
+     | Varg_varglist ((Varg_string (CT_string "COERCION")) 
+                       ::((Varg_string assum) ::
+                       ((Varg_ident id) :: (c :: [])))) ->
       CT_constr_coercion (id, coerce_iVARG_to_FORMULA c)
      | _ -> xlate_error "unexpected field in build_record_field_list" in
  CT_recconstr_list (List.map build_record_field l);;
@@ -1544,6 +1546,8 @@ let rec cvt_varg =
      | "Pos" -> Varg_sorttype (CT_sortc "Set")
      | "Null" -> Varg_sorttype (CT_sortc "Prop")
      | _ -> xlate_error "cvt_varg : PROP : Failed match ")
+    | Node (_, "CONSTR", ((Node (_, "PROP", [])) :: [])) ->
+     Varg_sorttype (CT_sortc "Prop")
     | Node (_, "CONSTR", ((Node (_, "TYPE", [])) :: [])) ->
      Varg_sorttype (CT_sortc "Type")
     | Node (_, "CONSTR", [c]) -> Varg_constr (xlate_formula c)
@@ -1709,10 +1713,18 @@ and xlate_vernac =
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
      | "DefinedNamed", [] ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Definition"), ctv_ID_OPT_NONE)
-     | "SaveAnonymousThm", ((Varg_ident s) :: []) ->
+     | "SaveAnonymous", [Varg_string (CT_string kind); Varg_ident s] ->
+	let kind_string = 
+	  match kind with
+	      "THEOREM" -> "Theorem"
+	    | "LEMMA" -> "Lemma"
+	    | "FACT" -> "Fact"
+	    | "REMARK" -> "Remark"
+	    | "DECL" -> "Decl"
+	    | _ -> assert false in
+      CT_save (CT_coerce_THM_to_THM_OPT (CT_thm kind_string), ctf_ID_OPT_SOME s)
+     | "SaveAnonymous", [Varg_ident s] ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctf_ID_OPT_SOME s)
-     | "SaveAnonymousRmk", ((Varg_ident s) :: []) ->
-      CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Remark"), ctf_ID_OPT_SOME s)
      | "TRANSPARENT", (id :: idl) ->
             CT_transparent(CT_id_ne_list(strip_varg_ident id,
                    List.map strip_varg_ident idl))
@@ -1784,6 +1796,20 @@ and xlate_vernac =
       CT_variable (xlate_var kind, b)
      | "Check", ((Varg_string (CT_string kind)) :: (c :: [])) ->
       CT_check (coerce_iVARG_to_FORMULA c)
+     | "SearchPattern",Varg_constr c::l ->
+          (match l with
+	     | [] -> CT_search_pattern(c, 
+                            CT_coerce_NONE_to_IN_OR_OUT_MODULES CT_none)
+	     | (Varg_string (CT_string x))::(Varg_ident m1)::l1 ->
+		 let l2 = CT_id_ne_list(m1, List.map coerce_iVARG_to_ID l1) in
+                 let modifier = 
+		   (match x with
+		      | "inside" -> CT_in_modules l2
+		      | "outside" -> CT_out_modules l2
+		      | _ -> xlate_error "bad extra argument for Search") in
+		   CT_search_pattern(c, modifier)
+	     | _ -> xlate_error "bad argument list for SearchPattern")
+
      | "SEARCH", (Varg_ident id):: l -> 
           (match l with
 	     | [] -> CT_search(id, CT_coerce_NONE_to_IN_OR_OUT_MODULES CT_none)
@@ -1801,7 +1827,7 @@ and xlate_vernac =
        "RECORD",
          ((Varg_string coercion_or_not) :: ((Varg_ident s) ::
            ((Varg_binderlist binders) ::
-             ((Varg_sorttype c) ::
+             (c1 ::
                ((Varg_varglist rec_constructor_or_none) ::
                  ((Varg_varglist field_list) :: [])))))) ->
       let record_constructor =
@@ -1813,7 +1839,11 @@ and xlate_vernac =
        ((match coercion_or_not with CT_string "" ->
           CT_coerce_NONE_to_COERCION_OPT(CT_none)
         | _ -> CT_coercion_atm),
-        s, binders, c, record_constructor,
+        s, binders, 
+        (match c1 with (Varg_sorttype c) -> c
+        |(Varg_constr (CT_coerce_SORT_TYPE_to_FORMULA c)) -> c
+        | _ -> assert false),
+         record_constructor,
          build_record_field_list field_list)
      | (*Inversions from tactics/Inv.v *)
        "MakeSemiInversionLemmaFromHyp",
@@ -1963,19 +1993,19 @@ and xlate_vernac =
      | "SETHYPSLIMIT", ((Varg_int n) :: []) -> CT_sethyp n
      | "UNSETHYPSLIMIT", [] -> CT_unsethyp
      | "COERCION",
-         ((Varg_string s) ::
+         ((Varg_string (CT_string s)) ::
            ((Varg_string (CT_string str)) ::
              ((Varg_ident id1) :: ((Varg_ident id2) :: ((Varg_ident id3) :: []))))) ->
       let id_opt =
        match str with
        | "IDENTITY" -> CT_identity
        | "" -> CT_coerce_NONE_to_IDENTITY_OPT CT_none
-       | _ -> xlate_error "unknown flag for a coercion" in
+       | _ -> xlate_error "unknown flag for a coercion1" in
       let local_opt =
-       match str with
+       match s with
        | "LOCAL" -> CT_local
        | "" -> CT_coerce_NONE_to_LOCAL_OPT CT_none
-       | _ -> xlate_error "unknown flag for a coercion" in
+       | _ -> xlate_error "unknown flag for a coercion2" in
       CT_coercion (local_opt, id_opt, id1, id2, id3)
      | "CLASS", (_ :: ((Varg_ident id1) :: [])) -> CT_class id1
      | "PrintGRAPH", [] -> CT_print_graph