Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 1899 insertions, 0 deletions

diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
new file mode 100644
index 00000000..5b265ec8
--- /dev/null
+++ b/contrib/interface/showproof.ml
@@ -0,0 +1,1899 @@
+(*
+#use "/cygdrive/D/Tools/coq-7avril/dev/base_include";;
+open Coqast;;
+*)
+open Environ
+open Evd
+open Names
+open Nameops
+open Libnames
+open Term
+open Termops
+open Util
+open Proof_type
+open Coqast
+open Pfedit
+open Translate
+open Term
+open Reductionops
+open Clenv
+open Typing
+open Inductive
+open Inductiveops
+open Vernacinterp
+open Declarations
+open Showproof_ct
+open Proof_trees
+open Sign
+open Pp
+open Printer
+open Rawterm
+open Tacexpr
+open Genarg
+(*****************************************************************************)
+(*
+   Arbre de preuve maison:
+   
+*)
+
+(* hypotheses *)
+
+type nhyp = {hyp_name : identifier;
+             hyp_type : Term.constr;
+             hyp_full_type: Term.constr}
+;;
+
+type ntactic = tactic_expr
+;;
+
+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 ni = match n with Name ni -> ni | _ -> assert false 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 (TacArg (Tacexp t),_) -> true  
+   |  Tactic (TacAtom (_,TacAuto _), _) -> true
+   |  Tactic (TacAtom (_,TacSymmetry _), _) -> 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 (Refine 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
+          | _ -> assert false)
+
+   else [rast ]
+;;
+*)
+let rule_to_ntactic r =
+   let rt =
+     (match r with
+       Tactic (t,_) -> t
+     | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h)
+     | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in
+   if rule_is_complex r
+   then (match rt with
+           TacArg (Tacexp _) as t -> t
+          | _ -> assert false)
+
+   else rt
+;;
+
+(*
+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_named 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_named 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} = 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= to_nproof_rec sigma sign (subproof_of_proof pf) in
+          let ntree= fill_unproved p1 
+              (List.map (fun x -> (to_nproof_rec sigma sign x).t_proof)
+		 spfl) in
+	  (match r with
+	    Tactic (TacAtom (_, TacAuto _),_) ->
+	      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 (TacAtom (dummy_loc,TacExtend (dummy_loc,"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"
+    |"Let" -> "Let"
+    | 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)
+      | _ -> assert false)
+  in enum_rec f ln
+;;
+
+
+let constr_of_ast = Constrintern.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 sp_tac tac = failwith "TODO"
+
+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
+                Prod(_,_,_) -> 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
+     Prod(n,t,c)->
+        let vl = (adrel (n,t) vl) in nsortrec vl c
+   | Lambda(n,t,c) ->
+        let vl = (adrel (n,t) vl) in nsortrec vl c
+   | App(f,args) -> nsortrec vl f
+   | Sort(Prop(Null)) -> Prop(Null)
+   | Sort(c) -> c
+   | Ind(ind) ->
+          let (mib,mip) = lookup_mind_specif vl ind in
+          mip.mind_sort
+   | Construct(c) ->
+          nsortrec vl (mkInd (inductive_of_constructor c))
+   | Case(_,x,t,a) 
+        -> nsortrec vl x
+   | Cast(x,t)-> nsortrec vl t
+   | Const 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 ->
+      match group_lhyp lh with
+       (h1::lh1)::lh2 -> 
+        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)
+     |_-> assert false
+;;
+	
+(* 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
+       | _ -> assert false
+;;
+*)
+let name_tactic = function
+  | TacIntroPattern _ -> "Intro"
+  | TacAssumption -> "Assumption"
+  | _ -> failwith "TODO"
+;;
+
+(*
+let arg1_tactic tac =
+  match tac with
+    (Node(_,"Interp",
+		(Node(_,_,
+		      (Node(_,_,x::_))::_))::_))::_ ->x
+  | (Node(_,_,x::_))::_ -> x
+  | x::_ -> x
+  | _ -> assert false
+;;
+*)
+
+let arg1_tactic tac = failwith "TODO"
+
+let arg2_tactic tac =
+   match tac with
+     (Node(_,"Interp",
+		(Node(_,_,
+		      (Node(_,_,_::x::_))::_))::_))::_ -> x
+    | (Node(_,_,_::x::_))::_ -> x
+    | _ -> assert false
+;;
+
+(*
+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)
+  | _ -> assert false
+;;
+*)
+      
+
+
+
+
+let id_of_command x =
+  match x with
+      Node(_,_,Node(_,_,y::_)::_) ->  y
+     |_ -> assert false
+;;
+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}}=
+  match lh with
+   {hyp_name=n}::_ -> n
+  | _ -> assert false
+;;
+
+let rec find_type x t=
+    match (kind_of_term (strip_outer_cast t)) with 
+      Prod(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)
+     |_-> assert false 
+;;
+
+(***********************************************************************
+Traitement des égalités
+*)
+(*
+let is_equality e =
+   match  (kind_of_term e) with
+     AppL args ->
+       (match (kind_of_term args.(0)) with
+	 Const (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
+     App (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
+     App (f,args) -> (args.(1) , args.(2))
+    | _ -> assert false
+;;
+
+let eq_term = eq_constr;;
+
+let is_equality_tac = function
+  | TacAtom (_,
+      (TacExtend
+	(_,("ERewriteLR"|"ERewriteRL"|"ERewriteLRocc"|"ERewriteRLocc"
+	 |"ERewriteParallel"|"ERewriteNormal"
+	 |"RewriteLR"|"RewriteRL"|"Replace"),_)
+      | TacReduce _
+      | TacSymmetry _ | TacReflexivity
+      | TacExact _ | TacIntroPattern _ | TacIntroMove _ | TacAuto _)) -> true
+  | _ -> false
+
+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 is_equality_tac tac
+      	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))]
+  | _ -> assert false
+;;
+
+let stde = Global.env;;
+
+let dbize env = Constrintern.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) (arg1_tactic tac));(* TODO *)
+			  (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 (TacId _,ltree) -> natural_ntree ig (List.hd ltree)
+      | Proof (TacAtom (_,tac),ltree) -> 
+	 (let ntext = 
+	  match tac with
+(* Pas besoin de l'argument éventuel de la tactique *)
+	    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
+	  | 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
+	  | (* "Simpl" *)TacReduce (r,cl)  ->
+	      natural_reduce ig lh g gs ge r cl ltree
+	  | TacExtend (_,"InfoAuto",[]) -> natural_infoauto ig lh g gs ltree
+	  | TacAuto _ -> natural_auto ig lh g gs ltree
+	  | TacExtend (_,"EAuto",_) -> natural_auto ig lh g gs ltree
+	  | TacTrivial _ -> natural_trivial ig lh g gs ltree
+	  | TacAssumption -> natural_trivial ig lh g gs ltree
+	  | TacClear _ -> natural_clear ig lh g gs ltree
+(* Besoin de l'argument de la tactique *)
+	  | TacSimpleInduction (NamedHyp id,_) -> 
+              natural_induction ig lh g gs ge id ltree false
+	  | 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
+	  | 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
+	  | 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
+	  | TacExtend (_,"ElimIntro",[a]) ->
+	      let c = out_gen wit_constr a in
+	      natural_elim ig lh g gs ge c ltree true
+	  | TacExtend (_,"Rewrite",[_;a]) ->
+	      let (c,_) = out_gen wit_constr_with_bindings a in
+	      natural_rewrite ig lh g gs c ltree
+	  | TacExtend (_,"ERewriteRL",[a]) ->
+	      let c = out_gen wit_constr a in (* TODO *)
+	      natural_rewrite ig lh g gs c ltree
+	  | TacExtend (_,"ERewriteLR",[a]) ->
+	      let c = out_gen wit_constr a in (* TODO *)
+	      natural_rewrite ig lh g gs c ltree
+	  |_ -> natural_generic ig lh g gs (sps (name_tactic tac)) (prl sp_tac [tac]) ltree
+         in
+          ntext (* spwithtac ntext tactic*)
+          )
+      | Proof _ -> failwith "Don't know what to do with that"
+    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 
+     Prod(_,_,c) -> prod_head c
+(*    |App(f,a) -> f *)
+    | _ -> t
+and string_of_sp sp = string_of_id (basename sp)
+and constr_of_mind mip i =
+  (string_of_id mip.mind_consnames.(i-1))
+and arity_of_constr_of_mind env indf i =
+     (get_constructors env 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 env indf) in
+ let (ind,_) = dest_ind_family indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let ti =(string_of_id mip.mind_typename) 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 mip !ci) in
+                      let aci=if with_intros
+			      then (arity_of_constr_of_mind env 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 mip 1) in
+       let aci=
+	 if with_intros
+         then (arity_of_constr_of_mind env 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 
+      Prod(_,t,c) -> t::(prod_list_var c)
+     |_ -> []
+and  hd_is_mind t ti =
+    try (let env = Global.env() in
+         let IndType (indf,targ) = find_rectype env Evd.empty t in
+	 let ncti= Array.length(get_constructors env indf) in
+	 let (ind,_) = dest_ind_family indf in
+         let (mib,mip) = lookup_mind_specif env ind in
+	 (string_of_id mip.mind_typename) = ti)
+    with _ -> false
+and mind_ind_info_hyp_constr indf c =
+  let env = Global.env() in
+  let (ind,_) = dest_ind_family indf in
+  let (mib,mip) = lookup_mind_specif env ind in
+  let p = mip.mind_nparams in
+  let a = arity_of_constr_of_mind env indf c in
+  let lp=ref (get_constructors env indf).(c).cs_args in
+  let lr=ref [] in
+  let ti = (string_of_id mip.mind_typename) 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 env indf) in
+ let (ind,_) = dest_ind_family indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let ti =(string_of_id mip.mind_typename) 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 mip !ci) in
+                      let aci=(arity_of_constr_of_mind env 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 arg2 ltree with_intros=
+ let env = (gLOB (g_env (List.hd ltree))) in
+ let arg1= mkVar arg2 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 env indf) in
+ let (ind,_) = dest_ind_family indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let ti =(string_of_id mip.mind_typename) 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 mip !ci) in
+                      let aci=(arity_of_constr_of_mind env 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 narg ltree =
+  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
+  match lh1 with
+     {hyp_name=nfun;hyp_type=tfun}::lh2 ->
+  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)
+        ]
+   | _ -> assert false
+and natural_reduce ig lh g gs ge mode la ltree =
+  match la with
+    {onhyps=Some[];onconcl=true} -> 
+      spv
+        [  (natural_lhyp lh ig.ihsg);
+          (show_goal2 lh ig g gs ""); 
+          (prl (natural_ntree 
+		  {ihsg=All_subgoals_hyp;isgintro="simpl"})
+             ltree)
+        ]
+  | {onhyps=Some[hyp]; onconcl=false} ->
+      spv
+        [  (natural_lhyp lh ig.ihsg);
+          (show_goal2 lh ig g gs ""); 
+          (prl (natural_ntree 
+		  {ihsg=Reduce_hyp;isgintro=""})
+             ltree)
+        ]
+  | _ -> assert false
+and natural_split ig lh g gs ge la ltree =
+  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)
+        ]
+  | _ -> assert false
+and natural_generalize ig lh g gs ge la ltree =
+  match la with
+    [arg] ->
+      let env= (gLOB ge) in
+      let arg1= (*dbize env*) arg in
+      let type_arg=type_of (Global.env()) Evd.empty 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)
+        ]
+    | _ -> assert false
+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" [];;