Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

46 files changed, 2339 insertions, 1704 deletions

diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index 1ffa347a..d336f599 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccproof.ml 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: ccproof.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
 
 (* This file uses the (non-compressed) union-find structure to generate *) 
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
@@ -16,58 +16,107 @@ open Names
 open Term
 open Ccalgo
   
-type proof=
+type rule=
     Ax of constr
   | SymAx of constr
   | Refl of term
   | Trans of proof*proof
   | Congr of proof*proof
   | Inject of proof*constructor*int*int 
-		  
-let pcongr=function
-    Refl t1, Refl t2 -> Refl (Appli (t1,t2))
-  | p1, p2 -> Congr (p1,p2)
-
-let rec ptrans=function
-    Refl _, p ->p
-  | p, Refl _ ->p
-  | Trans(p1,p2), p3 ->ptrans(p1,ptrans (p2,p3))
-  | Congr(p1,p2), Congr(p3,p4) ->pcongr(ptrans(p1,p3),ptrans(p2,p4))
-  | Congr(p1,p2), Trans(Congr(p3,p4),p5) ->
-      ptrans(pcongr(ptrans(p1,p3),ptrans(p2,p4)),p5)
-  | p1, p2 ->Trans (p1,p2)
-	
-let rec psym=function
-    Refl p->Refl p
-  | SymAx s->Ax s
-  | Ax s-> SymAx s
-  | Inject (p,c,n,a)-> Inject (psym p,c,n,a)
-  | Trans (p1,p2)-> ptrans (psym p2,psym p1)
-  | Congr (p1,p2)-> pcongr (psym p1,psym p2)
+and proof = 
+    {p_lhs:term;p_rhs:term;p_rule:rule}
+
+let prefl t = {p_lhs=t;p_rhs=t;p_rule=Refl t}
+
+let pcongr p1 p2 = 
+  match p1.p_rule,p2.p_rule with 
+    Refl t1, Refl t2 -> prefl (Appli (t1,t2))
+  | _, _ -> 
+      {p_lhs=Appli (p1.p_lhs,p2.p_lhs);
+       p_rhs=Appli (p1.p_rhs,p2.p_rhs);
+       p_rule=Congr (p1,p2)}
+
+let rec ptrans p1 p3=
+  match p1.p_rule,p3.p_rule with
+      Refl _, _ ->p3
+    | _, Refl _ ->p1
+    | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3)
+    | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4)
+    | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
+	ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
+  | _, _ -> 
+      if p1.p_rhs = p3.p_lhs then 
+	{p_lhs=p1.p_lhs;
+	 p_rhs=p3.p_rhs;
+	 p_rule=Trans (p1,p3)}
+      else anomaly "invalid cc transitivity"
 	
-let pcongr=function
-    Refl t1, Refl t2 ->Refl (Appli (t1,t2))
-  | p1, p2 -> Congr (p1,p2)
+let rec psym p = 
+  match p.p_rule with 
+      Refl _ -> p 
+    | SymAx s ->
+	{p_lhs=p.p_rhs;
+	 p_rhs=p.p_lhs;
+	 p_rule=Ax s}
+    | Ax s->      
+	{p_lhs=p.p_rhs;
+	 p_rhs=p.p_lhs;
+	 p_rule=SymAx s}
+  | Inject (p0,c,n,a)-> 
+      {p_lhs=p.p_rhs;
+       p_rhs=p.p_lhs;
+       p_rule=Inject (psym p0,c,n,a)}
+  | Trans (p1,p2)-> ptrans (psym p2) (psym p1)
+  | Congr (p1,p2)-> pcongr (psym p1) (psym p2)
+
+let pax axioms s =
+  let l,r = Hashtbl.find axioms s in
+    {p_lhs=l;
+     p_rhs=r;
+     p_rule=Ax s}
+
+let psymax axioms s =
+  let l,r = Hashtbl.find axioms s in
+    {p_lhs=r;
+     p_rhs=l;
+     p_rule=SymAx s}
+
+let rec nth_arg t n=
+  match t with 
+      Appli (t1,t2)-> 
+	if n>0 then 
+	  nth_arg t1 (n-1)
+	else t2
+    | _ -> anomaly "nth_arg: not enough args"
+
+let pinject p c n a =
+  {p_lhs=nth_arg p.p_lhs (n-a);
+   p_rhs=nth_arg p.p_rhs (n-a);
+   p_rule=Inject(p,c,n,a)}
 
 let build_proof uf=
-  
+
+  let axioms = axioms uf in
+
   let rec equal_proof i j=
-    if i=j then Refl (term uf i) else 
+    if i=j then prefl (term uf i) else 
       let (li,lj)=join_path uf i j in
-	ptrans (path_proof i li,psym (path_proof j lj))
+	ptrans (path_proof i li) (psym (path_proof j lj))
   
   and edge_proof ((i,j),eq)=
     let pi=equal_proof i eq.lhs in
     let pj=psym (equal_proof j eq.rhs) in
     let pij=
       match eq.rule with 
-	  Axiom (s,reversed)->if reversed then SymAx s else Ax s
+	  Axiom (s,reversed)->
+	    if reversed then psymax axioms s 
+	    else pax axioms s
 	| Congruence ->congr_proof eq.lhs eq.rhs
 	| Injection (ti,ipac,tj,jpac,k) ->
 	    let p=ind_proof ti ipac tj jpac in
 	    let cinfo= get_constructor_info uf ipac.cnode in
-	      Inject(p,cinfo.ci_constr,cinfo.ci_nhyps,k)	
-    in  ptrans(ptrans (pi,pij),pj)
+	      pinject p cinfo.ci_constr cinfo.ci_nhyps k	
+    in  ptrans (ptrans pi pij) pj
 
   and constr_proof i t ipac=
     if ipac.args=[] then
@@ -79,49 +128,26 @@ let build_proof uf=
       let rj=find uf j in
       let u=find_pac uf rj npac in
       let p=constr_proof j u npac in
-	ptrans (equal_proof i t, pcongr (p,Refl targ))
+	ptrans (equal_proof i t) (pcongr p (prefl targ))
 
   and path_proof i=function
-      [] -> Refl (term uf i)
-    | x::q->ptrans (path_proof (snd (fst x)) q,edge_proof x)
+      [] -> prefl (term uf i)
+    | x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x)
   
   and congr_proof i j=
     let (i1,i2) = subterms uf i
     and (j1,j2) = subterms uf j in   
-      pcongr (equal_proof i1 j1, equal_proof i2 j2)
+      pcongr (equal_proof i1 j1) (equal_proof i2 j2)
 	
   and ind_proof i ipac j jpac=
     let p=equal_proof i j 
     and p1=constr_proof i i ipac 
     and p2=constr_proof j j jpac in
-      ptrans(psym p1,ptrans(p,p2))
+      ptrans (psym p1) (ptrans p p2)
   in
     function
 	`Prove (i,j) -> equal_proof i j
       | `Discr (i,ci,j,cj)-> ind_proof i ci j cj
 
-let rec nth_arg t n=
-  match t with 
-      Appli (t1,t2)-> 
-	if n>0 then 
-	  nth_arg t1 (n-1)
-	else t2
-    | _ -> anomaly "nth_arg: not enough args"
 
-let rec type_proof axioms p=
-  match p with
-      Ax s->Hashtbl.find axioms s
-    | SymAx s-> let (t1,t2)=Hashtbl.find axioms s in (t2,t1)
-    | Refl t-> t,t
-    | Trans (p1,p2)->
-	let (s1,t1)=type_proof axioms p1 
-	and (t2,s2)=type_proof axioms p2 in
-	  if t1=t2 then (s1,s2) else anomaly "invalid cc transitivity"
-    | Congr (p1,p2)->
-	let (i1,j1)=type_proof axioms p1
-	and (i2,j2)=type_proof axioms p2 in
-	  Appli (i1,i2),Appli (j1,j2)
-    | Inject (p,c,n,a)->
-	let (ti,tj)=type_proof axioms p in
-	  nth_arg ti (n-a),nth_arg tj (n-a)
 
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index abdd6fea..572b2c53 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -6,26 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccproof.mli 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: ccproof.mli 9856 2007-05-24 14:05:40Z corbinea $ *)
 
 open Ccalgo
 open Names
 open Term
 
-type proof =
+type rule=
     Ax of constr
   | SymAx of constr
   | Refl of term
-  | Trans of proof * proof
-  | Congr of proof * proof
-  | Inject of proof * constructor * int * int
+  | Trans of proof*proof
+  | Congr of proof*proof
+  | Inject of proof*constructor*int*int 
+and proof = 
+    private {p_lhs:term;p_rhs:term;p_rule:rule}
 
 val build_proof : 
   forest -> 
   [ `Discr of int * pa_constructor * int * pa_constructor
   | `Prove of int * int ] -> proof
 
-val type_proof :
-  (constr, (term * term)) Hashtbl.t -> proof -> term * term
 
 
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index ea8aceeb..86251254 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: cctac.ml 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
 
 (* This file is the interface between the c-c algorithm and Coq *)
 
@@ -37,6 +37,12 @@ let _f_equal = constant ["Init";"Logic"] "f_equal"
 
 let _eq_rect = constant ["Init";"Logic"] "eq_rect"
 
+let _refl_equal = constant ["Init";"Logic"] "refl_equal"
+
+let _sym_eq = constant ["Init";"Logic"] "sym_eq"
+
+let _trans_eq = constant ["Init";"Logic"] "trans_eq"
+
 let _eq = constant ["Init";"Logic"] "eq"
 
 let _False = constant ["Init";"Logic"] "False"
@@ -210,54 +216,73 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   
 (* generate an adhoc tactic following the proof tree  *)
 
-let rec proof_tac axioms=function
-    Ax c -> exact_check c
-  | SymAx c -> tclTHEN symmetry (exact_check c)
-  | Refl t -> reflexivity
-  | Trans (p1,p2)->let t=(constr_of_term (snd (type_proof axioms p1))) in
-      (tclTHENS (transitivity t) 
-	 [(proof_tac axioms p1);(proof_tac axioms p2)])
-  | Congr (p1,p2)->
-      fun gls->
-	let (f1,f2)=(type_proof axioms p1) 
-	and (x1,x2)=(type_proof axioms p2) in
-        let tf1=constr_of_term f1 and tx1=constr_of_term x1 
-	and tf2=constr_of_term f2 and tx2=constr_of_term x2 in
-	let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1
-	and typfx=pf_type_of gls (mkApp(tf1,[|tx1|])) in
-	let id=pf_get_new_id (id_of_string "f") gls in
-	let appx1=mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
-	let lemma1=
-	  mkApp(Lazy.force _f_equal,[|typf;typfx;appx1;tf1;tf2|])
-	and lemma2=
-	  mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2|]) in
-	  (tclTHENS (transitivity (mkApp(tf2,[|tx1|])))
-	     [tclTHEN (apply lemma1) (proof_tac axioms p1);
-  	      tclFIRST
-		[tclTHEN (apply lemma2) (proof_tac axioms p2);
-		 reflexivity;
-		 fun gls ->
-		   errorlabstrm  "Congruence" 
-		   (Pp.str 
-		      "I don't know how to handle dependent equality")]]
-	     gls)
-  | Inject (prf,cstr,nargs,argind)  as gprf->
-      (fun gls ->
-	 let ti,tj=type_proof axioms prf in
-	 let ai,aj=type_proof axioms gprf in
-	 let cti=constr_of_term ti in
-	 let ctj=constr_of_term tj in
-	 let cai=constr_of_term ai in
-	 let intype=pf_type_of gls cti in
-	 let outtype=pf_type_of gls cai in
+let _M =mkMeta
+
+let rec proof_tac p gls =
+  match p.p_rule with
+      Ax c -> exact_check c gls
+    | SymAx c -> 
+	let l=constr_of_term p.p_lhs and 
+	    r=constr_of_term p.p_rhs in
+        let typ = pf_type_of gls l in 	  
+	  exact_check
+	    (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
+    | Refl t ->
+	let lr = constr_of_term t in
+	let typ = pf_type_of gls lr in 
+	exact_check
+	   (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
+    | Trans (p1,p2)->
+	let t1 = constr_of_term p1.p_lhs and
+	    t2 = constr_of_term p1.p_rhs and
+	    t3 = constr_of_term p2.p_rhs in
+	let typ = pf_type_of gls t2 in 
+	let prf = 
+	  mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
+	  tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
+    | Congr (p1,p2)->
+	let tf1=constr_of_term p1.p_lhs 
+	and tx1=constr_of_term p2.p_lhs 
+	and tf2=constr_of_term p1.p_rhs 
+	and tx2=constr_of_term p2.p_rhs in
+	let typf = pf_type_of gls tf1 in
+	let typx = pf_type_of gls tx1 in
+	let typfx = prod_applist typf [tx1] in
+	let id = pf_get_new_id (id_of_string "f") gls in
+	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
+	let lemma1 =
+	  mkApp(Lazy.force _f_equal,
+		[|typf;typfx;appx1;tf1;tf2;_M 1|]) in
+	let lemma2=
+	  mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
+	let prf = 
+	  mkApp(Lazy.force _trans_eq,
+		[|typfx;
+		  mkApp(tf1,[|tx1|]);
+		  mkApp(tf2,[|tx1|]);
+		  mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in
+	  tclTHENS (refine prf)
+	    [tclTHEN (refine lemma1) (proof_tac p1);
+  	     tclFIRST
+	       [tclTHEN (refine lemma2) (proof_tac p2);
+		reflexivity;
+		fun gls ->
+		  errorlabstrm  "Congruence" 
+		    (Pp.str 
+		       "I don't know how to handle dependent equality")]] gls
+  | Inject (prf,cstr,nargs,argind) ->
+	 let ti=constr_of_term prf.p_lhs in
+	 let tj=constr_of_term prf.p_rhs in
+	 let default=constr_of_term p.p_lhs in
+	 let intype=pf_type_of gls ti in
+	 let outtype=pf_type_of gls default in
 	 let special=mkRel (1+nargs-argind) in
-	 let default=constr_of_term ai in
 	 let proj=build_projection intype outtype cstr special default gls in
 	 let injt=
-	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;cti;ctj|]) in 
-	   tclTHEN (apply injt) (proof_tac axioms prf) gls)
+	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in 
+	   tclTHEN (refine injt) (proof_tac prf) gls
 
-let refute_tac axioms c t1 t2 p gls =      
+let refute_tac c t1 t2 p gls =      
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let intype=pf_type_of gls tt1 in
   let neweq=
@@ -266,9 +291,9 @@ let refute_tac axioms c t1 t2 p gls =
   let hid=pf_get_new_id (id_of_string "Heq") gls in
   let false_t=mkApp (c,[|mkVar hid|]) in
     tclTHENS (true_cut (Name hid) neweq)
-      [proof_tac axioms p; simplest_elim false_t] gls
+      [proof_tac p; simplest_elim false_t] gls
 
-let convert_to_goal_tac axioms c t1 t2 p gls =
+let convert_to_goal_tac c t1 t2 p gls =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let sort=pf_type_of gls tt2 in
   let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in 
@@ -278,20 +303,19 @@ let convert_to_goal_tac axioms c t1 t2 p gls =
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
     tclTHENS (true_cut (Name e) neweq) 
-      [proof_tac axioms p;exact_check endt] gls
+      [proof_tac p;exact_check endt] gls
 
-let convert_to_hyp_tac axioms c1 t1 c2 t2 p gls =
+let convert_to_hyp_tac c1 t1 c2 t2 p gls =
   let tt2=constr_of_term t2 in
   let h=pf_get_new_id (id_of_string "H") gls in
   let false_t=mkApp (c2,[|mkVar h|]) in
     tclTHENS (true_cut (Name h) tt2)
-      [convert_to_goal_tac axioms c1 t1 t2 p;
+      [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t] gls
   
-let discriminate_tac axioms cstr p gls =
-  let t1,t2=type_proof axioms p in 
-  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype=pf_type_of gls tt1 in
+let discriminate_tac cstr p gls =
+  let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
+  let intype=pf_type_of gls t1 in
   let concl=pf_concl gls in
   let outsort=mkType (new_univ ()) in
   let xid=pf_get_new_id (id_of_string "X") gls in
@@ -303,12 +327,12 @@ let discriminate_tac axioms cstr p gls =
   let hid=pf_get_new_id (id_of_string "Heq") gls in     
   let proj=build_projection intype outtype cstr trivial concl gls in
   let injt=mkApp (Lazy.force _f_equal,
-		  [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in   
+		  [|intype;outtype;proj;t1;t2;mkVar hid|]) in   
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|outtype;trivial;pred;identity;concl;injt|]) in
-  let neweq=mkApp(Lazy.force _eq,[|intype;tt1;tt2|]) in
+  let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
     tclTHENS (true_cut (Name hid) neweq) 
-      [proof_tac axioms p;exact_check endt] gls
+      [proof_tac p;exact_check endt] gls
       
 (* wrap everything *)
 	
@@ -333,12 +357,12 @@ let cc_tactic depth additionnal_terms gls=
 	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
 	  match reason with
 	      Discrimination (i,ipac,j,jpac) ->
-		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in	  
+		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
 		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
-		  discriminate_tac (axioms uf) cstr p gls
+		  discriminate_tac cstr p gls
 	    | Incomplete ->
 		let metacnt = ref 0 in
-		let newmeta _ = incr metacnt; mkMeta !metacnt in
+		let newmeta _ = incr metacnt; _M !metacnt in
 		let terms_to_complete = 
 		  List.map 
 		    (build_term_to_complete uf newmeta) 
@@ -363,14 +387,13 @@ let cc_tactic depth additionnal_terms gls=
 	    | Contradiction dis ->
 		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
 		let ta=term uf dis.lhs and tb=term uf dis.rhs in
-		let axioms = axioms uf in 
 		  match dis.rule with
-		      Goal -> proof_tac axioms p gls
-		    | Hyp id -> refute_tac axioms id ta tb p gls
+		      Goal -> proof_tac p gls
+		    | Hyp id -> refute_tac id ta tb p gls
 		    | HeqG id -> 
-			convert_to_goal_tac axioms id ta tb p gls
+			convert_to_goal_tac id ta tb p gls
 		    | HeqnH (ida,idb) -> 
-			convert_to_hyp_tac axioms ida ta idb tb p gls
+			convert_to_hyp_tac ida ta idb tb p gls
 		    
 
 let cc_fail gls =
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index ff4f7499..dec7273b 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -621,33 +621,39 @@ let build_proof
     fun g -> 
       
 (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
-	match kind_of_term dyn_infos.info with 
-	  | Case(_,_,t,_) -> 
-	      let g_nb_prod = nb_prod (pf_concl g) in
-	      let type_of_term = pf_type_of g t in
-	      let term_eq =
-		make_refl_eq type_of_term t
+	match kind_of_term dyn_infos.info with 	  | Case(ci,ct,t,cb) -> 
+	      let do_finalize_t dyn_info' = 
+		fun g ->
+		  let t = dyn_info'.info in 
+		  let dyn_infos = {dyn_info' with info = 
+		      mkCase(ci,ct,t,cb)} in
+		  let g_nb_prod = nb_prod (pf_concl g) in
+		  let type_of_term = pf_type_of g t in
+		  let term_eq =
+		    make_refl_eq type_of_term t
+		  in
+		  tclTHENSEQ
+		    [
+		      h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+		      thin dyn_infos.rec_hyps;
+		      pattern_option [[-1],t] None;
+		      h_simplest_case t;
+		      (fun g' -> 
+			 let g'_nb_prod = nb_prod (pf_concl g') in 
+			 let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
+			 		     observe_tac "treat_new_case"
+			 (treat_new_case  
+			    ptes_infos
+			    nb_instanciate_partial 
+			    (build_proof do_finalize) 
+			    t 
+			    dyn_infos)
+			   g'
+		      )
+			
+		    ] g
 	      in
-	      tclTHENSEQ
-		[
-		  h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
-		  thin dyn_infos.rec_hyps;
-		  pattern_option [[-1],t] None;
-		  h_simplest_case t;
-		  (fun g' -> 
-		     let g'_nb_prod = nb_prod (pf_concl g') in 
-		     let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
-		     observe_tac "treat_new_case" 
-		       (treat_new_case  
-		       ptes_infos
-		       nb_instanciate_partial 
-		       (build_proof do_finalize) 
-		       t 
-		       dyn_infos)
-		       g'
-		  )
-		  
-		] g
+	      build_proof do_finalize_t {dyn_infos with info = t} g
 	  | Lambda(n,t,b) ->
 	      begin
 		match kind_of_term( pf_concl g) with
@@ -1474,7 +1480,7 @@ let prove_principle_for_gen
  	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
       );
       observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids)));
-      observe_tac "h_fix" (h_fix (Some fix_id) (npost_rec_arg + 1)); 
+      observe_tac "h_fix" (h_fix (Some fix_id) (List.length args_ids + 1)); 
       h_intros (List.rev (acc_rec_arg_id::args_ids));
       Equality.rewriteLR (mkConst eq_ref);
       observe_tac "finish" (fun gl' -> 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 6e2af224..82bee01f 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -209,7 +209,7 @@ let rec is_rec names =
   let rec lookup names = function 
     | RVar(_,id) -> check_id id names
     | RRef _ | REvar _ | RPatVar _ | RSort _ |  RHole _ | RDynamic _ -> false
-    | RCast(_,b,_,_) -> lookup names b
+    | RCast(_,b,_) -> lookup names b
     | RRec _ -> error "RRec not handled"
     | RIf(_,b,_,lhs,rhs) -> 
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
@@ -270,7 +270,30 @@ let derive_inversion fix_names =
 	   if do_observe () then Cerrors.explain_exn e else mt ())
   with _ -> ()
 
-let generate_principle 
+let warning_error names e = 
+  match e with 
+    | Building_graph e -> 
+	Pp.msg_warning 
+	  (str "Cannot define graph(s) for " ++ 
+	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	     if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+    | Defining_principle e -> 
+	Pp.msg_warning
+	  (str "Cannot define principle(s) for "++ 
+	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	     if do_observe () then Cerrors.explain_exn e else mt ())
+    | _ -> anomaly ""
+
+let error_error names e = 
+  match e with 
+    | Building_graph e -> 
+	errorlabstrm ""  
+	  (str "Cannot define graph(s) for " ++ 
+	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	     if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+    | _ -> anomaly ""
+
+let generate_principle  on_error
     is_general do_built fix_rec_l recdefs  interactive_proof 
     (continue_proof : int -> Names.constant array -> Term.constr array -> int -> 
       Tacmach.tactic) : unit =
@@ -324,18 +347,7 @@ let generate_principle
 	()
       end
   with e -> 
-    match e with 
-      | Building_graph e -> 
-	    Pp.msg_warning 
-	    (str "Cannot define graph(s) for " ++ 
-	       h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	       if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
-      | Defining_principle e -> 
-	    Pp.msg_warning
-	    (str "Cannot define principle(s) for "++ 
-	       h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	       if do_observe () then Cerrors.explain_exn e else mt ())
-      | _ -> anomaly ""
+    on_error names e 
 
 let register_struct is_rec fixpoint_exprl = 
   match fixpoint_exprl with 
@@ -459,13 +471,14 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
     using_lemmas args ret_type body
 	  
 
-let do_generate_principle register_built interactive_proof fixpoint_exprl  = 
+let do_generate_principle on_error register_built interactive_proof fixpoint_exprl  = 
   let recdefs,rec_impls = build_newrecursive fixpoint_exprl in 
   let _is_struct = 
     match fixpoint_exprl with 
       | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
+	      on_error
 	      true
 	      register_built
 	      fixpoint_exprl 
@@ -478,6 +491,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
       | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
+	      on_error
 	      true
 	      register_built
 	      fixpoint_exprl 
@@ -530,6 +544,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	  let is_rec = List.exists (is_rec fix_names) recdefs in
 	  if register_built then register_struct is_rec old_fixpoint_exprl;
 	  generate_principle
+	    on_error
 	    false
 	    register_built
 	    fixpoint_exprl
@@ -596,8 +611,10 @@ let rec add_args id new_args b =
   | CPatVar _ -> b
   | CEvar _ -> b
   | CSort _ -> b
-  | CCast(loc,b1,ck,b2)  -> 
-      CCast(loc,add_args id new_args b1,ck,add_args id new_args b2)
+  | CCast(loc,b1,CastConv(ck,b2))  -> 
+      CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
+  | CCast(loc,b1,CastCoerce) ->
+      CCast(loc,add_args id new_args b1,CastCoerce)
   | CNotation _ -> anomaly "add_args : CNotation"
   | CPrim _ -> b
   | CDelimiters _ -> anomaly "add_args : CDelimiters"
@@ -732,7 +749,7 @@ let make_graph (f_ref:global_reference) =
 		let id = id_of_label (con_label c) in 
 		[(id,None,nal_tas,t,b)]
 	in
-	do_generate_principle false false expr_list;
+	do_generate_principle error_error false false expr_list;
 	(* We register the infos *)
 	let mp,dp,_ = repr_con c in 
 	List.iter 
@@ -742,6 +759,6 @@ let make_graph (f_ref:global_reference) =
 
 (* let make_graph _ = assert false	 *)
 	  
-let do_generate_principle = do_generate_principle true 
+let do_generate_principle = do_generate_principle warning_error true 
 
 
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 26a1066c..9cee9edc 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -203,7 +203,10 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 	match fas with 
 	  | (_,fun_name,_)::_ -> 
 	      begin
-		make_graph (Nametab.global fun_name);
+		begin
+		    make_graph (Nametab.global fun_name)
+		end
+		;
 		try Functional_principles_types.build_scheme fas
 		with Functional_principles_types.No_graph_found -> 
 		  Util.error ("Cannot generate induction principle(s)")
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 04110ea9..9ec02d4c 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -478,7 +478,72 @@ let generalize_depedent_of x hyp g =
 
 
 
-
+    (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis 
+       (unfolding, substituting, destructing cases \ldots)
+    *)
+let  rec intros_with_rewrite g = 
+  observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
+and intros_with_rewrite_aux : tactic = 
+  fun g -> 
+    let eq_ind = Coqlib.build_coq_eq () in 
+    match kind_of_term (pf_concl g) with 
+	  | Prod(_,t,t') -> 
+	      begin 
+		match kind_of_term t with 
+		  | App(eq,args) when (eq_constr eq eq_ind) -> 
+		      if isVar args.(1)
+		      then 			
+			let id = pf_get_new_id (id_of_string "y") g  in 
+			tclTHENSEQ [ h_intro id;
+				     generalize_depedent_of (destVar args.(1)) id; 
+				     tclTRY (Equality.rewriteLR (mkVar id));
+				     intros_with_rewrite
+				   ] 
+			  g
+		      else
+			begin 
+			  let id = pf_get_new_id (id_of_string "y") g  in 
+			  tclTHENSEQ[
+			    h_intro id;
+			    tclTRY (Equality.rewriteLR (mkVar id));
+			    intros_with_rewrite
+			  ] g
+			end
+		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> 
+		      Tauto.tauto g
+		  | Case(_,_,v,_) -> 
+		      tclTHENSEQ[
+			h_case (v,Rawterm.NoBindings);
+			intros_with_rewrite
+		      ] g
+		  | LetIn _ -> 
+		      tclTHENSEQ[
+			h_reduce 
+			  (Rawterm.Cbv
+			     {Rawterm.all_flags 
+			      with Rawterm.rDelta = false; 		 
+			     }) 
+			  onConcl
+			;
+			intros_with_rewrite
+		      ] g
+		  | _ -> 			
+		      let id = pf_get_new_id (id_of_string "y") g  in 
+		      tclTHENSEQ [ h_intro id;intros_with_rewrite] g
+	      end
+	  | LetIn _ -> 
+	      tclTHENSEQ[
+		h_reduce 
+		  (Rawterm.Cbv
+		     {Rawterm.all_flags 
+		      with Rawterm.rDelta = false; 		 
+		     }) 
+		  onConcl
+		;
+		intros_with_rewrite
+	      ] g
+	  | _ -> tclIDTAC g 
+  
 let rec reflexivity_with_destruct_cases g = 
   let destruct_case () = 
     try 
@@ -492,10 +557,34 @@ let rec reflexivity_with_destruct_cases g =
 	| _ -> reflexivity
     with _ -> reflexivity
   in
-  tclFIRST
+  let eq_ind =     Coqlib.build_coq_eq () in
+  let discr_inject =
+    Tacticals.onAllClauses (
+       fun sc g -> 
+	 match sc with 
+	     None -> tclIDTAC g
+	   | Some ((_,id),_) -> 
+	       match kind_of_term  (pf_type_of g (mkVar id)) with 
+		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> 
+		     if Equality.discriminable (pf_env g) (project g) t1 t2 
+		     then Equality.discr id g
+		     else if Equality.injectable (pf_env g) (project g) t1 t2
+		     then tclTHEN (Equality.inj [] id) intros_with_rewrite  g
+		     else tclIDTAC g
+		 | _ -> tclIDTAC g
+    )
+  in
+  (tclFIRST
     [ reflexivity;
-      destruct_case ()
-    ]
+      destruct_case ();
+      (*  We reach this point ONLY if 
+	  the same value is matched (at least) two times 
+	  along binding path.
+	  In this case, either we have a discriminable hypothesis and we are done, 
+	  either at least an injectable one and we do the injection before continuing
+      *)
+      tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases
+    ])
     g
 
 
@@ -566,7 +655,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	)
 	branches
     in
-    let eq_ind = Coqlib.build_coq_eq () in 
     (* We will need to change the function by its body 
        using [f_equation] if it is recursive (that is the graph is infinite 
        or unfold if the graph is finite 
@@ -596,71 +684,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	]
       else unfold_in_concl [([],Names.EvalConstRef (destConst f))]
     in
-    (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis 
-       (unfolding, substituting, destructing cases \ldots)
-    *)
-    let rec intros_with_rewrite_aux : tactic = 
-      fun g -> 
-	match kind_of_term (pf_concl g) with 
-	  | Prod(_,t,t') -> 
-	      begin 
-		match kind_of_term t with 
-		  | App(eq,args) when (eq_constr eq eq_ind) -> 
-		      if isVar args.(1)
-		      then 			
-			let id = pf_get_new_id (id_of_string "y") g  in 
-			tclTHENSEQ [ h_intro id;
-				     generalize_depedent_of (destVar args.(1)) id; 
-				     tclTRY (Equality.rewriteLR (mkVar id));
-				     intros_with_rewrite
-				   ] 
-			  g
-		      else
-			begin 
-			  let id = pf_get_new_id (id_of_string "y") g  in 
-			  tclTHENSEQ[
-			    h_intro id;
-			    tclTRY (Equality.rewriteLR (mkVar id));
-			    intros_with_rewrite
-			  ] g
-			end
-		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> 
-		      Tauto.tauto g
-		  | Case(_,_,v,_) -> 
-		      tclTHENSEQ[
-			h_case (v,Rawterm.NoBindings);
-			intros_with_rewrite
-		      ] g
-		  | LetIn _ -> 
-		      tclTHENSEQ[
-			h_reduce 
-			  (Rawterm.Cbv
-			     {Rawterm.all_flags 
-			      with Rawterm.rDelta = false; 		 
-			     }) 
-			  onConcl
-			;
-			intros_with_rewrite
-		      ] g
-		  | _ -> 			
-		      let id = pf_get_new_id (id_of_string "y") g  in 
-		      tclTHENSEQ [ h_intro id;intros_with_rewrite] g
-	      end
-	  | LetIn _ -> 
-	      tclTHENSEQ[
-		h_reduce 
-		  (Rawterm.Cbv
-		     {Rawterm.all_flags 
-		      with Rawterm.rDelta = false; 		 
-		     }) 
-		  onConcl
-		;
-		intros_with_rewrite
-	      ] g
-	  | _ -> tclIDTAC g 
-    and intros_with_rewrite g = 
-      observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
-    in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in 
     let min_constr_number = ref 0 in
@@ -698,7 +721,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	h_intro graph_principle_id;
 	observe_tac "" (tclTHEN_i 
 	  (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
-	  (fun i g -> prove_branche i g ))
+	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
 
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index aca84f06..b34a1097 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -351,7 +351,7 @@ let rec find_type_of nb b =
 	  then raise (Invalid_argument "find_type_of : not a valid inductive");
 	  ind_type	   
 	end
-    | RCast(_,b,_,_) -> find_type_of nb b 
+    | RCast(_,b,_) -> find_type_of nb b 
     | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *)
     | _ -> raise (Invalid_argument "not a ref")
     
@@ -575,7 +575,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		let f_res = build_entry_lc env funnames args_res.to_avoid f in
 		combine_results combine_app f_res  args_res
 	    | RDynamic _ ->error "Not handled RDynamic" 
-	    | RCast(_,b,_,_) -> 
+	    | RCast(_,b,_) -> 
 		(* for an applied cast we just trash the cast part 
 		   and restart the work. 
 
@@ -685,7 +685,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 
 	end
     | RRec _ -> error "Not handled RRec"
-    | RCast(_,b,_,_) -> 
+    | RCast(_,b,_) -> 
 	build_entry_lc env funnames  avoid b
     | RDynamic _ -> error "Not handled RDynamic"
 and build_entry_lc_from_case env funname make_discr
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index ba5c2bbd..113ddd8b 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
 let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
 let mkRSort s = RSort(dummy_loc,s)
 let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
-let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t)
+let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
 
 (*
   Some basic functions to decompose rawconstrs
@@ -145,8 +145,10 @@ let change_vars =
       | RRec _ -> error "Local (co)fixes are not supported"
       | RSort _ -> rt 
       | RHole _ -> rt 
-      | RCast(loc,b,k,t) -> 
-	  RCast(loc,change_vars mapping b,k,change_vars mapping t)
+      | RCast(loc,b,CastConv (k,t)) -> 
+	  RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
+      | RCast(loc,b,CastCoerce) -> 
+	  RCast(loc,change_vars mapping b,CastCoerce)
       | RDynamic _ -> error "Not handled RDynamic"
   and change_vars_br mapping ((loc,idl,patl,res) as br) = 
     let new_mapping = List.fold_right Idmap.remove idl mapping in 
@@ -324,8 +326,10 @@ let rec alpha_rt excluded rt =
     | RRec _ -> error "Not handled RRec"
     | RSort _ -> rt 
     | RHole _ -> rt 
-    | RCast (loc,b,k,t) -> 
-	RCast(loc,alpha_rt excluded b,k,alpha_rt excluded t)
+    | RCast (loc,b,CastConv (k,t)) -> 
+	RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
+    | RCast (loc,b,CastCoerce) -> 
+	RCast(loc,alpha_rt excluded b,CastCoerce)
     | RDynamic _ -> error "Not handled RDynamic"
     | RApp(loc,f,args) -> 
 	RApp(loc,
@@ -375,7 +379,8 @@ let is_free_in id =
     | RRec _ -> raise (UserError("",str "Not handled RRec"))
     | RSort _ -> false
     | RHole _ -> false
-    | RCast (_,b,_,t) -> is_free_in b || is_free_in t
+    | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
+    | RCast (_,b,CastCoerce) -> is_free_in b
     | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
   and is_free_in_br (_,ids,_,rt) =
     (not (List.mem id ids)) && is_free_in rt
@@ -469,8 +474,10 @@ let replace_var_by_term x_id term =
       | RRec _ -> raise (UserError("",str "Not handled RRec"))
       | RSort _ -> rt 
       | RHole _ -> rt 
-      | RCast(loc,b,k,t) -> 
-	  RCast(loc,replace_var_by_pattern b,k,replace_var_by_pattern t)
+      | RCast(loc,b,CastConv(k,t)) -> 
+	  RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
+      | RCast(loc,b,CastCoerce) -> 
+	  RCast(loc,replace_var_by_pattern b,CastCoerce)
       | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
   and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = 
     if List.exists (fun id -> id_ord id x_id == 0) idl 
@@ -554,7 +561,8 @@ let ids_of_rawterm c =
       | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
       | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
       | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
-      | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+      | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+      | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
       | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
       | RLetTuple (_,nal,(na,po),b,c) -> 
           List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
@@ -619,8 +627,10 @@ let zeta_normalize =
       | RRec _ -> raise (UserError("",str "Not handled RRec"))
       | RSort _ -> rt 
       | RHole _ -> rt 
-      | RCast(loc,b,k,t) -> 
-	  RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t)
+      | RCast(loc,b,CastConv(k,t)) -> 
+	  RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
+      | RCast(loc,b,CastCoerce) -> 
+	  RCast(loc,zeta_normalize_term b,CastCoerce)
       | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
   and zeta_normalize_br (loc,idl,patl,res) = 
     (loc,idl,patl,zeta_normalize_term res)
@@ -660,7 +670,8 @@ let expand_as =
 	      expand_as map br1, expand_as map br2)
       | RRec _ ->  error "Not handled RRec"
       | RDynamic _ -> error "Not handled RDynamic"
-      | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t)
+      | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
+      | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
       | RCases(loc,po,el,brl) ->
 	  RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 60195229..df03a579 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -408,9 +408,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CDynamic (_, _) -> assert false
    | CDelimiters (_, key, num) -> 
 	 CT_num_encapsulator(CT_num_type key , xlate_formula  num)
-   | CCast (_, e,_, t) -> 
+   | CCast (_, e, CastConv (_, t)) -> 
        CT_coerce_TYPED_FORMULA_to_FORMULA
 	 (CT_typed_formula(xlate_formula e, xlate_formula t))
+   | CCast (_, e, CastCoerce) -> assert false
    | CPatVar (_, (_,i)) when is_int_meta i ->
        CT_coerce_ID_to_FORMULA(CT_metac (CT_int (int_of_meta i)))
    | CPatVar (_, (false, s)) ->
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index da0817d1..be9ea5ae 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -13,7 +13,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* $Id: coq_omega.ml 8934 2006-06-09 14:30:12Z herbelin $ *)
+(* $Id: coq_omega.ml 9963 2007-07-09 14:02:20Z letouzey $ *)
 
 open Util
 open Pp
@@ -302,6 +302,7 @@ let coq_eq_ind_r = lazy (constant "eq_ind_r")
 let coq_dec_or = lazy (constant "dec_or")
 let coq_dec_and = lazy (constant "dec_and")
 let coq_dec_imp = lazy (constant "dec_imp")
+let coq_dec_iff = lazy (constant "dec_iff")
 let coq_dec_not = lazy (constant "dec_not")
 let coq_dec_False = lazy (constant "dec_False")
 let coq_dec_not_not = lazy (constant "dec_not_not")
@@ -312,6 +313,7 @@ let coq_not_and = lazy (constant "not_and")
 let coq_not_imp = lazy (constant "not_imp")
 let coq_not_not = lazy (constant "not_not")
 let coq_imp_simp = lazy (constant "imp_simp")
+let coq_iff = lazy (constant "iff")
 
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
 
@@ -388,6 +390,8 @@ let destructurate_prop t =
     | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args)
     | _, [_;_] when c = build_coq_and () -> Kapp (And,args)
     | _, [_;_] when c = build_coq_or () -> Kapp (Or,args)
+    | _, [t1;t2] when c = Lazy.force coq_iff -> 
+	Kapp (And,[mkArrow t1 t2;mkArrow t2 t1])
     | _, [_] when c = build_coq_not () -> Kapp (Not,args)
     | _, [] when c = build_coq_False () -> Kapp (False,args)
     | _, [] when c = build_coq_True () -> Kapp (True,args)
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 353fcdb3..a4acd9a9 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -46,6 +46,9 @@ open Eauto
 open Genarg
 
 
+let compute_renamed_type gls c = 
+  rename_bound_var (pf_env gls) [] (pf_type_of gls c)
+
 let qed () = Command.save_named true 
 let defined () = Command.save_named false
 
@@ -388,32 +391,57 @@ let rec compute_le_proofs = function
   | a::tl ->
       tclORELSE assumption 
 	(tclTHENS
-	   (apply_with_bindings
-	      (delayed_force le_trans,
-	       ExplicitBindings[dummy_loc,NamedHyp(id_of_string "m"),a]))
+	   (fun g -> 
+	      let le_trans = delayed_force le_trans in 
+	      let t_le_trans = compute_renamed_type g le_trans in 
+	      let m_id = 
+		let _,_,t = destProd t_le_trans in 
+		let na,_,_ = destProd t in 
+		Nameops.out_name na
+	      in
+	      apply_with_bindings
+		(le_trans,
+		 ExplicitBindings[dummy_loc,NamedHyp m_id,a])
+		g
+	   )
 	   [compute_le_proofs tl; 
             tclORELSE (apply (delayed_force le_n)) assumption])
 
 let make_lt_proof pmax le_proof =
   tclTHENS
-    (apply_with_bindings
-       (delayed_force le_lt_trans,
-	ExplicitBindings[dummy_loc,NamedHyp(id_of_string "m"), pmax]))
-    [compute_le_proofs le_proof; 
-     tclTHENLIST[apply (delayed_force lt_S_n); default_full_auto]];;
+    (fun g -> 
+       let le_lt_trans = delayed_force le_lt_trans in 
+       let t_le_lt_trans = compute_renamed_type g le_lt_trans in 
+       let m_id = 
+	 let _,_,t = destProd t_le_lt_trans in 
+	 let na,_,_ = destProd t in 
+	 Nameops.out_name na
+       in
+       apply_with_bindings
+	 (le_lt_trans,
+	  ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g)
+    [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); 
+     tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];;
 
 let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
   match cond_eqs with
     [] -> tclIDTAC
   | eq::eqs ->
       (fun g -> 
+	 let t_eq = compute_renamed_type g (mkVar eq) in 
+	 let k_id,def_id = 
+	   let k_na,_,t = destProd t_eq in 
+	   let _,_,t  = destProd t in 
+	   let def_na,_,_ = destProd t in 
+	   Nameops.out_name k_na,Nameops.out_name def_na
+	 in
 	 tclTHENS
 	   (general_rewrite_bindings false
 	      (mkVar eq,
 	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
 				dummy_loc, NamedHyp def_id, mkVar def]))
 	   [list_cond_rewrite k def pmax eqs le_proofs;
-            make_lt_proof pmax le_proofs] g
+            observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g
       ) 
 
 let rec introduce_all_equalities func eqs values specs bound le_proofs 
@@ -1023,12 +1051,20 @@ let rec introduce_all_values_eq  cont_tac functional termine
       [] ->
 	tclTHENLIST
 	  [tclTHENS
-	     (general_rewrite_bindings false
+	     (fun gls -> 
+		let t_eq = compute_renamed_type gls (mkVar heq1) in 
+		let k_id,def_id = 
+		  let k_na,_,t = destProd t_eq in 
+		  let _,_,t  = destProd t in 
+		  let def_na,_,_ = destProd t in 
+		  Nameops.out_name k_na,Nameops.out_name def_na
+		in
+		general_rewrite_bindings false
 		(mkVar heq1,
 		 ExplicitBindings[dummy_loc,NamedHyp k_id,
 				  f_S(f_S(mkVar pmax));
 				  dummy_loc,NamedHyp def_id,
-				  f]))
+				  f]) gls )
 	     [tclTHENLIST
 		[simpl_iter();
 		 unfold_constr (reference_of_constr functional);
@@ -1067,12 +1103,22 @@ let rec introduce_all_values_eq  cont_tac functional termine
 		   h_intros [heq;heq2];
 		   rewriteLR (mkVar heq2);
 		   tclTHENS
-		     (general_rewrite_bindings false
-			(mkVar heq,
-			 ExplicitBindings
-			   [dummy_loc, NamedHyp k_id,
-			    f_S(mkVar pmax');
-			    dummy_loc, NamedHyp def_id, f]))
+		     ( fun g -> 
+			 let t_eq = compute_renamed_type g (mkVar heq) in 
+			 let k_id,def_id = 
+			   let k_na,_,t = destProd t_eq in 
+			   let _,_,t  = destProd t in 
+			   let def_na,_,_ = destProd t in 
+			   Nameops.out_name k_na,Nameops.out_name def_na
+			 in
+			 general_rewrite_bindings false
+			   (mkVar heq,
+			    ExplicitBindings
+			      [dummy_loc, NamedHyp k_id,
+			       f_S(mkVar pmax');
+			       dummy_loc, NamedHyp def_id, f]) 
+			   g
+		     )
 		     [tclIDTAC;
 		      tclTHENLIST
 			[apply (delayed_force le_lt_n_Sm);
@@ -1132,9 +1178,9 @@ let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
 	      | fn,args ->
 		  fun g ->
 		    let ids = ids_of_named_context (pf_hyps g) in
-		    rec_leaf_eq  
+		    observe_tac "rec_leaf_eq" (rec_leaf_eq  
 		      termine f ids (constr_of_reference functional)
-		      eqs expr fn args g));;
+		      eqs expr fn args) g));;
 
 let (com_eqn : identifier ->
        global_reference -> global_reference -> global_reference
@@ -1159,10 +1205,19 @@ let (com_eqn : identifier ->
 	       )
 	  )
        );
+(*      (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); 
+     Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript);
+*)
      Options.silently defined (); 
     );;
 
 
+let nf_zeta env =       
+  Reductionops.clos_norm_flags  (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+    env
+    Evd.empty
+
+
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq 
     generate_induction_principle using_lemmas : unit =
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
@@ -1171,10 +1226,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in 
 (*   Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in 
+  let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
+  let eq' = nf_zeta env_eq' eq'  in 
   let res = 
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
 (*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
-(*     Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
+(*     Pp.msgnl (str "eq' := " ++ Printer.pr_lconstr_env env eq' ++ fnl () ++str (string_of_int rec_arg_num)); *)
     match kind_of_term eq' with 
       | App(e,[|_;_;eq_fix|]) -> 
 	  mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars  eq_fix))
@@ -1201,16 +1258,19 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     let term_ref = Nametab.locate (make_short_qualid term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
 (*     message "start second proof"; *)
+    let continue = ref true in 
     begin 
       try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type)
       with e -> 
 	begin 
 	  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
-	  then anomalylabstrm "" (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e);
-	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
-	  anomaly "Cannot create equation Lemma"
+	  then (Pp.msgnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e); continue := false)
+	  else (ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
+	  anomaly "Cannot create equation Lemma")
 	end
     end;
+    if !continue 
+    then
     let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
     let f_ref = destConst (constr_of_reference f_ref) 
     and functional_ref = destConst (constr_of_reference functional_ref) 
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 83ea5b63..d20cafc1 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -1848,6 +1848,15 @@ Definition exact_divide (k : Z) (body : term) (t : nat)
           end
       | false => TrueTerm
       end
+  | NeqTerm (Tint Z0) b =>
+      match eq_term (scalar_norm t (body * Tint k)%term) b with
+      | true =>
+          match eq_Z k 0 with
+          | true => FalseTerm
+          | false => NeqTerm (Tint 0) body
+          end
+      | false => TrueTerm
+      end
   | _ => TrueTerm
   end.
 
@@ -1858,18 +1867,24 @@ Theorem exact_divide_valid :
 unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; Simplify;
  simpl in |- *; auto; elim_eq_term (scalar_norm t (k2 * Tint k1)%term) t1;
  simpl in |- *; auto; elim_eq_Z k1 0; simpl in |- *; 
- auto; intros H1 H2; elim H2; elim scalar_norm_stable; 
- simpl in |- *; generalize H1; case (interp_term e k2); 
+ auto; intros H1 H2; elim H2; elim scalar_norm_stable;
+ simpl in |- *; 
+ [
+ generalize H1; case (interp_term e k2); 
  try trivial;
  (case k1; simpl in |- *;
    [ intros; absurd (0 = 0); assumption
    | intros p2 p3 H3 H4; discriminate H4
-   | intros p2 p3 H3 H4; discriminate H4 ]).
-
+   | intros p2 p3 H3 H4; discriminate H4 ])
+ |
+ subst k1; rewrite Zmult_comm; simpl in *; intros; absurd (0=0); trivial
+ |
+ generalize H1; case (interp_term e k2); 
+ try trivial; intros p2 p3 H3 H4; discriminate H4
+ ].
 Qed.
 
 
-
 (* \paragraph{[O_DIV_APPROX]}
   La preuve reprend le schéma de la précédente mais on
   est sur une opération de type valid1 et non sur une opération terminale. *)
@@ -1954,7 +1969,7 @@ Definition state (m : Z) (s : step) (prop1 prop2 : proposition) :=
   match prop1 with
   | EqTerm (Tint Z0) b1 =>
       match prop2 with
-      | EqTerm (Tint Z0) (b2 + - b3)%term =>
+      | EqTerm b2 b3 =>
           EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term)
       | _ => TrueTerm
       end
@@ -1965,10 +1980,8 @@ Theorem state_valid : forall (m : Z) (s : step), valid2 (state m s).
 
 unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify;
  simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *; 
- intros H1 H2; elim H1;
- rewrite (Zplus_comm (- interp_term e t5) (interp_term e t3)); 
- elim H2; simpl in |- *; reflexivity.
-
+ intros H1 H2; elim H1.
+ rewrite H2; rewrite Zplus_opp_l; simpl; reflexivity.
 Qed.
 
 (* \subsubsection{Tactiques générant plusieurs but}
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 285fc0ca..e7e7b3c5 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -6,6 +6,10 @@
 
  *************************************************************************)
 
+(* The addition on int, since it while be hidden soon by the one on BigInt *)
+
+let (+.) = (+)
+
 open Const_omega
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -792,6 +796,9 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
     | Kimp(t1,t2) ->
 	binprop env ctxt (not negated) (not negated) gl 
 	  (fun i x y -> Pimp(i,x,y)) t1 t2
+    | Kapp("iff",[t1;t2]) ->
+	binprop env ctxt negated negated gl 
+	  (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
     | _ -> Pprop c
   with e when Logic.catchable_exception e -> Pprop c
 
@@ -995,10 +1002,10 @@ let rec equas_of_solution_tree = function
       list_union (equas_of_solution_tree t1) (equas_of_solution_tree t2)
   | Leaf s -> s.s_equa_deps
 
-
-(* Because of really_useful_prop, decidable formulas such as Pfalse
-   and Ptrue are moved to Pprop, thus breaking the decidability check
-   in ReflOmegaCore.concl_to_hyp... *)
+(* [really_useful_prop] pushes useless props in a new Pprop variable *)
+(* Things get shorter, but may also get wrong, since a Prop is considered 
+   to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance 
+   Pfalse is decidable. So should not be used on conclusion (??) *)
 
 let really_useful_prop l_equa c =
   let rec real_of = function
@@ -1034,6 +1041,14 @@ let really_useful_prop l_equa c =
     None -> Pprop (real_of c)
   | Some t -> t
 
+let rec vars_of_prop = function 
+  | Pequa(_,e) -> vars_of_equations [e]
+  | Pnot p -> vars_of_prop p
+  | Por(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
+  | Pand(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
+  | Pimp(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
+  | _ -> []
+
 let rec display_solution_tree ch = function
     Leaf t -> 
       output_string ch 
@@ -1160,10 +1175,15 @@ let replay_history env env_hyp =
       |	CONSTANT_NUL e :: l ->
 	  mkApp (Lazy.force coq_s_constant_nul, 
 		 [|  mk_nat (get_hyp env_hyp e) |])
-      |	NEGATE_CONTRADICT(e1,e2,b) :: l ->
+      |	NEGATE_CONTRADICT(e1,e2,true) :: l ->
 	  mkApp (Lazy.force coq_s_negate_contradict, 
 		 [|  mk_nat (get_hyp env_hyp e1.id);
 		     mk_nat (get_hyp env_hyp e2.id) |])
+      |	NEGATE_CONTRADICT(e1,e2,false) :: l ->
+	  mkApp (Lazy.force coq_s_negate_contradict_inv, 
+		 [|  mk_nat (List.length e2.body); 
+		     mk_nat (get_hyp env_hyp e1.id);
+		     mk_nat (get_hyp env_hyp e2.id) |])
       | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
 	  let i =  get_hyp env_hyp e.id in
 	  let r1 = loop (CCEqua e1 :: env_hyp) l1 in
@@ -1254,14 +1274,18 @@ let resolution env full_reified_goal systems_list =
   let l_hyps = id_concl :: list_remove id_concl l_hyps' in
   let useful_hyps =
     List.map (fun id -> List.assoc id full_reified_goal) l_hyps in
-  let useful_vars = vars_of_equations equations in
+  let useful_vars = 
+    let really_useful_vars = vars_of_equations equations in
+    let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in     
+    list_uniq (List.sort compare (really_useful_vars @ concl_vars))
+  in 
   (* variables a introduire *)
   let to_introduce = add_stated_equations env solution_tree in
   let stated_vars =  List.map (fun (v,_,_,_) -> v) to_introduce in
   let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in
   let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in
   (* L'environnement de base se construit en deux morceaux :
-     - les variables des équations utiles
+     - les variables des équations utiles (et de la conclusion)
      - les nouvelles variables declarées durant les preuves *)
   let all_vars_env = useful_vars @ stated_vars in
   let basic_env =
@@ -1280,8 +1304,7 @@ let resolution env full_reified_goal systems_list =
               to_introduce in
   let reified_concl = 
     match useful_hyps with
-      (Pnot p) :: _ ->
-	reified_of_proposition env (really_useful_prop useful_equa_id p)
+      (Pnot p) :: _ -> reified_of_proposition env p
     | _ ->  reified_of_proposition env Pfalse in
   let l_reified_terms =
     (List.map
@@ -1301,9 +1324,13 @@ let resolution env full_reified_goal systems_list =
 	          [| e.e_trace |]
       |	((O_left | O_mono) :: l) -> app coq_p_left [| loop l |]
       |	(O_right :: l) -> app coq_p_right [| loop l |] in
-    app coq_pair_step 
-        [| mk_nat (list_index e.e_origin.o_hyp l_hyps) ;
-	   loop e.e_origin.o_path |] in
+    let correct_index = 
+      let i = list_index e.e_origin.o_hyp l_hyps in 
+      (* PL: it seems that additionnally introduced hyps are in the way during 
+             normalization, hence this index shifting... *) 
+      if i=0 then 0 else i +. List.length to_introduce
+    in 	
+    app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in
   let normalization_trace =
     mk_list (Lazy.force coq_h_step) (List.map normalize_equation equations) in
 
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index bbdcd443..f5f845c2 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -13,6 +13,7 @@ Require Import BinNat.
 Require Import Setoid.
 Require Import Ring_theory.
 Require Import Ring_polynom.
+Import List.
 
 Set Implicit Arguments.
 
@@ -172,7 +173,7 @@ Section ZMORPHISM.
  Lemma gen_Zeqb_ok : forall x y, 
    Zeq_bool x y = true -> [x] == [y].
  Proof.
-  intros x y H; repeat rewrite same_genZ.
+  intros x y H.
   assert (H1 := Zeqb_ok x y H);unfold IDphi in H1.
   rewrite H1;rrefl.
  Qed.
@@ -365,9 +366,236 @@ Section NMORPHISM.
 
 End NMORPHISM.
 
+(* Words on N : initial structure for almost-rings. *)
+Definition Nword := list N.
+Definition NwO : Nword := nil.
+Definition NwI : Nword := 1%N :: nil.
+
+Definition Nwcons n (w : Nword) : Nword :=
+  match w, n with
+  | nil, 0%N => nil
+  | _, _ => n :: w
+  end.
+
+Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword :=
+  match w1, w2 with
+  | n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2'
+  | nil, _ => w2
+  | _, nil => w1
+  end.
+
+Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w.
+
+Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2).
+
+Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword :=
+  match w with
+  | m :: w' => (n*m)%N :: Nwscal n w'
+  | nil => nil
+  end.
+
+Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword :=
+  match w1 with
+  | 0%N::w1' => Nwopp (Nwmul w1' w2)
+  | n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2)
+  | nil => nil
+  end.
+Fixpoint Nw_is0 (w : Nword) : bool :=
+  match w with
+  | nil => true
+  | 0%N :: w' => Nw_is0 w'
+  | _ => false
+  end. 
+
+Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool :=
+  match w1, w2 with
+  | n1::w1', n2::w2' =>
+     if Neq_bool n1 n2 then Nweq_bool w1' w2' else false
+  | nil, _ => Nw_is0 w2
+  | _, nil => Nw_is0 w1
+  end.
+
+Section NWORDMORPHISM.
+ Variable R : Type.
+ Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
+ Variable req : R -> R -> Prop.
+  Notation "0" := rO.  Notation "1" := rI.
+  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
+  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
+  Notation "x == y" := (req x y).
+  Variable Rsth : Setoid_Theory R req.
+     Add Setoid R req Rsth as R_setoid5.
+     Ltac rrefl := gen_reflexivity Rsth.
+ Variable Reqe : ring_eq_ext radd rmul ropp req.
+   Add Morphism radd : radd_ext5.  exact (Radd_ext Reqe). Qed.
+   Add Morphism rmul : rmul_ext5.  exact (Rmul_ext Reqe). Qed.
+   Add Morphism ropp : ropp_ext5.  exact (Ropp_ext Reqe). Qed.
+
+ Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
+   Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed.
+   Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+   Ltac add_push := gen_add_push radd Rsth Reqe ARth.
+
+ Fixpoint gen_phiNword (w : Nword) : R :=
+  match w with
+  | nil => 0
+  | n :: nil => gen_phiN rO rI radd rmul n
+  | N0 :: w' => - gen_phiNword w'
+  | n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w'
+  end.
+
+ Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0.
+Proof.
+induction w; simpl in |- *; intros; auto.
+ reflexivity.
+
+ destruct a.
+  destruct w.
+   reflexivity.
+
+   rewrite IHw in |- *; trivial.
+   apply (ARopp_zero Rsth Reqe ARth).
+
+   discriminate.
+Qed.
+
+  Lemma gen_phiNword_cons : forall w n,
+    gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
+induction w.
+ destruct n; simpl in |- *; norm.
+
+ intros.
+ destruct n; norm.
+Qed.
+
+  Lemma gen_phiNword_Nwcons : forall w n,
+    gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
+destruct w; intros.
+ destruct n; norm.
+
+ unfold Nwcons in |- *.
+ rewrite gen_phiNword_cons in |- *.
+ reflexivity.
+Qed.
+
+ Lemma gen_phiNword_ok : forall w1 w2,
+   Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.
+induction w1; intros.
+ simpl in |- *.
+ rewrite (gen_phiNword0_ok _ H) in |- *.
+ reflexivity.
+
+ rewrite gen_phiNword_cons in |- *.
+ destruct w2.
+  simpl in H.
+  destruct a; try  discriminate.
+  rewrite (gen_phiNword0_ok _ H) in |- *.
+  norm.
+
+  simpl in H.
+  rewrite gen_phiNword_cons in |- *.
+  case_eq (Neq_bool a n); intros.
+   rewrite H0 in H.
+   rewrite <- (Neq_bool_ok _ _ H0) in |- *.
+   rewrite (IHw1 _ H) in |- *.
+   reflexivity.
+
+   rewrite H0 in H;  discriminate H.
+Qed.
+
+
+Lemma Nwadd_ok : forall x y,
+   gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y.
+induction x; intros.
+ simpl in |- *.
+ norm.
+
+ destruct y.
+  simpl Nwadd; norm.
+
+  simpl Nwadd in |- *.
+  repeat rewrite gen_phiNword_cons in |- *.
+  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- *.
+   destruct Reqe; constructor; trivial.
+
+   rewrite IHx in |- *.
+   norm.
+   add_push (- gen_phiNword x); reflexivity.
+Qed.
+
+Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
+simpl in |- *.
+unfold Nwopp in |- *; simpl in |- *.
+intros.
+rewrite gen_phiNword_Nwcons in |- *; norm.
+Qed.
+
+Lemma Nwscal_ok : forall n x,
+  gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x.
+induction x; intros.
+ norm.
+
+ simpl Nwscal in |- *.
+ repeat rewrite gen_phiNword_cons in |- *.
+ rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *.
+  destruct Reqe; constructor; trivial.
+
+  rewrite IHx in |- *.
+  norm.
+Qed.
+
+Lemma Nwmul_ok : forall x y,
+   gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y.
+induction x; intros.
+ norm.
+
+ destruct a.
+  simpl Nwmul in |- *.
+  rewrite Nwopp_ok in |- *.
+  rewrite IHx in |- *.
+  rewrite gen_phiNword_cons in |- *.
+  norm.
+
+  simpl Nwmul in |- *.
+  unfold Nwsub in |- *.
+  rewrite Nwadd_ok in |- *.
+  rewrite Nwscal_ok in |- *.
+  rewrite Nwopp_ok in |- *.
+  rewrite IHx in |- *.
+  rewrite gen_phiNword_cons in |- *.
+  norm.
+Qed.
+
+(* Proof that [.] satisfies morphism specifications *)
+ Lemma gen_phiNword_morph : 
+  ring_morph 0 1 radd rmul rsub ropp req
+   NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword.
+constructor.
+ reflexivity.
+
+ reflexivity.
+
+ exact Nwadd_ok.
+
+ intros.
+ unfold Nwsub in |- *.
+ rewrite Nwadd_ok in |- *.
+ rewrite Nwopp_ok in |- *.
+ norm.
+
+ exact Nwmul_ok.
+
+ exact Nwopp_ok.
+
+ exact gen_phiNword_ok.
+Qed.
+
+End NWORDMORPHISM.
+
+
+
  (* syntaxification of constants in an abstract ring:
-    the inverse of gen_phiPOS 
-    Why we do not reconnize only rI ?????? *)
+    the inverse of gen_phiPOS *)
  Ltac inv_gen_phi_pos rI add mul t :=
    let rec inv_cst t :=
    match t with
@@ -390,6 +618,18 @@ End NMORPHISM.
    end in
    inv_cst t.
 
+(* The (partial) inverse of gen_phiNword *)
+ Ltac inv_gen_phiNword rO rI add mul opp t :=
+   match t with
+     rO => constr:NwO
+   | _ =>
+     match inv_gen_phi_pos rI add mul t with
+       NotConstant => NotConstant
+     | ?p => constr:(Npos p::nil)
+     end
+   end.
+
+
 (* The inverse of gen_phiN *)
  Ltac inv_gen_phiN rO rI add mul t :=
    match t with
@@ -417,9 +657,18 @@ End NMORPHISM.
      end
    end.
 
-(* A simpl tactic reconninzing nothing *)
- Ltac inv_morph_nothing t := constr:(NotConstant).
+(* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above
+   are only optimisations that directly returns the reifid constant
+   instead of resorting to the constant propagation of the simplification
+   algorithm. *) 
+Ltac inv_gen_phi rO rI cO cI t :=
+  match t with
+  | rO => cO
+  | rI => cI
+  end.
 
+(* A simple tactic recognizing no constant *)
+ Ltac inv_morph_nothing t := constr:(NotConstant).
 
 Ltac coerce_to_almost_ring set ext rspec :=
   match type of rspec with
@@ -441,7 +690,7 @@ Ltac abstract_ring_morphism set ext rspec :=
   | ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec)
   | semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec)
   | almost_ring_theory _ _ _ _ _ _ _ =>
-      fail 1 "an almost ring cannot be abstract"
+      constr:(gen_phiNword_morph set ext rspec)
   | _ => fail 1 "bad ring structure"
   end.
 
@@ -502,7 +751,7 @@ Ltac ring_elements set ext rspec pspec sspec rk :=
        | ring_morph _ _ _ _ _ _ _  _ _ _ _ _ _  _ _ => m 
        | @semi_morph _ _ _ _ _ _  _ _ _ _ _  _ _   => 
            constr:(SRmorph_Rmorph set m) 
-       | _ => fail 2 " ici"
+       | _ => fail 2 "ring anomaly"
        end
     | _ => fail 1 "ill-formed ring kind"
     end in
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 7419f184..b55c5443 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -108,31 +108,37 @@ Ltac FV Cst CstPow add mul sub opp pow t fv :=
  (* syntaxification of ring expressions *)
 Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := 
  let rec mkP t :=
+    let f :=
     match Cst t with
     | InitialRing.NotConstant =>
         match t with 
         | (radd ?t1 ?t2) => 
+          fun _ =>
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(PEadd e1 e2)
         | (rmul ?t1 ?t2) => 
+          fun _ =>
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(PEmul e1 e2)
         | (rsub ?t1 ?t2) => 
+          fun _ => 
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(PEsub e1 e2)
         | (ropp ?t1) =>
+          fun _ =>
           let e1 := mkP t1 in constr:(PEopp e1)
         | (rpow ?t1 ?n) =>
           match CstPow n with
           | InitialRing.NotConstant => 
-            let p := Find_at t fv in constr:(PEX C p)
-          | ?c => let e1 := mkP t1 in constr:(PEpow e1 c)
+            fun _ => let p := Find_at t fv in constr:(PEX C p)
+          | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c)
           end
         | _ =>
-          let p := Find_at t fv in constr:(PEX C p)
+          fun _ => let p := Find_at t fv in constr:(PEX C p)
         end
-    | ?c => constr:(PEc c)
-    end
+    | ?c => fun _ => constr:(@PEc C c)
+    end in
+    f ()
  in mkP t.
 
 Ltac ParseRingComponents lemma :=
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 8b2ce26b..f963fc9c 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id: newring.ml4 9603 2007-02-07 00:41:16Z barras $ i*)
+(*i $Id: newring.ml4 9968 2007-07-11 15:49:07Z barras $ i*)
 
 open Pp
 open Util
@@ -166,8 +166,10 @@ let decl_constant na c =
       const_entry_boxed = true}, 
     IsProof Lemma))
 
-let ltac_call tac args =
+let ltac_call tac (args:glob_tactic_arg list) =
   TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+let ltac_acall tac (args:glob_tactic_arg list) =
+  TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)
 
 let ltac_lcall tac args =
   TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
@@ -276,12 +278,18 @@ let coq_mk_reqe = my_constant "mk_reqe"
 let coq_semi_ring_theory = my_constant "semi_ring_theory"
 let coq_mk_seqe = my_constant "mk_seqe"
 
+let ltac_inv_morph_gen = zltac"inv_gen_phi"
 let ltac_inv_morphZ = zltac"inv_gen_phiZ"
 let ltac_inv_morphN = zltac"inv_gen_phiN"
+let ltac_inv_morphNword = zltac"inv_gen_phiNword"
 let coq_abstract = my_constant"Abstract"
 let coq_comp = my_constant"Computational"
 let coq_morph = my_constant"Morphism"
 
+(* morphism *)
+let coq_ring_morph = my_constant "ring_morph"
+let coq_semi_morph = my_constant "semi_morph"
+
 (* power function *)
 let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
 let coq_pow_N_pow_N = my_constant "pow_N_pow_N"
@@ -527,6 +535,18 @@ let dest_ring env sigma th_spec =
     | _ -> error "bad ring structure"
 
 
+let dest_morph env sigma m_spec =
+  let m_typ = Retyping.get_type_of env sigma m_spec in
+  match kind_of_term m_typ with
+      App(f,[|r;zero;one;add;mul;sub;opp;req;
+              c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
+        when f = Lazy.force coq_ring_morph ->
+          (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
+    | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
+        when f = Lazy.force coq_semi_morph ->
+        (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
+    | _ -> error "bad morphism structure"
+
 
 type coeff_spec =
     Computational of constr (* equality test *)
@@ -545,22 +565,34 @@ type cst_tac_spec =
     CstTac of raw_tactic_expr
   | Closed of reference list
 
-let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac =
+let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
   match cst_tac with
       Some (CstTac t) -> Tacinterp.glob_tactic t
     | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc)
     | None ->
-        (match opp, kind with
-            None, _ ->
+        (match rk, opp, kind with
+            Abstract, None, _ ->
               let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
-          | Some opp, Some _ ->
+          | Abstract, Some opp, Some _ ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
-          | _ -> error"a tactic must be specified for an almost_ring")
+          | Abstract, Some opp, None ->
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in
+              TacArg
+                (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+          | Computational _,_,_ ->
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
+              TacArg
+                (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
+          | Morphism mth,_,_ ->
+              let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
+              TacArg
+                (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
 
 let make_hyp env c =
-  let t = (Typeops.typing env c).uj_type in
+  let t = Retyping.get_type_of env Evd.empty c in
   lapp coq_mkhypo [|t;c|]
 
 let make_hyp_list env lH =
@@ -608,7 +640,8 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign =
 
   let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in
   let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in
-  let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in
+  let cst_tac =
+    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
         Some t -> Tacinterp.glob_tactic t
@@ -980,7 +1013,8 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
   let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in
   let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in
   let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in
-  let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in
+  let cst_tac =
+    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
         Some t -> Tacinterp.glob_tactic t
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index 46121ff1..f047b729 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -1,6 +1,8 @@
 Require Import Wf.
 Require Import Coq.subtac.Utils.
 
+(** Reformulation of the Wellfounded module using subsets where possible. *)
+
 Section Well_founded.
   Variable A : Type.
   Variable R : A -> A -> Prop.
@@ -75,23 +77,70 @@ Require Import Wf_nat.
 Require Import Lt.
 
 Section Well_founded_measure.
-Variable A : Type.
-Variable f : A -> nat.
-Definition R := fun x y => f x < f y.
+  Variable A : Type.
+  Variable m : A -> nat.
+  
+  Section Acc.
+    
+    Variable P : A -> Type.
+    
+    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
+    
+    Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
+      F_sub x (fun y: { y : A | m y < m x}  => Fix_measure_F_sub (proj1_sig y) 
+        (Acc_inv r (m (proj1_sig y)) (proj2_sig y))).
+    
+    Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
+  
+  End Acc.
 
-Section FixPoint.
+  Section FixPoint.
+    Variable P : A -> Type.
+    
+    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
+    
+    Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
+    
+    Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)).
+    
+    Hypothesis
+      F_ext :
+      forall (x:A) (f g:forall y:{y:A | m y < m x}, P (`y)),
+        (forall y:{ y:A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
 
-Variable P : A -> Type.
+    Lemma Fix_measure_F_eq :
+      forall (x:A) (r:Acc lt (m x)),
+        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r.
+    Proof.
+      intros x.
+      set (y := m x).
+      unfold Fix_measure_F_sub.
+      intros r ; case r ; auto.
+    Qed.
+    
+    Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s.
+    Proof.
+      intros x r s.
+      rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto.
+    Qed.
 
-Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x.
- 
-Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (f x)) {struct r} : P x :=
-   F_sub x (fun y: { y : A | f y < f x}  => Fix_measure_F_sub (proj1_sig y) 
-   (Acc_inv r (f (proj1_sig y)) (proj2_sig y))).
+    Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)).
+    Proof.
+      intro x; unfold Fix_measure in |- *.
+      rewrite <- (Fix_measure_F_eq ).
+      apply F_ext; intros.
+      apply Fix_measure_F_inv.
+    Qed.
 
-Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)).
+    Lemma fix_measure_sub_eq :
+        forall x : A,
+          Fix_measure_sub P F_sub x =
+          let f_sub := F_sub in
+            f_sub x (fun  {y : A | m y < m x}=> Fix_measure (`y)).
+      exact Fix_measure_eq.
+    Qed.
 
-End FixPoint.
+ End FixPoint.
 
 End Well_founded_measure.
 
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v
index 1a12ac82..4610f346 100644
--- a/contrib/subtac/FunctionalExtensionality.v
+++ b/contrib/subtac/FunctionalExtensionality.v
@@ -1,3 +1,11 @@
+Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
+  f = g -> forall x, f x = g x.
+Proof.
+  intros.
+  rewrite H.
+  auto.
+Qed.
+
 Axiom fun_extensionality : forall A B (f g : A -> B), 
   (forall x, f x = g x) -> f = g.
 
@@ -23,3 +31,17 @@ Proof.
   apply (fun_extensionality_dep _ _ _ _ H).
   rewrite H0 ; auto.
 Qed.
+
+Lemma fix_sub_measure_eq_ext :
+  forall (A : Type) (f : A -> nat) (P : A -> Type)
+    (F_sub : forall x : A, (forall  {y : A | f y < f x}, P (`y)) -> P x),
+    forall x : A,
+      Fix_measure_sub A f P F_sub x =
+        F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)).
+Proof.
+  intros ; apply Fix_measure_eq ; auto.
+  intros.
+  assert(f0 = g).
+  apply (fun_extensionality_dep _ _ _ _ H).
+  rewrite H0 ; auto.
+Qed.
diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v
new file mode 100644
index 00000000..f2b216d9
--- /dev/null
+++ b/contrib/subtac/Heq.v
@@ -0,0 +1,34 @@
+Require Export JMeq.
+
+(** Notation for heterogenous equality. *)
+
+Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level).
+
+(** Do something on an heterogeneous equality appearing in the context. *)
+
+Ltac on_JMeq tac := 
+  match goal with
+    | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H
+  end.
+
+(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *)
+
+Ltac simpl_one_JMeq :=
+  on_JMeq 
+  ltac:(fun H => let H' := fresh "H" in 
+    assert (H' := JMeq_eq H) ; clear H ; rename H' into H).
+
+(** Repeat it for every possible hypothesis. *)
+
+Ltac simpl_JMeq := repeat simpl_one_JMeq.
+
+(** Just simplify an h.eq. without clearing it. *)
+
+Ltac simpl_one_dep_JMeq :=
+  on_JMeq
+  ltac:(fun H => let H' := fresh "H" in 
+    assert (H' := JMeq_eq H)).
+
+
+
+
diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
new file mode 100644
index 00000000..a00234dd
--- /dev/null
+++ b/contrib/subtac/SubtacTactics.v
@@ -0,0 +1,158 @@
+Ltac induction_with_subterm c H :=
+  let x := fresh "x" in
+  let y := fresh "y" in
+  (remember c as x ; rewrite <- y in H ; induction H ; subst).
+
+Ltac induction_on_subterm c :=
+  let x := fresh "x" in
+  let y := fresh "y" in
+  (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; 
+  clear y).
+
+Ltac induction_with_subterms c c' H :=
+  let x := fresh "x" in
+  let y := fresh "y" in
+  let z := fresh "z" in
+  let w := fresh "w" in
+  (set(x := c) ; assert(y:x = c) by reflexivity ;
+  set(z := c') ; assert(w:z = c') by reflexivity ;
+  rewrite <- y in H ; rewrite <- w in H ; 
+  induction H ; subst).
+
+
+Ltac destruct_one_pair :=
+ match goal with
+   | [H : (_ /\ _) |- _] => destruct H
+   | [H : prod _ _ |- _] => destruct H
+ end.
+
+Ltac destruct_pairs := repeat (destruct_one_pair).
+
+Ltac destruct_one_ex :=
+  let tac H := let ph := fresh "H" in destruct H as [H ph] in
+    match goal with
+      | [H : (ex _) |- _] => tac H
+      | [H : (sig ?P) |- _ ] => tac H
+      | [H : (ex2 _) |- _] => tac H
+    end.
+
+Ltac destruct_exists := repeat (destruct_one_ex).
+
+Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht].
+
+Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H].
+
+Tactic Notation "contradiction" "by" constr(t) := 
+  let H := fresh in assert t as H by auto with * ; contradiction.
+
+Ltac discriminates :=
+  match goal with
+    | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity
+    | _ => discriminate
+  end.
+
+Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex).
+
+Ltac on_last_hyp tac := 
+  match goal with
+    [ H : _ |- _ ] => tac H
+  end.
+
+Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t.
+
+Ltac revert_last := 
+  match goal with
+    [ H : _ |- _ ] => revert H
+  end.
+
+Ltac reverse := repeat revert_last.
+
+Ltac on_call f tac :=
+  match goal with
+    | H : ?T |- _  =>
+      match T with
+        | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)
+        | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
+        | context [f ?x ?y ?z ?w] => tac (f x y z w)
+        | context [f ?x ?y ?z] => tac (f x y z)
+        | context [f ?x ?y] => tac (f x y) 
+        | context [f ?x] => tac (f x)
+      end
+    | |- ?T  =>
+      match T with
+        | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)
+        | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
+        | context [f ?x ?y ?z ?w] => tac (f x y z w)
+        | context [f ?x ?y ?z] => tac (f x y z)
+        | context [f ?x ?y] => tac (f x y)
+        | context [f ?x] => tac (f x)
+      end
+  end.
+
+(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
+Ltac destruct_call f :=
+  let tac t := destruct t in on_call f tac.
+
+Ltac destruct_call_as f l :=
+  let tac t := destruct t as l in on_call f tac.
+
+Tactic Notation "destruct_call" constr(f) := destruct_call f.
+Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l.
+
+Ltac myinjection :=
+  let tac H := inversion H ; subst ; clear H in
+    match goal with
+      | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
+      | [ H : ?f ?a ?b = ?f' ?a' ?b'  |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g'  |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H
+      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
+      | _ => idtac
+    end.
+
+Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0.
+
+Ltac bang :=
+  match goal with
+    | |- ?x => 
+      match x with
+        | context [False_rect _ ?p] => elim p
+      end
+  end.
+
+Require Import Eqdep.
+
+Ltac elim_eq_rect :=
+  match goal with
+    | [ |- ?t ] => 
+      match t with
+        | context [ @eq_rect _ _ _ _ _ ?p ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+      end
+  end.
+
+Ltac real_elim_eq_rect :=
+  match goal with
+    | [ |- ?t ] => 
+      match t with
+        | context [ @eq_rect _ _ _ _ _ ?p ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+      end
+  end.
+ 
\ No newline at end of file
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 4a2208ce..76f49dd3 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -1,75 +1,65 @@
+Require Export Coq.subtac.SubtacTactics.
+
 Set Implicit Arguments.
 
-Notation "'fun' { x : A | P } => Q" :=
-  (fun x:{x:A|P} => Q)
-  (at level 200, x ident, right associativity).
+(** Wrap a proposition inside a subset. *)
 
-Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
+Notation " {{ x }} " := (tt : { y : unit | x }).
+
+(** A simpler notation for subsets defined on a cartesian product. *)
+
+Notation "{ ( x , y )  :  A  |  P }" := 
+  (sig (fun anonymous : A => let (x,y) := anonymous in P))
+  (x ident, y ident) : type_scope.
+
+(** Generates an obligation to prove False. *)
 
 Notation " ! " := (False_rect _ _).
 
-Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
-intros.
-induction t.
-exact x.
-Defined.
+(** Abbreviation for first projection and hiding of proofs of subset objects. *)
+
+Notation " ` t " := (proj1_sig t) (at level 10) : core_scope.
+Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
+
+(** Coerces objects to their support before comparing them. *)
 
-Lemma ex_pi2  : forall (A : Prop) (P : A -> Prop) (t : ex P),
- P (ex_pi1 t).
-intros A P.
-dependent inversion t.
-simpl.
-exact p.
-Defined.
+Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).
 
+(** Quantifying over subsets. *)
+
+Notation "'fun' { x : A | P } => Q" :=
+  (fun x:{x:A|P} => Q)
+  (at level 200, x ident, right associativity).
 
-Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
 Notation "'forall' { x : A | P } , Q" :=
   (forall x:{x:A|P}, Q)
   (at level 200, x ident, right associativity).
 
-Lemma subset_simpl : forall (A : Set) (P : A -> Prop) 
-	(t : sig P), P (` t).
-Proof.
-intros.
-induction t.
- simpl ; auto.
-Qed.
-
-Ltac destruct_one_pair :=
- match goal with
- | [H : (ex _) |- _] => destruct H
- | [H : (ex2 _) |- _] => destruct H
- | [H : (sig _) |- _] => destruct H
- | [H : (_ /\ _) |- _] => destruct H
-end.
-
-Ltac destruct_exists := repeat (destruct_one_pair) .
-
-Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; auto with arith.  
-
-(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
-Ltac destruct_call f :=
-  match goal with
-    | H : ?T |- _  =>
-      match T with
-         context [f ?x ?y ?z] => destruct (f x y z)
-       | context [f ?x ?y] => destruct (f x y)
-       | context [f ?x] => destruct (f x)        
-      end
-    | |- ?T  =>
-      match T with
-        context [f ?x ?y ?z] => let n := fresh "H" in set (n:=f x y z); destruct n
-        | context [f ?x ?y] => let n := fresh "H" in set (n:=f x y); destruct n
-        | context [f ?x] => let n := fresh "H" in set (n:=f x); destruct n
-      end
-    end.
+Require Import Coq.Bool.Sumbool.
+
+(** Construct a dependent disjunction from a boolean. *)
+
+Notation "'dec'" := (sumbool_of_bool) (at level 0). 
 
+(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
+
+Notation in_right := (@right _ _ _).
+Notation in_left := (@left _ _ _).
+
+(** Default simplification tactic. *)
+
+Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
+  try (solve [ red ; intros ; discriminate ]) ; auto with *.  
+
+(** Extraction directives *)
 Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
-Extract Inductive prod => "pair" [ "" ].
-Extract Inductive sigT => "pair" [ "" ].
+(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
+(* Extract Inductive sigT => "prod" [ "" ]. *)
 
 Require Export ProofIrrelevance.
+Require Export Coq.subtac.Heq.
+
+Delimit Scope program_scope with program.
diff --git a/contrib/subtac/context.ml b/contrib/subtac/context.ml
deleted file mode 100644
index 236b0ea5..00000000
--- a/contrib/subtac/context.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-open Term
-open Names
-
-type t = rel_declaration list (* name, optional coq interp, algorithmic type *)
-
-let assoc n t = 
-  let _, term, typ = List.find (fun (x, _, _) -> x = n) t in
-    term, typ
-
-let assoc_and_index x l =
-  let rec aux i = function
-      (y, term, typ) :: tl -> if x = y then i, term, typ else aux (succ i) tl
-    | [] -> raise Not_found
-  in aux 0 l
-
-let id_of_name = function
-    Name id -> id
-  | Anonymous -> raise (Invalid_argument "id_of_name")
-(*
-
-let subst_ctx ctx c = 
-  let rec aux ((ctx, n, c) as acc) = function
-      (name, None, typ) :: tl -> 
-	aux (((id_of_name name, None, rel_to_vars ctx typ) :: ctx), 
-	     pred n, c) tl
-    | (name, Some term, typ) :: tl ->
-	let t' = Term.substnl [term] n c in
-	  aux (ctx, n, t') tl
-    | [] -> acc
-  in 
-  let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in 
-    (x, rel_to_vars x z)
-*)
-
-let subst_env env c = (env, c)
diff --git a/contrib/subtac/context.mli b/contrib/subtac/context.mli
deleted file mode 100644
index 671d6f36..00000000
--- a/contrib/subtac/context.mli
+++ /dev/null
@@ -1,5 +0,0 @@
-type t = Term.rel_declaration list
-val assoc : 'a -> ('a * 'b * 'c) list -> 'b * 'c
-val assoc_and_index : 'a -> ('a * 'b * 'c) list -> int * 'b * 'c
-val id_of_name : Names.name -> Names.identifier
-val subst_env : 'a -> 'b -> 'a * 'b
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 1844fea5..2a84fdd0 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -11,52 +11,33 @@ open Evd
 open List
 open Pp
 open Util
+open Subtac_utils
 
-let reverse_array arr = 
-  Array.of_list (List.rev (Array.to_list arr))
-    
 let trace s = 
   if !Options.debug then (msgnl s; msgerr s)
   else ()
 
-(** Utilities to find indices in lists *)
-let list_index x l =
-  let rec aux i = function
-      k :: tl -> if k = x then i else aux (succ i) tl
-    | [] -> raise Not_found
-  in aux 0 l
-
-let list_assoc_index x l =
-  let rec aux i = function
-      (k, _, v) :: tl -> if k = x then i else aux (succ i) tl
-    | [] -> raise Not_found
-  in aux 0 l
-
-
 (** Substitute evar references in t using De Bruijn indices, 
   where n binders were passed through. *)
 let subst_evar_constr evs n t = 
   let seen = ref Intset.empty in
-  let evar_info id = 
-    let rec aux i = function
-	(k, x) :: tl -> 
-	  if k = id then x else aux (succ i) tl
-      | [] -> raise Not_found
-    in aux 0 evs
-  in
+  let evar_info id = List.assoc id evs in
   let rec substrec depth c = match kind_of_term c with
     | Evar (k, args) ->
-	let (id, idstr), hyps, _, _ = 
+	let (id, idstr), hyps, chop, _, _ = 
 	  try evar_info k
 	  with Not_found -> 
 	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
 	in
         seen := Intset.add id !seen;
-(* 	  (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ *)
-(* 			int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () ); *)
 	  (* Evar arguments are created in inverse order, 
 	     and we must not apply to defined ones (i.e. LetIn's)
 	  *)
+	let args = 
+	  let n = match chop with None -> 0 | Some c -> c in 
+	  let (l, r) = list_chop n (List.rev (Array.to_list args)) in
+	    List.rev r
+	in
 	let args =
 	  let rec aux hyps args acc =
 	     match hyps, args with
@@ -66,9 +47,13 @@ let subst_evar_constr evs n t =
 		   aux tlh tla acc
 	       | [], [] -> acc
 	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
-	   in aux hyps (Array.to_list args) [] 
-	 in
-	   mkApp (mkVar idstr, Array.of_list args)
+	  in aux hyps args [] 
+	in
+  	  (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (List.length args) ++ str "arguments," ++
+			int (List.length hyps) ++ str " hypotheses" ++ spc () ++
+			pp_list (fun x -> my_print_constr (Global.env ()) x) args);
+ 	   with _ -> ());
+	  mkApp (mkVar idstr, Array.of_list args)
     | _ -> map_constr_with_binders succ substrec depth c
   in 
   let t' = substrec 0 t in
@@ -78,10 +63,7 @@ let subst_evar_constr evs n t =
 (** Substitute variable references in t using De Bruijn indices, 
   where n binders were passed through. *)
 let subst_vars acc n t = 
-  let var_index id = 
-    let idx = list_index id acc in
-      idx + 1
-  in
+  let var_index id = Util.list_index id acc in
   let rec substrec depth c = match kind_of_term c with
     | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
     | _ -> map_constr_with_binders succ substrec depth c
@@ -89,47 +71,58 @@ let subst_vars acc n t =
     substrec 0 t
 
 (** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
-  to a product : forall H1 : t1, ..., forall Hn : tn, concl.
+    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
     Changes evars and hypothesis references to variable references.
+    A little optimization: don't include unnecessary let-ins and their dependencies.
 *)
-let etype_of_evar evs ev hyps =
+let etype_of_evar evs hyps concl =
   let rec aux acc n = function
       (id, copt, t) :: tl ->
 	let t', s = subst_evar_constr evs n t in
 	let t'' = subst_vars acc 0 t' in
-	let copt', s = 
-	  match copt with
+	let rest, s' = aux (id :: acc) (succ n) tl in
+	let s' = Intset.union s s' in
+	  (match copt with
 	      Some c -> 
-		let c', s' = subst_evar_constr evs n c in
-		  Some c', Intset.union s s'
-	    | None -> None, s
-	in
-	let copt' = option_map (subst_vars acc 0) copt' in
- 	let rest, s' = aux (id :: acc) (succ n) tl in
-	  mkNamedProd_or_LetIn (id, copt', t'') rest, Intset.union s' s
+		if noccurn 1 rest then lift (-1) rest, s'
+		else
+		  let c', s'' = subst_evar_constr evs n c in
+		  let c' = subst_vars acc 0 c' in
+		    mkNamedProd_or_LetIn (id, Some c', t'') rest, Intset.union s'' s'
+	    | None -> 
+		mkNamedProd_or_LetIn (id, None, t'') rest, s')
     | [] ->
-	let t', s = subst_evar_constr evs n ev.evar_concl in
+	let t', s = subst_evar_constr evs n concl in
 	  subst_vars acc 0 t', s
   in aux [] 0 (rev hyps)
 
 
 open Tacticals
     
-let rec take n l = 
-  if n = 0 then [] else List.hd l :: take (pred n) (List.tl l)    
-
 let trunc_named_context n ctx = 
   let len = List.length ctx in
-    take (len - n) ctx
+    list_firstn (len - n) ctx
   
-let eterm_obligations name nclen evm t tycon = 
+let rec chop_product n t = 
+  if n = 0 then Some t
+  else 
+    match kind_of_term t with
+      | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
+      | _ -> None
+
+let eterm_obligations name nclen isevars evm fs t tycon = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
+  trace (str " In eterm: isevars: " ++ my_print_evardefs isevars);
+  trace (str "Term given to eterm" ++ spc () ++
+	    Termops.print_constr_env (Global.env ()) t);
   let evl = List.rev (to_list evm) in
   let evn = 
     let i = ref (-1) in
       List.rev_map (fun (id, ev) -> incr i; 
-		  (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl
+		      (id, (!i, id_of_string
+			      (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))),
+		       ev)) evl
   in
   let evts = 
     (* Remove existential variables in types and build the corresponding products *)
@@ -137,8 +130,22 @@ let eterm_obligations name nclen evm t tycon =
       (fun (id, (n, nstr), ev) l ->
 	 let hyps = Environ.named_context_of_val ev.evar_hyps in
 	 let hyps = trunc_named_context nclen hyps in
-	 let evtyp, deps = etype_of_evar l ev hyps in
-	 let y' = (id, ((n, nstr), hyps, evtyp, deps)) in
+	 let evtyp, deps = etype_of_evar l hyps ev.evar_concl in
+	 let evtyp, hyps, chop = 
+	   match chop_product fs evtyp with
+	       Some t -> 
+		 (try
+		    trace (str "Choped a product: " ++ spc () ++
+			     Termops.print_constr_env (Global.env ()) evtyp ++ str " to " ++ spc () ++
+			     Termops.print_constr_env (Global.env ()) t);
+		  with _ -> ());
+		 t, trunc_named_context fs hyps, fs
+	     | None -> evtyp, hyps, 0
+	 in
+	 let loc, k = evar_source id isevars in
+	 let opacity = match k with QuestionMark o -> o | _ -> true in
+	 let opaque = if not opacity || chop <> fs then None else Some chop in
+	 let y' = (id, ((n, nstr), hyps, opaque, evtyp, deps)) in
 	   y' :: l) 
       evn []
   in 
@@ -146,26 +153,20 @@ let eterm_obligations name nclen evm t tycon =
     subst_evar_constr evts 0 t 
   in
   let evars = 
-    List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts
+    List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), deps) evts
   in
-(*     (try  *)
-(*        trace (str "Term given to eterm" ++ spc () ++ *)
-(* 		Termops.print_constr_env (Global.env ()) t); *)
-(*        trace (str "Term constructed in eterm" ++ spc () ++ *)
-(* 		Termops.print_constr_env (Global.env ()) t'); *)
-(*        ignore(iter *)
-(* 		(fun (name, typ, deps) -> *)
-(* 		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ *)
-(* 			    Termops.print_constr_env (Global.env ()) typ)) *)
-(* 		evars); *)
-(*      with _ -> ()); *)
+    (try
+       trace (str "Term constructed in eterm" ++ spc () ++
+		Termops.print_constr_env (Global.env ()) t');
+       ignore(iter
+		(fun (name, typ, _, deps) ->
+		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
+			    Termops.print_constr_env (Global.env ()) typ))
+		evars);
+     with _ -> ());
     Array.of_list (List.rev evars), t'
 
-let mkMetas n = 
-  let rec aux i acc = 
-    if i > 0 then aux (pred i) (Evarutil.mk_new_meta () :: acc)
-    else acc
-  in aux n []
+let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
 
 (* let eterm evm t (tycon : types option) =  *)
 (*   let t, tycon, evs = eterm_term evm t tycon in *)
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index 3a571ee1..76994c06 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: eterm.mli 9326 2006-10-31 12:57:26Z msozeau $ i*)
+(*i $Id: eterm.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 open Tacmach
 open Term
@@ -18,7 +18,10 @@ val mkMetas : int -> constr list
 
 (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
 
-val eterm_obligations : identifier -> int -> evar_map -> constr -> types option -> 
-  (identifier * types * Intset.t) array * constr (* Obl. name, type as product and dependencies as indexes into the array *)
+(* id, named context length, evars, number of
+   function prototypes to try to clear from evars contexts, object and optional type *)
+val eterm_obligations : identifier -> int -> evar_defs -> evar_map -> int -> constr -> types option -> 
+  (identifier * types * bool * Intset.t) array * constr
+    (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index e31326e9..43a3bec4 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -10,7 +10,7 @@
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
 
-(* $Id: g_subtac.ml4 9588 2007-02-02 16:17:13Z herbelin $ *)
+(* $Id: g_subtac.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
@@ -104,15 +104,36 @@ VERNAC COMMAND EXTEND Subtac_Obligations
 | [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ]
 END
 
+VERNAC COMMAND EXTEND Subtac_Solve_Obligation
+| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligation num (Some name) (Tacinterp.interp t) ]
+| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligation num None (Tacinterp.interp t) ]
+      END
+
 VERNAC COMMAND EXTEND Subtac_Solve_Obligations
-| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ]
-| [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ]
+| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ]
+| [ "Solve" "Obligations" "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ]
+| [ "Solve" "Obligations" ] -> 
+    [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ]
+      END
+
+VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations
+| [ "Solve" "All" "Obligations" "using" tactic(t) ] -> 
+    [ Subtac_obligations.solve_all_obligations (Tacinterp.interp t) ]
+| [ "Solve" "All" "Obligations" ] -> 
+    [ Subtac_obligations.solve_all_obligations (Subtac_obligations.default_tactic ()) ]
+      END
+
+VERNAC COMMAND EXTEND Subtac_Admit_Obligations
 | [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] 
 | [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] 
     END
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ]
+| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 5e46bead..8bc310d5 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
+(* $Id: subtac.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Global
 open Pp
@@ -37,85 +37,11 @@ open Subtac_utils
 open Coqlib
 open Printer
 open Subtac_errors
-open Context
 open Eterm
 
 let require_library dirpath =
   let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
     Library.require_library [qualid] None
-(*
-let subtac_one_fixpoint env isevars (f, decl) = 
-  let ((id, n, bl, typ, body), decl) = 
-    Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) 
-  in
-  let _ = 
-    try trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
-	       Ppconstr.pr_constr_expr body)
-    with _ -> ()
-  in ((id, n, bl, typ, body), decl)
-*)
-	      
-let subtac_fixpoint isevars l = 
-  (* TODO: Copy command.build_recursive *)
-  ()
-(*
-let save id const (locality,kind) hook =
-  let {const_entry_body = pft;
-       const_entry_type = tpo;
-       const_entry_opaque = opacity } = const in
-  let l,r = match locality with
-    | Local when Lib.sections_are_opened () ->
-        let k = logical_kind_of_goal_kind kind in
-	let c = SectionLocalDef (pft, tpo, opacity) in
-	let _ = declare_variable id (Lib.cwd(), c, k) in
-	(Local, VarRef id)
-    | Local ->
-        let k = logical_kind_of_goal_kind kind in
-        let kn = declare_constant id (DefinitionEntry const, k) in
-	(Global, ConstRef kn)
-    | Global ->
-        let k = logical_kind_of_goal_kind kind in
-        let kn = declare_constant id (DefinitionEntry const, k) in
-	(Global, ConstRef kn) in
-  Pfedit.delete_current_proof ();
-  hook l r;
-  definition_message id
-
-let save_named opacity =
-  let id,(const,persistence,hook) = Pfedit.cook_proof () in
-  let const = { const with const_entry_opaque = opacity } in
-  save id const persistence hook
-
-let check_anonymity id save_ident =
-  if atompart_of_id id <> "Unnamed_thm" then
-    error "This command can only be used for unnamed theorem"
-(*
-    message("Overriding name "^(string_of_id id)^" and using "^save_ident)
-*)
-
-let save_anonymous opacity save_ident =
-  let id,(const,persistence,hook) = Pfedit.cook_proof () in
-  let const = { const with const_entry_opaque = opacity } in
-  check_anonymity id save_ident;
-  save save_ident const persistence hook
-
-let save_anonymous_with_strength kind opacity save_ident =
-  let id,(const,_,hook) = Pfedit.cook_proof () in
-  let const = { const with const_entry_opaque = opacity } in
-  check_anonymity id save_ident;
-  (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const (Global, Proof kind) hook
-
-let subtac_end_proof = function
-  | Admitted -> admit ()
-  | Proved (is_opaque,idopt) ->
-    if_verbose show_script ();
-    match idopt with
-    | None -> save_named is_opaque
-    | Some ((_,id),None) -> save_anonymous is_opaque id
-    | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
-
-	*)
 
 open Pp
 open Ppconstr
@@ -142,48 +68,45 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
       
 let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
 
-let subtac_utils_path =
-  make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"])
-let utils_tac s =
-  lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s))
-
-let utils_call tac args =
-  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
-
 let start_proof_and_print env isevars idopt k t hook =
   start_proof_com env isevars idopt k t hook;
   print_subgoals ()
-  (*if !pcoq <> None then (out_some !pcoq).start_proof ()*)
+	  
+let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
+  
+let assumption_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is assumed")
 
-let _ = Subtac_obligations.set_default_tactic 
-    (Tacinterp.eval_tactic (utils_call "subtac_simpl" []))
+let declare_assumption env isevars idl is_coe k bl c =
+  if not (Pfedit.refining ()) then 
+    let evm, c, typ = 
+      Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None 
+    in
+      List.iter (Command.declare_one_assumption is_coe k c) idl
+  else
+    errorlabstrm "Command.Assumption"
+	(str "Cannot declare an assumption while in proof editing mode.")
+
+let vernac_assumption env isevars kind l =
+  List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l
 
 
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
-  (* check_required_library ["Coq";"Logic";"JMeq"]; *)
+(*   check_required_library ["Coq";"Logic";"JMeq"]; *)
   require_library "Coq.subtac.FixSub";
   require_library "Coq.subtac.Utils";
+  require_library "Coq.Logic.JMeq";
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
-    match command with
+  match command with
 	VernacDefinition (defkind, (locid, id), expr, hook) -> 
 	    (match expr with
 		 ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None
-(* 		   let evm, c, ctyp =  in *)
-(* 		     trace (str "Starting proof"); *)
-(* 		     Command.start_proof id goal_kind c hook; *)
-(* 		     trace (str "Started proof");	      *)
-		     
 	       | DefineBody (bl, _, c, tycon) -> 
-		   Subtac_pretyping.subtac_proof env isevars id bl c tycon
-		     (* let tac = Eterm.etermtac (evm, c) in  *)
-		     (* 		     trace (str "Starting proof"); *)
-		     (* 		     Command.start_proof id goal_kind ctyp hook; *)
-		     (* 		     trace (str "Started proof"); *)
-		     (* 		     Pfedit.by tac) *))
+		   Subtac_pretyping.subtac_proof env isevars id bl c tycon)
       | VernacFixpoint (l, b) -> 
 	  let _ = trace (str "Building fixpoint") in
 	    ignore(Subtac_command.build_recursive l b)
@@ -199,6 +122,8 @@ let subtac (loc, command) =
 	  start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
 
 
+      | VernacAssumption (stre,l) -> 
+	  vernac_assumption env isevars stre l
 
       (*| VernacEndProof e -> 
 	  subtac_end_proof e*)
@@ -237,6 +162,10 @@ let subtac (loc, command) =
 		str "Uncoercible terms:" ++ spc ()
 		++ x ++ spc () ++ str "and" ++ spc () ++ y
 	in msg_warning cmds
+
+    | Cases.PatternMatchingError (env, exn) as e ->
+	debug 2 (Himsg.explain_pattern_matching_error env exn);
+	raise e
     
     | Type_errors.TypeError (env, exn) as e ->
 	debug 2 (Himsg.explain_type_error env exn);
diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli
index 25922782..b51150aa 100644
--- a/contrib/subtac/subtac.mli
+++ b/contrib/subtac/subtac.mli
@@ -1,3 +1,2 @@
 val require_library : string -> unit
-val subtac_fixpoint : 'a -> 'b -> unit
 val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index fbe1ac37..04cad7c0 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -8,6 +8,7 @@
 
 (* $Id: cases.ml 9399 2006-11-22 16:11:53Z herbelin $ *)
 
+open Cases
 open Util
 open Names
 open Nameops
@@ -29,52 +30,6 @@ open Evarconv
 
 open Subtac_utils
 
-(* Pattern-matching errors *)
-
-type pattern_matching_error =
-  | BadPattern of constructor * constr
-  | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor * int
-  | WrongNumargInductive of inductive * int
-  | WrongPredicateArity of constr * constr * constr
-  | NeedsInversion of constr * constr
-  | UnusedClause of cases_pattern list
-  | NonExhaustive of cases_pattern list
-  | CannotInferPredicate of (constr * types) array
-
-exception PatternMatchingError of env * pattern_matching_error
-
-let raise_pattern_matching_error (loc,ctx,te) =
-  Stdpp.raise_with_loc loc (PatternMatchingError(ctx,te))
-
-let error_bad_pattern_loc loc cstr ind =
-  raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind))
-
-let error_bad_constructor_loc loc cstr ind =
-  raise_pattern_matching_error (loc, Global.env(), BadConstructor (cstr,ind))
-
-let error_wrong_numarg_constructor_loc loc env c n =
-  raise_pattern_matching_error (loc, env, WrongNumargConstructor(c,n))
-
-let error_wrong_numarg_inductive_loc loc env c n =
-  raise_pattern_matching_error (loc, env, WrongNumargInductive(c,n))
-
-let error_wrong_predicate_arity_loc loc env c n1 n2 =
-  raise_pattern_matching_error (loc, env, WrongPredicateArity (c,n1,n2))
-
-let error_needs_inversion env x t =
-  raise (PatternMatchingError (env, NeedsInversion (x,t)))
-
-module type S = sig
-  val compile_cases :
-    loc ->
-    (type_constraint -> env -> rawconstr -> unsafe_judgment) *
-      Evd.evar_defs ref ->
-    type_constraint -> 
-    env -> rawconstr option * tomatch_tuple * cases_clauses ->
-    unsafe_judgment
-end
-
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
 (************************************************************************)
@@ -1500,7 +1455,7 @@ let set_arity_signature dep n arsign tomatchl pred x =
   in
   decomp_block [] pred (tomatchl,arsign)
 
-let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
+let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
   let cook (n, l, env, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
 	let indf' = lift_inductive_family n indf in
@@ -1587,6 +1542,39 @@ let extract_arity_signature env0 tomatchl tmsign =
     | _ -> assert false
   in List.rev (buildrec 0 (tomatchl,tmsign))
 
+let extract_arity_signatures env0 tomatchl tmsign =
+  let get_one_sign tm (na,t) =
+    match tm with
+      | NotInd (bo,typ) -> 
+	  (match t with
+	    | None -> [na,bo,typ]
+	    | Some (loc,_,_,_) -> 
+ 	    user_err_loc (loc,"",
+	    str "Unexpected type annotation for a term of non inductive type"))
+      | IsInd (_,IndType(indf,realargs)) ->
+	  let (ind,params) = dest_ind_family indf in
+	  let nrealargs = List.length realargs in
+	  let realnal =
+	    match t with
+	      | Some (loc,ind',nparams,realnal) ->
+		  if ind <> ind' then
+		    user_err_loc (loc,"",str "Wrong inductive type");
+		  if List.length params <> nparams
+		    or nrealargs <> List.length realnal then
+		      anomaly "Ill-formed 'in' clause in cases";
+		  List.rev realnal
+	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
+	  let arsign = fst (get_arity env0 indf) in
+	    (na,None,build_dependent_inductive env0 indf)
+	    ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in
+  let rec buildrec = function
+    | [],[] -> []
+    | (_,tm)::ltm, x::tmsign ->
+	let l = get_one_sign tm x in
+	  l :: buildrec (ltm,tmsign)
+    | _ -> assert false
+  in List.rev (buildrec (tomatchl,tmsign))
+
 let inh_conv_coerce_to_tycon loc env isevars j tycon =
   match tycon with
     | Some p ->
@@ -1596,44 +1584,80 @@ let inh_conv_coerce_to_tycon loc env isevars j tycon =
     | None -> j
 
 let out_ind = function IsInd (_, IndType(x, y)) -> (x, y) | _ -> assert(false)
-  
-let list_mapi f l = 
-  let rec aux n = function
-      [] -> []
-    | hd :: tl -> f n hd :: aux (succ n) tl
-  in aux 0 l
-
-let constr_of_pat env isevars ty pat idents = 
-  let rec typ env ty pat idents = 
+	       
+let string_of_name name = 
+  match name with
+    | Anonymous -> "anonymous"
+    | Name n -> string_of_id n
+	
+let id_of_name n = id_of_string (string_of_name n)
+
+let make_prime_id name = 
+  let str = string_of_name name in
+    id_of_string str, id_of_string (str ^ "'")
+
+let prime avoid name = 
+  let previd, id = make_prime_id name in
+    previd, next_ident_away_from id avoid
+
+let make_prime avoid prevname =
+  let previd, id = prime !avoid prevname in
+    avoid := id :: !avoid;
+    previd, id
+
+let eq_id avoid id = 
+  let hid = id_of_string ("Heq_" ^ string_of_id id) in
+  let hid' = next_ident_away_from hid avoid in
+    hid'
+
+let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
+    
+let hole = RHole (dummy_loc, Evd.QuestionMark true)
+
+let context_of_arsign l =
+  let (x, _) = List.fold_right
+    (fun c (x, n) -> 
+      (lift_rel_context n c @ x, List.length c + n))
+    l ([], 0)
+  in x
+
+let constr_of_pat env isevars arsign pat avoid = 
+  let rec typ env (ty, realargs) pat avoid = 
     trace (str "Typing pattern " ++ Printer.pr_cases_pattern pat ++ str " in env " ++
 	     print_env env ++ str" should have type: " ++ my_print_constr env ty);
     match pat with
     | PatVar (l,name) -> 
-	let name, idents' = match name with
-	    Name n -> name, idents
+	trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name)));
+	let name, avoid = match name with
+	    Name n -> name, avoid
 	  | Anonymous -> 
-	      let n' = next_ident_away_from (id_of_string "wildcard") idents in
-		Name n', n' :: idents
+	      let previd, id = prime avoid (Name (id_of_string "wildcard")) in
+		Name id, id :: avoid 
 	in
-(* 	  trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); *)
-	  PatVar (l, name), [name, None, ty], mkRel 1, 1, idents'
+	  trace (str "Treated pattern variable " ++ str (string_of_id (id_of_name name)));
+	  PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid
     | PatCstr (l,((_, i) as cstr),args,alias) ->
-	let _ind = inductive_of_constructor cstr in
-	let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) ty in
+	let cind = inductive_of_constructor cstr in
+	let IndType (indf, _) = find_rectype env (Evd.evars_of !isevars) (lift (-(List.length realargs)) ty) in
 	let ind, params = dest_ind_family indf in
+	if ind <> cind then error_bad_constructor_loc l cstr ind;
 	let cstrs = get_constructors env indf in
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
 	assert(nb_args_constr = List.length args);
-	let idents' = idents in
-	let patargs, args, sign, env, n, m, idents' = 
+	let patargs, args, sign, env, n, m, avoid = 
 	  List.fold_right2
-	    (fun (na, c, t) ua (patargs, args, sign, env, n, m, idents)  ->
-	       let pat', sign', arg', n', idents' = typ env (lift (n - m) t) ua idents in
+	    (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid)  ->
+	       let pat', sign', arg', typ', argtypargs, n', avoid = 
+		 typ env (lift (n - m) t, []) ua avoid 
+	       in
 	       let args' = arg' :: List.map (lift n') args in
 	       let env' = push_rels sign' env in
-		 (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, idents'))
-	    ci.cs_args (List.rev args) ([], [], [], env, 0, 0, idents')
+		 (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid))
+	    ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid)
 	in
 	let args = List.rev args in
 	let patargs = List.rev patargs in
@@ -1641,120 +1665,244 @@ let constr_of_pat env isevars ty pat idents =
 	let cstr = mkConstruct ci.cs_cstr in
 	let app = applistc cstr (List.map (lift (List.length sign)) params) in
 	let app = applistc app args in
-(* 	  trace (str "New pattern: " ++ Printer.pr_cases_pattern pat'); *)
-(* 	let alname = if alias <> Anonymous then alias else Name (id_of_string "anon") in *)
-(* 	let al = alname, Some (mkRel 1), lift 1 ty in *)
-	  if alias <> Anonymous then
-	    pat', (alias, Some app, ty) :: sign, lift 1 app, n + 1, idents'
-	  else pat', sign, app, n, idents'
+	  trace (str "Getting type of app: " ++ my_print_constr env app);
+	let apptype = Retyping.get_type_of env (Evd.evars_of !isevars) app in	
+	  trace (str "Family and args of apptype: " ++ my_print_constr env apptype);
+	let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) apptype in
+	  trace (str "Got Family and args of apptype: " ++ my_print_constr env apptype);
+	  match alias with
+	      Anonymous ->
+		pat', sign, app, apptype, realargs, n, avoid
+	    | Name id ->
+		let sign = (alias, None, lift m ty) :: sign in
+		let avoid = id :: avoid in
+		let sign, i, avoid =
+		  try
+		    let env = push_rels sign env in
+		    isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars;
+		    trace (str "convertible types for alias : " ++ my_print_constr env (lift (succ m) ty)
+		    ++ my_print_constr env (lift 1 apptype));
+		    let eq_t = mk_eq (lift (succ m) ty)
+		      (mkRel 1) (* alias *)
+		      (lift 1 app) (* aliased term *)
+		    in 
+		    let neq = eq_id avoid id in
+		      (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid
+		  with Reduction.NotConvertible -> sign, 1, avoid
+		in
+		  (* Mark the equality as a hole *)
+		  pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
   in 
-  let pat', sign, y, z, idents = typ env ty pat idents in 
-  let c = it_mkProd_or_LetIn y sign in
-    trace (str "Constr_of_pat gives: " ++ my_print_constr env c);
-    pat', (sign, y), idents
-
-let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |])
-
-let vars_of_ctx = 
-  List.rev_map (fun (na, _, t) -> 
-	      match na with
-		  Anonymous -> raise (Invalid_argument "vars_of_ctx")
-		| Name n -> RVar (dummy_loc, n))
-
-(*let build_ineqs eqns pats = 
-  List.fold_left 
-    (fun (sign, c) eqn -> 
-       let acc = fold_left3
-	 (fun acc prevpat (ppat_sign, ppat_c, ppat_ty) (pat, pat_c) ->
-	    match acc with
-		None -> None
-	      | Some (sign,len, c) ->
-		  if is_included pat prevpat then
-		    let lens = List.length ppat_sign in
-		    let acc = 
-		      (lift_rels lens ppat_sign @ sign, 
-		       lens + len,
-		       mkApp (Lazy.force eq_ind,
-			      [| ppat_ty ; ppat_c ; 
-				 lift (lens + len) pat_c |]) :: c)
-		    in Some acc
-		  else None)
-	 (sign, c) eqn.patterns eqn.c_patterns pats
-       in match acc with 
-	   None -> (sign, c)
-	 | Some (sign, len, c) ->
-	     it_mkProd_or_LetIn c sign
-	     
-    )
-    ([], []) eqns*)
-
-let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
+(*   let tycon, arity = mk_tycon_from_sign env isevars arsign arity in *)
+  let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in 
+  let c = it_mkProd_or_LetIn patc sign in
+  trace (str "arity signature is : " ++ my_print_rel_context env arsign);
+  trace (str "signature is : " ++ my_print_rel_context env sign);
+  trace (str "patty, args are : " ++ my_print_constr env (applistc patty args));
+  trace (str "Constr_of_pat gives: " ++ my_print_constr env c);
+  trace (str "with args: " ++ pp_list (my_print_constr (push_rels sign env)) args);
+  pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid
+
+
+(* shadows functional version *)
+let eq_id avoid id = 
+  let hid = id_of_string ("Heq_" ^ string_of_id id) in
+  let hid' = next_ident_away_from hid !avoid in
+    avoid := hid' :: !avoid;
+    hid'
+
+let rels_of_patsign = 
+  List.map (fun ((na, b, t) as x) -> 
+    match b with 
+      | Some t' when kind_of_term t' = Rel 0 -> (na, None, t)
+      | _ -> x)
+
+let vars_of_ctx ctx = 
+  let _, y =
+    List.fold_right (fun (na, b, t)  (prev, vars) -> 
+      match b with 
+	| Some t' when kind_of_term t' = Rel 0 -> 
+	    prev, 
+	    (RApp (dummy_loc, 
+		(RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
+	| _ ->
+	    match na with
+		Anonymous -> raise (Invalid_argument "vars_of_ctx")
+	      | Name n -> n, RVar (dummy_loc, n) :: vars)
+      ctx (id_of_string "vars_of_ctx: error", [])
+  in List.rev y
+
+let rec is_included x y = 
+  match x, y with
+    | PatVar _, _ -> true
+    | _, PatVar _ -> true
+    | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias')  ->
+	if i = i' then List.for_all2 is_included args args'
+	else false
+
+(* liftsign is the current pattern's signature length *)
+let build_ineqs prevpatterns pats liftsign =
+  let _tomatchs = List.length pats in
+  let diffs = 
+    List.fold_left 
+      (fun c eqnpats -> 
+	 let acc = List.fold_left2
+	   (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) 
+	      (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) ->
+	      match acc with
+		  None -> None
+		| Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *)
+		    if is_included curpat ppat then
+		      (* Length of previous pattern's signature *)
+		      let lens = List.length ppat_sign in
+		      (* Accumulated length of previous pattern's signatures *)
+		      let len' = lens + len in
+			trace (str "Lifting " ++ my_print_constr Environ.empty_env curpat_c ++ str " by "
+				  ++ int len');
+		      let acc = 
+			((* Jump over previous prevpat signs *)
+			  lift_rel_context len ppat_sign @ sign, 
+			  len',
+			  succ n, (* nth pattern *)
+			  mkApp (Lazy.force eq_ind,
+				[| lift (lens + liftsign) ppat_ty ;
+				   liftn liftsign (succ lens) ppat_c ;
+				   lift len' curpat_c |]) :: 
+			    List.map 
+			    (fun t -> 
+			      liftn (List.length curpat_sign) (succ len') (* Jump over the curpat signature *)
+			      (lift lens t (* Jump over this prevpat signature *))) c)
+		      in Some acc
+		    else None)
+	   (Some ([], 0, 0, [])) eqnpats pats
+	 in match acc with 
+	     None -> c
+	   | Some (sign, len, _, c') ->
+	       let conj = it_mkProd_or_LetIn (mk_not (mk_conj c')) 
+		 (lift_rel_context liftsign sign) 
+	       in
+		 conj :: c)
+      [] prevpatterns
+  in match diffs with [] -> None
+    | _ -> Some (mk_conj diffs)
+	
+let subst_rel_context k ctx subst =
+  let (_, ctx') =
+    List.fold_right 
+      (fun (n, b, t) (k, acc) ->
+	 (succ k, (n, option_map (substnl subst k) b, substnl subst k t) :: acc))
+      ctx (k, [])
+  in ctx'
+
+let lift_rel_contextn n k sign =
+  let rec liftrec k = function
+    | (na,c,t)::sign ->
+	(na,option_map (liftn n k) c,type_app (liftn n k) t)
+	::(liftrec (k-1) sign)
+    | [] -> []
+  in
+  liftrec (rel_context_length sign + k) sign
+
+let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs arity =
   let i = ref 0 in
-  List.fold_left
-    (fun (branches, eqns) eqn ->
-       let _, newpatterns, pats = 
-	 List.fold_right2 (fun pat (_, ty) (idents, newpatterns, pats) -> 
-			    let x, y, z = constr_of_pat env isevars (type_of_tomatch ty) pat idents in
-			      (z, x :: newpatterns, y :: pats)) 
-	   eqn.patterns tomatchs ([], [], [])
-       in
-       let rhs_rels, signlen = 
-	 List.fold_left (fun (renv, n) (sign,_) -> 
-			   ((lift_rel_context n sign) @ renv, List.length sign + n)) 
-	   ([], 0) pats in
-       let eqs, _, _ = List.fold_left2 
-	 (fun (eqs, n, slen) (sign, c) (tm, ty) -> 
-	    let len = n + signlen in (* Number of already defined equations + signature *)
-	    let csignlen = List.length sign in
-	    let slen' = slen - csignlen in (* Lift to get pattern variables signature *)	      
-	    let c = liftn (signlen - slen) signlen c in (* Lift to jump over previous ind signatures for pattern variables outside sign 
-							in c (e.g. type arguments of constructors instanciated by variables ) *)
-	    let cstr = lift (slen' + n) c in
-(* 	      trace (str "lift " ++ my_print_constr (push_rels sign env) c ++ *)
-(* 		       str " by " ++ int  ++ str " to get " ++ *)
-(* 		       my_print_constr (push_rels sign env) cstr); *)
-	    let app = 
-	      mkApp (Lazy.force eq_ind, 
-		     [| lift len (type_of_tomatch ty); cstr; lift len tm |])
-	    in app :: eqs, succ n, slen')
-	 ([], 0, signlen) pats tomatchs
-       in
-       let eqs_rels = List.map (fun eq -> Name (id_of_string "H"), None, eq) eqs in
-(*        let ineqs = build_ineqs eqns newpatterns in *)
-       let rhs_rels' = eqs_rels @ rhs_rels in
-       let rhs_env = push_rels rhs_rels' env in
-(*        (try trace (str "branch env: " ++ print_env rhs_env) *)
-(* 	with _ -> trace (str "error in print branch env")); *)
-       let tycon = lift_tycon (List.length eqs + signlen) tycon in
-	 
-       let j = typing_fun tycon rhs_env eqn.rhs.it in
-(* 	 (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *)
-(* 		       str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *)
-(* 	  with _ -> *)
-(* 	    trace (str "Error in typed branch pretty printing")); *)
+  let (x, y, z) = 
+    List.fold_left
+      (fun (branches, eqns, prevpatterns) eqn ->
+	 let _, newpatterns, pats = 
+	   List.fold_left2
+	     (fun (idents, newpatterns, pats) pat arsign -> 
+		let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in
+		  (idents, pat' :: newpatterns, cpat :: pats))
+	      ([], [], []) eqn.patterns sign
+	 in
+	 let newpatterns = List.rev newpatterns and pats = List.rev pats in
+	 let rhs_rels, pats, signlen = 
+	   List.fold_left 
+	     (fun (renv, pats, n) (sign,c, (s, args), p) -> 
+	       (* Recombine signatures and terms of all of the row's patterns *)
+(* 	       trace (str "treating pattern:" ++ my_print_constr Environ.empty_env c); *)
+	       let sign' = lift_rel_context n sign in
+	       let len = List.length sign' in
+		 (sign' @ renv, 
+		 (* lift to get outside of previous pattern's signatures. *)
+		 (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats,
+		 len + n))
+	     ([], [], 0) pats in
+	 let pats, _ = List.fold_left 
+	   (* lift to get outside of past patterns to get terms in the combined environment. *)
+	   (fun (pats, n) (sign, c, (s, args), p) ->
+	     let len = List.length sign in
+	       ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n))
+	   ([], 0) pats 
+	 in
+	 let rhs_rels' = rels_of_patsign rhs_rels in
+	 let _signenv = push_rel_context rhs_rels' env in
+(* 	   trace (str "Env with signature is: " ++ my_print_env _signenv);  *)
+	 let ineqs = build_ineqs prevpatterns pats signlen in
+	 let eqs_rels = 
+	   let eqs = (*List.concat (List.rev eqs)*) context_of_arsign eqs in
+	   let args, nargs = 
+	     List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
+(* 	       trace (str "treating arg:" ++ my_print_constr Environ.empty_env c); *)
+	       (args @ c :: allargs, List.length args + succ n))
+	       pats ([], 0)
+	   in
+	   let args = List.rev args in
+(* 	     trace (str " equalities " ++ my_print_rel_context Environ.empty_env eqs); *)
+(* 	     trace (str " args " ++ pp_list (my_print_constr _signenv) args); *)
+	     (* Make room for substitution of prime arguments by constr patterns *)
+	     let eqs' = lift_rel_contextn signlen nargs eqs in
+	     let eqs'' = subst_rel_context 0 eqs' args in
+(* 	       trace (str " new equalities " ++ my_print_rel_context Environ.empty_env eqs'); *)
+(* 	       trace (str " subtituted equalities " ++ my_print_rel_context _signenv eqs''); *)
+	     eqs''
+	 in
+	 let rhs_rels', lift_ineqs = 
+	   match ineqs with
+	       None -> eqs_rels @ rhs_rels', 0
+	     | Some ineqs -> 
+		 (* 		 let _ = trace (str"Generated inequalities: " ++ my_print_constr env ineqs) in *)
+		 lift_rel_context 1 eqs_rels @ ((Anonymous, None, ineqs) :: rhs_rels'), 1
+	 in
+	 let rhs_env = push_rels rhs_rels' env in
+(* 	          (try trace (str "branch env: " ++ print_env rhs_env) *)
+(* 	   	with _ -> trace (str "error in print branch env")); *)
+	 let tycon = lift_tycon (List.length eqs_rels + lift_ineqs + signlen) tycon in
+	   
+	 let j = typing_fun tycon rhs_env eqn.rhs.it in
+(* 	   	 (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *)
+(* 	   		       str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *)
+(* 	   	  with _ -> *)
+(* 	   	    trace (str "Error in typed branch pretty printing")); *)
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
 	 let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
-(* 	 (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) *)
-(* 	  with _ -> trace (str "Error in branch decl pp")); *)
+	   (* 	 (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) *)
+	   (* 	  with _ -> trace (str "Error in branch decl pp")); *)
 	 let branch = 
 	   let bref = RVar (dummy_loc, branch_name) in
-	   match vars_of_ctx rhs_rels with
-	       [] -> bref
-	     | l -> RApp (dummy_loc, bref, l)
+	     match vars_of_ctx rhs_rels with
+		 [] -> bref
+	       | l -> RApp (dummy_loc, bref, l)
 	 in
-(* 	 let branch =  *)
-(* 	   List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *)
-(* 	 in *)
-(* 	 (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) *)
-(* 	  with _ -> trace (str "Error in new branch pp")); *)
-	 incr i;
-	 let rhs = { eqn.rhs with it = branch } in
-	   (branch_decl :: branches,
-	    { eqn with patterns = newpatterns; rhs = rhs } :: eqns))
-    ([], []) eqns
-    
+	 let branch = match ineqs with
+	     Some _ -> RApp (dummy_loc, branch, [ hole ])
+	   | None -> branch
+	 in
+	   (* 	 let branch =  *)
+	   (* 	   List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *)
+	   (* 	 in *)
+	   (* 	 (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) *)
+	   (* 	  with _ -> trace (str "Error in new branch pp")); *)
+	   incr i;
+	   let rhs = { eqn.rhs with it = branch } in
+	     (branch_decl :: branches,
+	      { eqn with patterns = newpatterns; rhs = rhs } :: eqns,
+	      pats :: prevpatterns))
+      ([], [], []) eqns
+  in x, y
+      
 
 (* 		   liftn_rel_declaration *)
 
@@ -1769,52 +1917,28 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
  * A type constraint but no annotation case: it is assumed non dependent.
  *)
 
-let prepare_predicate_from_tycon loc typing_fun isevars env tomatchs arsign tycon = 
-  (* We extract the signature of the arity *)
-(*   List.iter *)
-(*       (fun arsign ->  *)
-(* 	 trace (str "arity signature: " ++ my_print_rel_context env arsign)) *)
-(*     arsign; *)
-(*   let env = List.fold_right push_rels arsign env in *)
-  let allnames = List.rev (List.map (List.map pi1) arsign) in
-  let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
-  let pred = out_some (valcon_of_tycon tycon) in
-  let predcclj, pred, neqs = 
-    let _, _, eqs = 
-      List.fold_left2
-	(fun (neqs, slift, eqs) ctx (tm,ty) ->
-	   let len = List.length ctx in
-	   let _name, _, _typ' = List.hd ctx in (* FixMe: Ignoring dependent inductives *)
-	   let eq = mkApp (Lazy.force eq_ind, 
-			   [| lift (neqs + nar) (type_of_tomatch ty); 
-			      mkRel (neqs + slift);
-			      lift (neqs + nar) tm|]) 
-	   in
-	     (succ neqs, slift - len, (Anonymous, None, eq) :: eqs))
-	(0, nar, []) (List.rev arsign) tomatchs
-    in
-    let len = List.length eqs in
-      it_mkProd_wo_LetIn (lift (nar + len) pred) eqs, pred, len
-  in
-  let predccl = nf_isevar !isevars predcclj in
-(*   let env' = List.fold_right push_rel_context arsign env in *)
-(*     trace (str " Env:" ++ my_print_env env' ++ str" Predicate: " ++ my_print_constr env' predccl); *)
-    build_initial_predicate true allnames predccl, pred
-    
 let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
   (* We extract the signature of the arity *)
   let arsign = extract_arity_signature env tomatchs sign in
+(*     (try List.iter *)
+(*       (fun arsign -> *)
+(* 	 trace (str "arity signature: " ++ my_print_rel_context env arsign)) *)
+(*       arsign; *)
+(*     with _ -> trace (str "error in arity signature printing")); *)
   let env = List.fold_right push_rels arsign env in
   let allnames = List.rev (List.map (List.map pi1) arsign) in
-  let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
-(*   let _ =  *)
-(*     option_map (fun tycon ->  *)
-(* 		  isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val  *)
-(* 		    (lift_tycon_type (List.length arsign) tycon)) *)
-(*       tycon *)
-(*   in *)
-  let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
-    Some (build_initial_predicate true allnames predccl)
+    match rtntyp with
+      | Some rtntyp ->
+	  let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
+	  let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
+	    Some (build_initial_predicate true allnames predccl)
+      | None -> 
+	  match valcon_of_tycon tycon with
+	    | Some ty -> 
+		let names,pred = 
+		  oldprepare_predicate_from_tycon loc false env isevars tomatchs sign ty
+		in Some (build_initial_predicate true names pred)
+	    | None -> None
   
 let lift_ctx n ctx = 
   let ctx', _ =
@@ -1837,70 +1961,240 @@ let abstract_tomatch env tomatchs =
       ([], [], []) tomatchs
   in List.rev prev, ctx
     
+let is_dependent_ind = function
+    IsInd (_, IndType (indf, args)) when List.length args > 0 -> true
+  | _ -> false
+
+let build_dependent_signature env evars avoid tomatchs arsign =
+  let avoid = ref avoid in
+  let arsign = List.rev arsign in
+  let allnames = List.rev (List.map (List.map pi1) arsign) in
+  let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
+  let eqs, neqs, refls, slift, arsign' = 
+    List.fold_left2 
+      (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign -> 
+	 (* The accumulator:
+	    previous eqs, 
+	    number of previous eqs, 
+	    lift to get outside eqs and in the introduced variables ('as' and 'in'), 
+	    new arity signatures
+	 *)
+	 match ty with
+	     IsInd (ty, IndType (indf, args)) when List.length args > 0 ->
+	       (* Build the arity signature following the names in matched terms as much as possible *)
+	       let argsign = List.tl arsign in (* arguments in inverse application order *)
+	       let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *)
+(* 	       let _ = trace (str "Working on dependent arg: " ++ my_print_rel_context *)
+(* 				(push_rel_context argsign env) [_appsign]) *)
+(* 	       in *)
+	       let argsign = List.rev argsign in (* arguments in application order *)
+	       let env', nargeqs, argeqs, refl_args, slift, argsign' =
+		 List.fold_left2
+		   (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) ->
+(* 		      trace (str "Matching indexes: " ++ my_print_constr env arg ++ *)
+(* 			       str " and " ++ my_print_rel_context env [(name,b,t)]); *)
+		      let argt = Retyping.get_type_of env evars arg in
+		      let eq, refl_arg = 
+			if Reductionops.is_conv env evars argt t then
+			  (mk_eq (lift (nargeqs + slift) argt)
+			     (mkRel (nargeqs + slift))
+			     (lift (nargeqs + nar) arg),
+			   mk_eq_refl argt arg)
+			else
+			  (mk_JMeq (lift (nargeqs + slift) appt)
+			     (mkRel (nargeqs + slift))
+			     (lift (nargeqs + nar) argt)
+			     (lift (nargeqs + nar) arg),
+			   mk_JMeq_refl argt arg)
+		      in
+		      let previd, id = 
+			let name = 
+			  match kind_of_term arg with 
+			      Rel n -> pi1 (lookup_rel n (rel_context env))
+			    | _ -> name
+			in
+			  make_prime avoid name 
+		      in
+			(env, succ nargeqs, 
+			 (Name (eq_id avoid previd), None, eq) :: argeqs, 
+			 refl_arg :: refl_args,
+			 pred slift,
+			 (Name id, b, t) :: argsign'))
+		   (env, 0, [], [], slift, []) args argsign
+	       in
+(* 		 trace (str "neqs: " ++ int neqs ++ spc () ++ *)
+(* 			  str "nargeqs: " ++ int nargeqs ++spc () ++ *)
+(* 			  str "slift: " ++ int slift ++spc () ++ *)
+(* 			  str "nar: " ++ int nar); *)
+	       let eq = mk_JMeq 
+		 (lift (nargeqs + slift) appt)
+		 (mkRel (nargeqs + slift))
+		 (lift (nargeqs + nar) ty) 
+		 (lift (nargeqs + nar) tm) 
+	       in
+	       let refl_eq = mk_JMeq_refl ty tm in
+	       let previd, id = make_prime avoid appn in
+		 (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs, 
+		 succ nargeqs, 
+		 refl_eq :: refl_args,
+		 pred slift, 
+		 (((Name id, appb, appt) :: argsign') :: arsigns))
+		   
+	   | _ -> 
+	       (* Non dependent inductive or not inductive, just use a regular equality *)
+	       let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in
+	       let previd, id = make_prime avoid name in
+	       let arsign' = (Name id, b, typ) in
+(* 	       let _ = trace (str "Working on arg: " ++ my_print_rel_context *)
+(* 				env [arsign']) *)
+(* 	       in *)
+	       let tomatch_ty = type_of_tomatch ty in
+	       let eq = 
+		 mk_eq (lift nar tomatch_ty)
+		   (mkRel slift) (lift nar tm)
+(* 		 mk_eq (lift (neqs + nar) tomatch_ty)  *)
+(* 		   (mkRel (neqs + slift)) (lift (neqs + nar) tm)  *)
+	       in
+		 ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs, 
+		  (mk_eq_refl tomatch_ty tm) :: refl_args,
+		  pred slift, (arsign' :: []) :: arsigns))
+      ([], 0, [], nar, []) tomatchs arsign
+  in 
+  let arsign'' = List.rev arsign' in
+    assert(slift = 0); (* we must have folded over all elements of the arity signature *)
+(*     begin try  *)
+(*       List.iter  *)
+(* 	(fun arsign -> *)
+(* 	   trace (str "old arity signature: " ++ my_print_rel_context env arsign)) *)
+(* 	arsign; *)
+      List.iter
+	(fun c ->
+	   trace (str "new arity signature: " ++ my_print_rel_context env c))
+	(arsign'');
+(*     with _ -> trace (str "error in arity signature printing") *)
+(*     end; *)
+    let env' = push_rel_context (context_of_arsign arsign') env in
+    let _eqsenv = push_rel_context (context_of_arsign eqs) env' in
+      (try trace (str "Where env with eqs is: " ++ my_print_env _eqsenv);
+	 trace (str "args: " ++ List.fold_left (fun acc x -> acc ++ my_print_constr env x)
+		  (mt()) refls)
+       with _ -> trace (str "error in equalities signature printing"));
+      arsign'', allnames, nar, eqs, neqs, refls
+      
+(* 	       let len = List.length eqs in *)
+(* 		 it_mkProd_wo_LetIn (lift (nar + len) pred) eqs, pred, len *)
+
+
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
   
-let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
-  let tycon0 = tycon in
+let liftn_rel_context n k sign =  
+  let rec liftrec k = function
+    | (na,c,t)::sign ->
+	(na,option_map (liftn n k) c,type_app (liftn n k) t)
+	::(liftrec (k-1) sign)
+    | [] -> []
+  in
+    liftrec (k + rel_context_length sign) sign
+
+let nf_evars_env evar_defs (env : env) : env = 
+  let nf t = nf_isevar evar_defs t in
+  let env0 : env = reset_context env in 
+  let f e (na, b, t) e' : env =
+    Environ.push_named (na, option_map nf b, nf t) e'
+  in
+  let env' = Environ.fold_named_context f ~init:env0 env in
+    Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, option_map nf b, nf t) e')
+     ~init:env' env
+      
+let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env eqns in
      
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
   let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+(*   isevars := nf_evar_defs !isevars; *)
+(*   let env = nf_evars_env !isevars (env : env) in *)
+(*      trace (str "Evars : " ++ my_print_evardefs !isevars); *)
+(*     trace (str "Env : " ++ my_print_env env); *)
+    
   let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in
   let tomatchs_len = List.length tomatchs_lets in
   let tycon = lift_tycon tomatchs_len tycon in
   let env = push_rel_context tomatchs_lets env in
-    match predopt with
-	None ->	  
-	  let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in
-	  let matx = List.rev matx in
-	  let len = List.length lets in
-	  let sign = 
-	    let arsign = extract_arity_signature env tomatchs (List.map snd tomatchl) in
-	      List.map (lift_rel_context len) arsign
-	  in
-	  let env = push_rels lets env in	      
-	  let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
-	  let tycon = lift_tycon len tycon in
-	  let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
-	  let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in
-	    
-	  (* We build the elimination predicate if any and check its consistency *)
-	  (* with the type of arguments to match *)
-	  let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon in
-	  (* We push the initial terms to match and push their alias to rhs' envs *)
-	  (* names of aliases will be recovered from patterns (hence Anonymous here) *)
-	  let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-	    
-	  let pb =
-	    { env      = env;
-	      isevars  = isevars;
-	      pred     = Some pred;
-	      tomatch  = initial_pushed;
-	      history  = start_history (List.length initial_pushed);
-	      mat      = matx;
-	      caseloc  = loc;
-	      typing_function = typing_fun } in
-	    
-	  let _, j = compile pb in
-	    (* We check for unused patterns *)
-	    List.iter (check_unused_pattern env) matx;
-	    let ty = out_some (valcon_of_tycon tycon0) in
-	    let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
-	    let j = 
-	      { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
-		uj_type = ty; }
-	    in
-	      inh_conv_coerce_to_tycon loc env isevars j tycon0
-
-      | Some rtntyp ->
-	  (* We build the elimination predicate if any and check its consistency *)
-	  (* with the type of arguments to match *)
-	  let tmsign = List.map snd tomatchl in
-	  let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon rtntyp in
-	    
+  let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in
+    if predopt = None then
+      let len = List.length eqns in 
+      let sign, allnames, signlen, eqs, neqs, args = 
+	(* The arity signature *)
+	let arsign = extract_arity_signatures env tomatchs (List.map snd tomatchl) in
+	  (* Build the dependent arity signature, the equalities which makes
+	     the first part of the predicate and their instantiations. *)
+	  trace (str "Arity signatures : " ++ my_print_rel_context env (context_of_arsign arsign));
+	let avoid = [] in
+	  build_dependent_signature env (Evd.evars_of !isevars) avoid tomatchs arsign
+
+      in
+      let tycon_constr = 
+	match valcon_of_tycon tycon with
+	  | None -> mkExistential env isevars 
+	  | Some t -> t
+      in
+      let lets, matx = 
+	(* Type the rhs under the assumption of equations *)
+	constrs_of_pats typing_fun tycon env isevars matx tomatchs sign neqs 
+	  (eqs : rel_context list) (lift (signlen + neqs) tycon_constr) in
+	
+      let matx = List.rev matx in
+      let _ = assert(len = List.length lets) in
+      let env = push_rels lets env in
+      let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
+      let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
+      let args = List.rev_map (lift len) args in
+      let sign = List.map (lift_rel_context len) sign in	
+      let pred = it_mkProd_wo_LetIn (lift (signlen + neqs) tycon_constr) 
+	(context_of_arsign eqs) in
+
+      let pred = liftn len (succ signlen) pred in
+(* 	it_mkProd_wo_LetIn (lift (len + signlen + neqs) tycon_constr) (liftn_rel_context len signlen eqs) in*) 
+      (* We build the elimination predicate if any and check its consistency *)
+      (* with the type of arguments to match *)
+      let _signenv = List.fold_right push_rels sign env in
+(* 	trace (str "Using predicate: " ++ my_print_constr signenv pred ++ str " in env: " ++ my_print_env signenv ++ str " len is " ++ int len); *)
+
+      let pred =
+	(* prepare_predicate_from_tycon loc typing_fun isevars env tomatchs eqs allnames signlen sign tycon in *)
+	build_initial_predicate true allnames pred in
+	(* We push the initial terms to match and push their alias to rhs' envs *)
+	(* names of aliases will be recovered from patterns (hence Anonymous here) *)
+      let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+	
+      let pb =
+	{ env      = env;
+	  isevars  = isevars;
+	  pred     = Some pred;
+	  tomatch  = initial_pushed;
+	  history  = start_history (List.length initial_pushed);
+	  mat      = matx;
+	  caseloc  = loc;
+	  typing_function = typing_fun } in
+	
+      let _, j = compile pb in
+	(* We check for unused patterns *)
+	List.iter (check_unused_pattern env) matx;
+	let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
+	let j = 
+	  { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
+	    uj_type = lift (-tomatchs_len) (nf_isevar !isevars tycon_constr); }
+	in j
+(* 	  inh_conv_coerce_to_tycon loc env isevars j tycon0 *)
+    else
+      (* We build the elimination predicate if any and check its consistency *)
+      (* with the type of arguments to match *)
+      let tmsign = List.map snd tomatchl in
+      let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in
+	
 	  (* We push the initial terms to match and push their alias to rhs' envs *)
 	  (* names of aliases will be recovered from patterns (hence Anonymous here) *)
 	  let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
diff --git a/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli
index 9e902126..02fe016d 100644
--- a/contrib/subtac/subtac_cases.mli
+++ b/contrib/subtac/subtac_cases.mli
@@ -19,32 +19,5 @@ open Rawterm
 open Evarutil
 (*i*)
 
-type pattern_matching_error =
-  | BadPattern of constructor * constr
-  | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor * int
-  | WrongNumargInductive of inductive * int
-  | WrongPredicateArity of constr * constr * constr
-  | NeedsInversion of constr * constr
-  | UnusedClause of cases_pattern list
-  | NonExhaustive of cases_pattern list
-  | CannotInferPredicate of (constr * types) array
-
-exception PatternMatchingError of env * pattern_matching_error
-
-val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a
-
-val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
-
-(*s Compilation of pattern-matching. *)
-
-module type S = sig
-  val compile_cases :
-    loc ->
-    (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
-    type_constraint -> 
-    env -> rawconstr option * tomatch_tuple * cases_clauses ->
-    unsafe_judgment
-end
-
-module Cases_F(C : Coercion.S) : S
+(*s Compilation of pattern-matching, subtac style. *)
+module Cases_F(C : Coercion.S) : Cases.S
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 3613ec4f..c764443f 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: subtac_coercion.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
+(* $Id: subtac_coercion.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Util
 open Names
@@ -26,7 +26,6 @@ open Subtac_utils
 open Coqlib
 open Printer
 open Subtac_errors
-open Context
 open Eterm
 open Pp
 
@@ -86,6 +85,13 @@ module Coercion = struct
 
   let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c
 
+  let lift_args n sign =
+    let rec liftrec k = function
+      | t::sign -> liftn n k t :: (liftrec (k-1) sign)
+      | [] -> []
+    in
+      liftrec (List.length sign) sign
+
   let rec mu env isevars t =   
     let isevars = ref isevars in
     let rec aux v = 
@@ -113,15 +119,41 @@ module Coercion = struct
 (*       (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++  *)
 (* 		  str " to "++ my_print_constr env y) *)
 (*        with _ -> ()); *)
-      try 
-	isevars := the_conv_x_leq env x y !isevars;
-(* 	(try debug 1 (str "Unified " ++ (my_print_constr env x) ++  *)
-(* 			str " and "++ my_print_constr env y); *)
-(* 	 with _ -> ()); *)
-	None
-      with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
+      let x = hnf env isevars x and y = hnf env isevars y in
+	try 
+	  isevars := the_conv_x_leq env x y !isevars;
+	  (* 	(try debug 1 (str "Unified " ++ (my_print_constr env x) ++  *)
+	  (* 			str " and "++ my_print_constr env y); *)
+	  (* 	 with _ -> ()); *)
+	  None
+	with Reduction.NotConvertible -> coerce' env x y
     and coerce' env x y : (Term.constr -> Term.constr) option =
       let subco () = subset_coerce env isevars x y in
+      let rec coerce_application typ c c' l l' =
+	let len = Array.length l in
+	let rec aux tele typ i co = 
+	  if i < len then
+	    let hdx = l.(i) and hdy = l'.(i) in
+	      try isevars := the_conv_x_leq env hdx hdy !isevars;
+		let (n, eqT, restT) = destProd typ in
+		aux (hdx :: tele) (subst1 hdy restT) (succ i) co
+	      with Reduction.NotConvertible ->
+		let (n, eqT, restT) = destProd typ in
+		let restargs = lift_args 1 
+		  (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
+		in 
+		let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in
+		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
+		let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
+(* 		let jmeq = mkApp (Lazy.force jmeq_ind, [| eqT; hdx; eqT; hdy |]) in *)
+		let evar = make_existential dummy_loc env isevars eq in
+		let eq_app x = mkApp (Lazy.force eq_rect,
+				      [| eqT; hdx; pred; x; hdy; evar|]) in
+		  trace (str"Inserting coercion at application");
+		  aux (hdy :: tele) (subst1 hdy restT) (succ i)  (fun x -> eq_app (co x))
+	  else co
+	in aux [] typ 0 (fun x -> x)
+      in
 (* 	(try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++  *)
 (* 		    str " to "++ my_print_constr env y); *)
 (* 	 with _ -> ()); *)
@@ -214,40 +246,25 @@ module Coercion = struct
 					    mkApp (prod.intro, [| a'; b'; x ; y |]))
 			   end
 		       else
-			 (* if len = 1 && len = Array.length l' && i = i' then *)
-(* 			   let argx, argy = l.(0), l'.(0) in *)
-(* 			   let indtyp = Inductiveops.type_of_inductive env i in *)
-(* 			   let argname, argtype, _ = destProd indtyp in *)
-(* 			   let eq = *)
-(* 			     mkApp (Lazy.force eqind, [| argtype; argx; argy |]) *)
-(* 			   in *)
-(* 			   let pred = mkLambda (argname, argtype,  *)
-(* 						mkApp (mkInd i, [| mkRel 1 |])) *)
-(* 			   in *)
-(* 			   let evar = make_existential dummy_loc env isevars eq in *)
-(* 			     Some (fun x -> *)
-(* 				     mkApp (Lazy.force eqrec,  *)
-(* 					    [| argtype; argx; pred; x; argy; evar |])) *)
-(* 			 else  *)subco ()
+			 if i = i' && len = Array.length l' then
+			   let evm = evars_of !isevars in
+			   let typ = Typing.type_of env evm c in
+			     (try subco () 
+			      with NoSubtacCoercion ->
+				
+(* 			     if not (is_arity env evm typ) then *)
+			       Some (coerce_application typ c c' l l'))
+(* 			     else subco () *)
+			 else
+			   subco ()
 		 | x, y when x = y ->
-		     let lam_type = Typing.type_of env (evars_of !isevars) c in
-		     let rec coerce typ i co =
-		       if i < Array.length l then
-			 let hdx = l.(i) and hdy = l'.(i) in
-			 let (n, eqT, restT) = destProd typ in
-			 let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in
-			 let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
-			 let evar = make_existential dummy_loc env isevars eq in
-			 let eq_app x = mkApp (Lazy.force eq_rect,
-					       [| eqT; hdx; pred; x; hdy; evar|])
-			 in 
-			   coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x))
-		       else co
-		     in
-		       if Array.length l = Array.length l' then (
-			 trace (str"Inserting coercion at application");
-			 Some (coerce lam_type 0 (fun x -> x))
-		       ) else subco ()
+		     if Array.length l = Array.length l' then
+		       let evm = evars_of !isevars in
+		       let lam_type = Typing.type_of env evm c in
+(* 			 if not (is_arity env evm lam_type) then ( *)
+			   Some (coerce_application lam_type c c' l l')
+(* 			 ) else subco () *)
+		     else subco ()
 		 | _ -> subco ())
 	  | _, _ ->  subco ()
 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 68ab8c46..86139039 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -56,7 +56,6 @@ let interp_gen kind isevars env
                ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
-  let c' = Subtac_utils.rewrite_cases env c' in
 (*     (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *)
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
     evar_nf isevars c'
@@ -178,10 +177,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let env = Global.env() in 
   let nc = named_context env in
   let nc_len = named_context_length nc in
-(*   let pr c = my_print_constr env c in *)
-(*   let prr = Printer.pr_rel_context env in *)
-(*   let prn = Printer.pr_named_context env in *)
-(*   let pr_rel env = Printer.pr_rel_context env in *)
+  let pr c = my_print_constr env c in
+  let prr = Printer.pr_rel_context env in
+  let _prn = Printer.pr_named_context env in
+  let _pr_rel env = Printer.pr_rel_context env in
 (*   let _ =  *)
 (*     try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++  *)
 (* 		 Ppconstr.pr_binders bl ++ str " : " ++  *)
@@ -193,40 +192,42 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in
   let before_length, after_length = List.length before, List.length after in
   let argid = match argname with Name n -> n | _ -> assert(false) in
-  let _liftafter = lift_binders 1 after_length after in
+  let liftafter = lift_binders 1 after_length after in
   let envwf = push_rel_context before env in
   let wf_rel, wf_rel_fun, measure_fn = 
     let rconstr_body, rconstr = 
       let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in
        let env = push_rel_context [arg] envwf in
        let capp = interp_constr isevars env app in
- 	capp, mkLambda (argname, argtyp, capp)
+ 	 capp, mkLambda (argname, argtyp, capp)
      in
+      trace (str"rconstr_body: " ++ pr rconstr_body);
        if measure then
  	let lt_rel = constr_of_global (Lazy.force lt_ref) in
  	let name s = Name (id_of_string s) in
- 	let wf_rel_fun = 
- 	  (fun x y ->
- 	      mkApp (lt_rel, [| subst1 x rconstr_body; 
- 				subst1 y rconstr_body |])) 
- 	in
+ 	let wf_rel_fun lift x y = (* lift to before_env *)
+	  trace (str"lifter rconstr_body:" ++ pr (liftn lift 2 rconstr_body));
+ 	  mkApp (lt_rel, [| subst1 x (liftn lift 2 rconstr_body); 
+ 			    subst1 y (liftn lift 2 rconstr_body) |])
+	in
  	let wf_rel = 
  	  mkLambda (name "x", argtyp,
  		    mkLambda (name "y", lift 1 argtyp,
- 			      wf_rel_fun (mkRel 2) (mkRel 1)))
+ 			      wf_rel_fun 0 (mkRel 2) (mkRel 1)))
  	in
  	  wf_rel, wf_rel_fun , Some rconstr
-       else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None
+       else rconstr, (fun lift x y -> mkApp (rconstr, [|x; y|])), None
   in
   let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
   in
   let argid' = id_of_string (string_of_id argid ^ "'") in
-  let wfarg len = (Name argid', None, 
+  let wfarg len = (Name argid', None,
   		   mkSubset (Name argid') (lift len argtyp) 
-		     (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
+		     (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1))))
   in
   let top_bl = after @ (arg :: before) in
-  let intern_bl = after @ (wfarg 1 :: arg :: before) in
+  let intern_bl = liftafter @ (wfarg 1 :: arg :: before) in
+    (try trace (str "Intern bl: " ++ prr intern_bl) with _ -> ());
   let top_env = push_rel_context top_bl env in
   let _intern_env = push_rel_context intern_bl env in
   let top_arity = interp_type isevars top_env arityc in
@@ -234,36 +235,45 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let projection = 
     mkApp (proj, [| argtyp ;
 		    (mkLambda (Name argid', argtyp,
-			       (wf_rel_fun (mkRel 1) (mkRel 3)))) ;
+			       (wf_rel_fun 1 (mkRel 1) (mkRel 3)))) ;
 		    mkRel 1
 		 |])
   in
-    (*   (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ()); *)
-  let intern_arity = substnl [projection] after_length top_arity in 
-(*   (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ()); *)
+  let intern_arity = it_mkProd_or_LetIn top_arity after in
+    (try trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity);
+       trace (str "Before lifting arity: " ++ my_print_constr env top_arity) with _ -> ());
+  (* Top arity is in top_env = after :: arg :: before *)
+(*   let intern_arity' = liftn 1 (succ after_length) top_arity in (\* arity in after :: wfarg :: arg :: before *\) *)
+(*       (try trace (str "projection: " "After lifting arity: " ++ my_print_constr env intern_arity' ++ spc ()); *)
+(* 	 trace (str "Intern env: " ++ prr intern_bl ++ str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ()); *)
+  let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for arg *)
+  (try trace (str "Top arity after subst: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ());
+(*   let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *)
+(*   (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *)
   let intern_before_env = push_rel_context before env in
-  let intern_fun_bl = after @ [wfarg 1]  in
+(*   let intern_fun_bl = liftafter @ [wfarg 1]  in (\* FixMe dependencies *\) *)
 (*   (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *)
-  let intern_fun_arity = intern_arity in
-(*   (try debug 2 (str "Intern fun arity: " ++  *)
-(* 		  my_print_constr intern_env intern_fun_arity) with _ -> ()); *)
-  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
+  (try trace (str "Intern arity: " ++
+		  my_print_constr _intern_env intern_arity) with _ -> ());
+  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
+  (try trace (str "Intern fun arity product: " ++
+		  my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ());
   let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
-  let fun_bl = after @ (intern_fun_binder :: [arg]) in
+  let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
 (*   (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *)
   let fun_env = push_rel_context fun_bl intern_before_env in
   let fun_arity = interp_type isevars fun_env arityc in
   let intern_body = interp_casted_constr isevars fun_env body fun_arity in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
-(*   let _ =  *)
-(*       try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++ *)
-(* 		   str "Intern bl" ++ prr intern_bl ++ spc () ++ *)
-(* 		   str "Top bl" ++ prr top_bl ++ spc () ++ *)
-(* 		   str "Intern arity: " ++ pr intern_arity ++ *)
-(* 		   str "Top arity: " ++ pr top_arity ++ spc () ++ *)
+  let _ =
+    try trace ((* str "Fun bl: " ++ prr fun_bl ++ spc () ++ *)
+		 str "Intern bl" ++ prr intern_bl ++ spc ())
+(* 		 str "Top bl" ++ prr top_bl ++ spc () ++ *)
+(* 		 str "Intern arity: " ++ pr intern_arity ++ *)
+(* 		 str "Top arity: " ++ pr top_arity ++ spc () ++ *)
 (* 		   str "Intern body " ++ pr intern_body_lam) *)
-(*       with _ -> () *)
-(*   in *)
+    with _ -> ()
+  in
   let _impl = 
     if Impargs.is_implicit_args()
     then Impargs.compute_implicits top_env top_arity
@@ -276,13 +286,16 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 	  mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
 		 [| argtyp ;
 		    wf_rel ;
-		    make_existential dummy_loc intern_before_env isevars wf_proof ;
+		    make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ;
 		    prop ;
 		    intern_body_lam |])
       | Some f ->
-	  mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), 
-		 [| argtyp ; f ; prop ;
-		    intern_body_lam |])
+	  lift (succ after_length) 
+	    (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), 
+		    [| argtyp ; 
+		       f ;
+		       prop ;
+		       intern_body_lam |]))
   in
   let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
   let def = it_mkLambda_or_LetIn def_appl binders_rel in
@@ -294,15 +307,22 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 (* 		     ++ str "Coq type: " ++ my_print_constr env fullctyp)  *)
 (*      with _ -> ()  *)
 (*   in *)
-  let evm = non_instanciated_map env isevars in
+  let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in
+  let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in
+  let evm = non_instanciated_map env isevars evm in
+
     (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
-  let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
+  let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in
     (*     (try trace (str "Generated obligations : "); *)
 (*        Array.iter *)
     (* 	 (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *)
     (* 	 evars; *)
     (*      with _ -> ());     *)
     Subtac_obligations.add_definition recname evars_def fullctyp evars
+
+let nf_evar_context isevars ctx = 
+  List.map (fun (n, b, t) -> 
+    (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
     
 let build_mutrec l boxed = 
   let sigma = Evd.empty and env = Global.env () in 
@@ -368,10 +388,13 @@ let build_mutrec l boxed =
       let (isevars, info, def) = defrec.(i) in
 	(*       let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *)
       let def = evar_nf isevars def in
+      let x, y, typ = arrec.(i) in
+      let typ = evar_nf isevars typ in
+      arrec.(i) <- (x, y, typ);
+      let rec_sign = nf_evar_context !isevars rec_sign in
       let isevars = Evd.undefined_evars !isevars in
 	(*       let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *)
       let evm = Evd.evars_of isevars in
-      let _, _, typ = arrec.(i) in
       let id = namerec.(i) in
 	(* Generalize by the recursive prototypes  *)
       let def = 
@@ -379,7 +402,7 @@ let build_mutrec l boxed =
       and typ = 
 	Termops.it_mkNamedProd_or_LetIn typ rec_sign
       in
-      let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in
+      let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in
 	collect_evars (succ i) ((id, def, typ, evars) :: acc)
     else acc
   in 
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
deleted file mode 100644
index bb35833f..00000000
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ /dev/null
@@ -1,154 +0,0 @@
-open Global
-open Pp
-open Util
-open Names
-open Sign
-open Evd
-open Term
-open Termops
-open Reductionops
-open Environ
-open Type_errors
-open Typeops
-open Libnames
-open Classops
-open List
-open Recordops 
-open Evarutil
-open Pretype_errors
-open Rawterm
-open Evarconv
-open Pattern
-open Dyn
-open Topconstr
-
-open Subtac_coercion
-open Subtac_utils
-open Coqlib
-open Printer
-open Subtac_errors
-open Context
-open Eterm
-
-
-let mkAppExplC (f, args) = CAppExpl (dummy_loc, (None, f), args)
-
-let mkSubset name typ prop = 
-  mkAppExplC (sig_ref,
-	      [ typ; mkLambdaC ([name], typ, prop) ])
-	      
-let mkProj1 u p x = 
-  mkAppExplC (proj1_sig_ref, [ u; p; x ])
-
-let mkProj2 u p x = 
-  mkAppExplC (proj2_sig_ref, [ u; p; x ])
-
-let list_of_local_binders l = 
-  let rec aux acc = function
-      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, c) :: acc) tl
-    | Topconstr.LocalRawAssum (nl, c) :: tl -> 
-	aux (List.fold_left (fun acc n -> (n, c) :: acc) acc nl) tl
-    | [] -> List.rev acc
-  in aux [] l
-       
-let abstract_constr_expr_bl abs c bl =
-  List.fold_right (fun (n, t) c -> abs ([n], t, c)) bl c
-
-let pr_binder_list b = 
-  List.fold_right (fun ((loc, name), t) acc -> Nameops.pr_name name ++ str " : " ++
-		     Ppconstr.pr_constr_expr t ++ spc () ++ acc) b (mt ()) 
-
-
-let rec rewrite_rec_calls l c = c
-(*
-let rewrite_fixpoint env l (f, decl) = 
-  let (id, (n, ro), bl, typ, body) = f in
-  let body = rewrite_rec_calls l body in
-    match ro with
-	CStructRec -> ((id, (n, ro), bl, typ, body), decl)
-      | CWfRec wfrel -> 
-	  let bls = list_of_local_binders bl in
-	  let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id id ++ 
-			 Ppconstr.pr_binders bl ++ str " : " ++ 
-			 Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
-			 Ppconstr.pr_constr_expr body)
-	  in
-	  let before, after = list_chop n bls in
-	  let _ = trace (str "Binders before the recursion arg: " ++ spc () ++
-			 pr_binder_list before ++ str "; after the recursion arg: " ++
-			 pr_binder_list after)
-	  in
-	  let ((locn, name) as lnid, ntyp), after = match after with
-	      hd :: tl -> hd, tl
-	    | _ -> assert(false) (* Rec arg must be in after *)
-	  in
-	  let nid = match name with
-	      Name id -> id
-	    | Anonymous -> assert(false) (* Rec arg _must_ be named *)
-	  in
-	  let _wfproof = 
-	    let _wf_rel = mkAppExplC (well_founded_ref, [ntyp; wfrel]) in
-	      (*make_existential_expr dummy_loc before wf_rel*)
-	      mkRefC lt_wf_ref
-	  in
-	  let nid', accproofid = 
-	    let nid = string_of_id nid in
-	      id_of_string (nid ^ "'"), id_of_string ("Acc_" ^ nid)
-	  in
-	  let lnid', laccproofid = (dummy_loc, Name nid'), (dummy_loc, Name accproofid) in
-	  let wf_prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
-	  let lam_wf_prop = mkLambdaC ([lnid'], ntyp, wf_prop) in
-	  let typnid' = mkSubset lnid' ntyp wf_prop in
-	  let internal_type = 
-	    abstract_constr_expr_bl mkProdC 
-	      (mkProdC ([lnid'], typnid', 
-			mkLetInC (lnid, mkProj1 ntyp lam_wf_prop (mkIdentC nid'), 
-				  abstract_constr_expr_bl mkProdC typ after)))
-	      before
-	  in
-	  let body' =
-	    let body =
-	      (* cast or we will loose some info at pretyping time as body
-		 is a function *)
-	      CCast (dummy_loc, body,  CastConv DEFAULTcast, typ) 
-	    in
-	    let body' = (* body abstracted by rec call *)
-	      mkLambdaC ([(dummy_loc, Name id)], internal_type, body)
-	    in
-	      mkAppC (body',
-		      [mkLambdaC 
-			 ([lnid'], typnid',
-			  mkAppC (mkIdentC id, 
-				  [mkProj1 ntyp lam_wf_prop (mkIdentC nid');
-				   (mkAppExplC (acc_inv_ref,
-						[ ntyp; wfrel;
-						  mkIdentC nid;
-						  mkIdentC accproofid;
-						  mkProj1 ntyp lam_wf_prop (mkIdentC nid');
-						  mkProj2 ntyp lam_wf_prop (mkIdentC nid') ])) ]))])
-	  in
-	  let acctyp = mkAppExplC (acc_ref, [ ntyp; wfrel; mkIdentC nid ]) in
-	  let bl' = 
-	    let rec aux acc = function
-		Topconstr.LocalRawDef _ as x :: tl -> 
-		  aux (x :: acc) tl
-	      | Topconstr.LocalRawAssum (bl, typ) as assum :: tl ->
-		  let rec aux' bl' = function
-		      ((loc, name') as x) :: tl ->
-			if name' = name then
-			  (if tl = [] then [] else [LocalRawAssum (tl, typ)]) @
-			  LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
-			    [LocalRawAssum (List.rev (x :: bl'), typ)]
-			else aux' (x :: bl') tl
-		    | [] -> [assum]
-		  in aux (aux' [] bl @ acc) tl
-	      | [] -> List.rev acc
-	    in aux [] bl
-	  in
-	  let _ = trace (str "Rewrote fixpoint: " ++ Ppconstr.pr_id id ++ 
-			 Ppconstr.pr_binders bl' ++ str " : " ++ 
-			 Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
-			 Ppconstr.pr_constr_expr body')
-	  in (id, (succ n, ro), bl', typ, body'), decl
-
-*)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
deleted file mode 100644
index 149e7580..00000000
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-val mkAppExplC :
-  Libnames.reference * Topconstr.constr_expr list -> Topconstr.constr_expr
-val mkSubset :
-  Names.name Util.located ->
-  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
-val mkProj1 :
-  Topconstr.constr_expr ->
-  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
-val mkProj2 :
-  Topconstr.constr_expr ->
-  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
-val list_of_local_binders :
-  Topconstr.local_binder list ->
-  (Names.name Util.located * Topconstr.constr_expr) list
-val pr_binder_list :
-  (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
-val rewrite_rec_calls : 'a -> 'b -> 'b
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index d6c1772f..d182f7cd 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,3 +1,4 @@
+(* -*- default-directory: "~/research/coq/trunk/" -*- *)
 open Printf
 open Pp
 open Subtac_utils
@@ -12,12 +13,22 @@ open Decl_kinds
 open Util
 open Evd
 
-type obligation_info = (Names.identifier * Term.types * Intset.t) array
+let pperror cmd = Util.errorlabstrm "Subtac" cmd
+let error s = pperror (str s)
+
+exception NoObligations of identifier option
+
+let explain_no_obligations = function
+    Some ident -> str "No obligations for program " ++ str (string_of_id ident)
+  | None -> str "No obligations remaining"
+
+type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
 
 type obligation =
     { obl_name : identifier;
       obl_type : types;
       obl_body : constr option;
+      obl_opaque : bool;
       obl_deps : Intset.t;
     }
 
@@ -36,8 +47,9 @@ let assumption_message id =
   Options.if_verbose message ((string_of_id id) ^ " is assumed")
 
 let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
+let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
 
-let set_default_tactic t = default_tactic := t
+let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
 
 let evar_of_obligation o = { evar_hyps = Global.named_context_val () ;
 			     evar_concl = o.obl_type ; 
@@ -81,26 +93,35 @@ let map_first m =
     
 let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 
+let freeze () = !from_prg, !default_tactic_expr
+let unfreeze (v, t) = from_prg := v; set_default_tactic t
+let init () =
+  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" [])
+
 let _ = 
   Summary.declare_summary "program-tcc-table"
-    { Summary.freeze_function = (fun () -> !from_prg);
-      Summary.unfreeze_function =
-        (fun v -> from_prg := v);
-      Summary.init_function =
-        (fun () -> from_prg := ProgMap.empty);
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-open Evd
+let progmap_union = ProgMap.fold ProgMap.add
 
-let terms_of_evar ev = 
-  match ev.evar_body with
-      Evar_defined b ->
-	let nc = Environ.named_context_of_val ev.evar_hyps in
-	let body = Termops.it_mkNamedLambda_or_LetIn b nc in
-	let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in
-	  body, typ
-    | _ -> assert(false)
+let cache (_, (infos, tac)) =
+  from_prg := infos;
+  default_tactic_expr := tac
+
+let (input,output) = 
+  declare_object
+    { (default_object "Program state") with
+      cache_function = cache;
+      load_function = (fun _ -> cache);
+      open_function = (fun _ -> cache);
+      classify_function = (fun _ -> Dispose);
+      export_function = (fun x -> Some x) }
+    
+open Evd
 	  
 let rec intset_to = function
     -1 -> Intset.empty
@@ -113,7 +134,8 @@ let subst_body prg =
 let declare_definition prg =
   let body = subst_body prg in
     (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
-		  my_print_constr (Global.env()) body);
+		  my_print_constr (Global.env()) body ++ str " : " ++ 
+		  my_print_constr (Global.env()) prg.prg_type);
      with _ -> ());
   let ce = 
     { const_entry_body = body;
@@ -163,7 +185,7 @@ let declare_obligation obl body =
   let ce = 
     { const_entry_body = body;
       const_entry_type = Some obl.obl_type;
-      const_entry_opaque = false;
+      const_entry_opaque = obl.obl_opaque;
       const_entry_boxed = false} 
   in
   let constant = Declare.declare_constant obl.obl_name 
@@ -190,42 +212,53 @@ let red = Reductionops.nf_betaiota
 let init_prog_info n b t deps nvrec obls =
   let obls' = 
     Array.mapi
-      (fun i (n, t, d) ->
+      (fun i (n, t, o, d) ->
 	 debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
          { obl_name = n ; obl_body = None; 
-	   obl_type = red t; 
+	   obl_type = red t; obl_opaque = o;
 	   obl_deps = d })
       obls
   in
     { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_nvrec = nvrec; }
     
-let pperror cmd = Util.errorlabstrm "Subtac" cmd
-let error s = pperror (str s)
-
 let get_prog name =
   let prg_infos = !from_prg in
     match name with
 	Some n -> 
 	  (try ProgMap.find n prg_infos
-	   with Not_found -> error ("No obligations for program " ^ string_of_id n))
+	   with Not_found -> raise (NoObligations (Some n)))
       | None -> 
 	  (let n = map_cardinal prg_infos in
 	     match n with 
-		 0 -> error "No obligations remaining"
+		 0 -> raise (NoObligations None)
 	       | 1 -> map_first prg_infos
 	       | _ -> error "More than one program with unsolved obligations")
 
+let get_prog_err n = 
+  try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
+
 let obligations_solved prg = (snd prg.prg_obligations) = 0
 
+let update_state s = 
+(*   msgnl (str "Updating obligations info"); *)
+  Lib.add_anonymous_leaf (input s)
+
+let obligations_message rem = 
+  if rem > 0 then
+    if rem = 1 then
+      Options.if_verbose msgnl (int rem ++ str " obligation remaining")
+    else
+      Options.if_verbose msgnl (int rem ++ str " obligations remaining")
+  else
+    Options.if_verbose msgnl (str "No more obligations remaining")
+      
 let update_obls prg obls rem = 
   let prg' = { prg with prg_obligations = (obls, rem) } in
     from_prg := map_replace prg.prg_name prg' !from_prg;
-    if rem > 0 then (
-      Options.if_verbose msgnl (int rem ++ str " obligation(s) remaining");
-    )
+    obligations_message rem;
+    if rem > 0 then ()
     else (
-      Options.if_verbose msgnl (str "No more obligations remaining");
       match prg'.prg_deps with
 	  [] ->
 	    declare_definition prg';
@@ -235,7 +268,10 @@ let update_obls prg obls rem =
 	      if List.for_all (fun x -> obligations_solved x) progs then 
 		(declare_mutual_definition progs;
 		 from_prg := List.fold_left
-		   (fun acc x -> ProgMap.remove x.prg_name acc) !from_prg progs))
+		   (fun acc x -> 
+		     ProgMap.remove x.prg_name acc) !from_prg progs));
+    update_state (!from_prg, !default_tactic_expr);
+    rem
 	    
 let is_defined obls x = obls.(x).obl_body <> None
 
@@ -246,7 +282,24 @@ let deps_remaining obls deps =
 	 else x :: acc)
       deps []
 
-let solve_obligation prg num =
+let kind_of_opacity o =
+  if o then Subtac_utils.goal_proof_kind
+  else Subtac_utils.goal_kind
+   
+let obligations_of_evars evars =
+  let arr = 
+    Array.of_list
+      (List.map
+	 (fun (n, t) ->
+	    { obl_name = n;
+	      obl_type = t;
+	      obl_body = None;
+	      obl_opaque = false;
+	      obl_deps = Intset.empty;
+	    }) evars)
+  in arr, Array.length arr
+
+let rec solve_obligation prg num =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
   let obl = obls.(num) in
@@ -256,22 +309,23 @@ let solve_obligation prg num =
       match deps_remaining obls obl.obl_deps with
 	  [] ->
 	    let obl = subst_deps_obl obls obl in
-	      Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type
+	      Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type
 		(fun strength gr -> 
 		   debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");		   
 		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
 		   let obls = Array.copy obls in
 		   let _ = obls.(num) <- obl in
-		     update_obls prg obls (pred rem));
+		     if update_obls prg obls (pred rem) <> 0 then
+		       auto_solve_obligations (Some prg.prg_name));
 	      trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		       Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
 	      Pfedit.by !default_tactic
 	| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 			++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
 
-let subtac_obligation (user_num, name, typ) =
+and subtac_obligation (user_num, name, typ) =
   let num = pred user_num in
-  let prg = get_prog name in
+  let prg = get_prog_err name in
   let obls, rem = prg.prg_obligations in
     if num < Array.length obls then
       let obl = obls.(num) in
@@ -280,20 +334,8 @@ let subtac_obligation (user_num, name, typ) =
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
       
-      
-let obligations_of_evars evars =
-  let arr = 
-    Array.of_list
-      (List.map
-	 (fun (n, t) ->
-	    { obl_name = n;
-	      obl_type = t;
-	      obl_body = None;
-	      obl_deps = Intset.empty;
-	    }) evars)
-  in arr, Array.length arr
-
-let solve_obligation_by_tac prg obls i tac =
+   
+and solve_obligation_by_tac prg obls i tac =
   let obl = obls.(i) in
   match obl.obl_body with 
       Some _ -> false
@@ -302,13 +344,15 @@ let solve_obligation_by_tac prg obls i tac =
 	   if deps_remaining obls obl.obl_deps = [] then
 	     let obl = subst_deps_obl obls obl in
 	     let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
-	       obls.(i) <- { obl with obl_body = Some t };
+	       if obl.obl_opaque then 
+		 obls.(i) <- declare_obligation obl t
+	       else
+		 obls.(i) <- { obl with obl_body = Some t };
 	       true		 
 	   else false
 	 with _ -> false)  
 
-let solve_obligations n tac = 
-  let prg = get_prog n in
+and solve_prg_obligations prg tac = 
   let obls, rem = prg.prg_obligations in
   let rem = ref rem in
   let obls' = Array.copy obls in
@@ -320,6 +364,27 @@ let solve_obligations n tac =
   in
     update_obls prg obls' !rem
 
+and solve_obligations n tac = 
+  let prg = get_prog_err n in
+    solve_prg_obligations prg tac
+
+and solve_all_obligations tac = 
+  ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
+      
+and try_solve_obligation n prg tac = 
+  let prg = get_prog prg in 
+  let obls, rem = prg.prg_obligations in
+  let obls' = Array.copy obls in
+    if solve_obligation_by_tac prg obls' n tac then
+      ignore(update_obls prg obls' (pred rem));
+    
+and try_solve_obligations n tac = 
+  try ignore (solve_obligations n tac) with NoObligations _ -> ()
+
+and auto_solve_obligations n : unit =
+  Options.if_verbose msgnl (str "Solving obligations automatically...");
+  try_solve_obligations n !default_tactic
+      
 let add_definition n b t obls =
   Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n b t [] (Array.make 0 0) obls in
@@ -332,7 +397,7 @@ let add_definition n b t obls =
     let len = Array.length obls in
     let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
       from_prg := ProgMap.add n prg !from_prg; 
-      solve_obligations (Some n) !default_tactic)
+      auto_solve_obligations (Some n))
 	
 let add_mutual_definitions l nvrec =
   let deps = List.map (fun (n, b, t, obls) -> n) l in
@@ -343,22 +408,21 @@ let add_mutual_definitions l nvrec =
       !from_prg l
   in
     from_prg := upd;
-    List.iter (fun x -> solve_obligations (Some x) !default_tactic) deps
+    List.iter (fun x -> auto_solve_obligations (Some x)) deps
 
 let admit_obligations n =
-  let prg = get_prog n in
+  let prg = get_prog_err n in
   let obls, rem = prg.prg_obligations in
-  let obls' = 
-    Array.mapi (fun i x -> 
+    Array.iteri (fun i x -> 
 		 match x.obl_body with 
 		     None -> 
-			 let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
-			   assumption_message x.obl_name;
-			   { x with obl_body = Some (mkConst kn) }
-		   | Some _ -> x)
-      obls
-  in
-    update_obls prg obls' 0
+                       let x = subst_deps_obl obls x in
+		       let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
+			 assumption_message x.obl_name;
+			 obls.(i) <- { x with obl_body = Some (mkConst kn) }
+		   | Some _ -> ())
+      obls;
+    ignore(update_obls prg obls 0)
 
 exception Found of int
 
@@ -367,21 +431,17 @@ let array_find f arr =
     raise Not_found
   with Found i -> i
 
-let rec next_obligation n =
-  let prg = get_prog n in
+let next_obligation n =
+  let prg = get_prog_err n in
   let obls, rem = prg.prg_obligations in
   let i = 
     array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = [])
       obls
-  in
-    if solve_obligation_by_tac prg obls i !default_tactic then (
-      update_obls prg obls (pred rem);
-      next_obligation n
-    ) else solve_obligation prg i
+  in solve_obligation prg i
       
 open Pp
 let show_obligations n =
-  let prg = get_prog n in
+  let prg = get_prog_err n in
   let n = prg.prg_name in
   let obls, rem = prg.prg_obligations in
     msgnl (int rem ++ str " obligation(s) remaining: ");
@@ -392,3 +452,4 @@ let show_obligations n =
 		    | Some _ -> ())
       obls
 			
+let default_tactic () = !default_tactic
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 3981d4c6..f015b80b 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,8 +1,10 @@
 open Util
 
-type obligation_info = (Names.identifier * Term.types * Intset.t) array
+type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
+    (* ident, type, opaque or transparent, dependencies *)
 
-val set_default_tactic : Proof_type.tactic -> unit
+val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
+val default_tactic : unit -> Proof_type.tactic
 
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
   obligation_info -> unit
@@ -14,8 +16,20 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op
 
 val next_obligation : Names.identifier option -> unit
 
-val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
+val solve_obligations : Names.identifier option -> Proof_type.tactic -> int 
+(* Number of remaining obligations to be solved for this program *)
+
+val solve_all_obligations : Proof_type.tactic -> unit 
+
+val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -> unit
+
+val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
 
 val show_obligations : Names.identifier option -> unit
 
 val admit_obligations : Names.identifier option -> unit
+
+exception NoObligations of Names.identifier option
+
+val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds
+
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 4d1ac731..cce9a358 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Global
 open Pp
@@ -36,7 +36,6 @@ open Subtac_utils
 open Coqlib
 open Printer
 open Subtac_errors
-open Context
 open Eterm
 
 module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion)
@@ -89,18 +88,18 @@ let list_split_at index l =
 
 open Vernacexpr
 
-let coqintern evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
-let coqinterp evd env : Topconstr.constr_expr -> Term.constr = Constrintern.interp_constr (evars_of evd) env
+let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
+let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env
 
 let env_with_binders env isevars l =
   let rec aux ((env, rels) as acc) = function
       Topconstr.LocalRawDef ((loc, name), def) :: tl -> 
-	let rawdef = coqintern !isevars env def in
+	let rawdef = coqintern_constr !isevars env def in
 	let coqdef, deftyp = interp env isevars rawdef empty_tycon in
 	let reldecl = (name, Some coqdef, deftyp) in
 	  aux  (push_rel reldecl env, reldecl :: rels) tl
     | Topconstr.LocalRawAssum (bl, typ) :: tl ->
-	let rawtyp = coqintern !isevars env typ in
+	let rawtyp = coqintern_type !isevars env typ in
 	let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
 	let acc = 
 	  List.fold_left (fun (env, rels) (loc, name) -> 
@@ -113,36 +112,37 @@ let env_with_binders env isevars l =
   in aux (env, []) l
 
 let subtac_process env isevars id l c tycon =
-  let env_binders, binders_rel = env_with_binders env isevars l in
+  let c = Command.abstract_constr_expr c l in
+(*   let env_binders, binders_rel = env_with_binders env isevars l in *)
   let tycon = 
     match tycon with
 	None -> empty_tycon
       | Some t -> 
-	  let t = coqintern !isevars env_binders t in
-	  let coqt, ttyp = interp env_binders isevars t empty_tycon in
+	  let t = Command.generalize_constr_expr t l in
+	  let t = coqintern_type !isevars env t in
+	  let coqt, ttyp = interp env isevars t empty_tycon in
 	    mk_tycon coqt
   in    
-  let c = coqintern !isevars env_binders c in
-  let c = Subtac_utils.rewrite_cases env c in
-  let coqc, ctyp = interp env_binders isevars c tycon in
-(*   let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ *)
-(* 		 str "Coq type: " ++ my_print_constr env_binders ctyp) *)
-(*   with _ -> ()  *)
+  let c = coqintern_constr !isevars env c in
+  let coqc, ctyp = interp env isevars c tycon in
+(*   let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *)
+(* 		 str "Coq type: " ++ my_print_constr env ctyp) *)
+(*   with _ -> () *)
 (*   in *)
-(*   let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ()))  with _ -> () in *)
+(*   let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars))  with _ -> () in *)
     
-  let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel 
-  and fullctyp = it_mkProd_or_LetIn ctyp binders_rel
-  in
-  let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in
-  let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in
-
-(*   let _ = try trace (str "After evar normalization: " ++ spc () ++ *)
-(* 		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () *)
-(* 		 ++ str "Coq type: " ++ my_print_constr env fullctyp)  *)
-(*      with _ -> ()  *)
+(*   let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel  *)
+(*   and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *)
 (*   in *)
-  let evm = non_instanciated_map env isevars in
+  let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in
+  let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in
+(*   let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *)
+(*   let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *)
+(*   let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *)
+(* 		       Evd.pr_evar_map evm) *)
+(*   with _ -> () *)
+(*   in *)
+  let evm = non_instanciated_map env isevars (evars_of !isevars) in
 (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
     evm, fullcoqc, fullctyp
 
@@ -152,5 +152,5 @@ let subtac_proof env isevars id l c tycon =
   let nc = named_context env in
   let nc_len = named_context_length nc in
   let evm, coqc, coqt = subtac_process env isevars id l c tycon in
-  let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
+  let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in
     add_definition id def coqt evars
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 6244aef3..53eec0b6 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping_F.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
+(* $Id: subtac_pretyping_F.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pp
 open Util
@@ -93,7 +93,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
   (* coerce to tycon if any *)
   let inh_conv_coerce_to_tycon loc env isevars j = function
-    | None -> j
+    | None -> j_nf_isevar !isevars j
     | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t
 
   let push_rels vars env = List.fold_right push_rel vars env
@@ -364,21 +364,21 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	      error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
 	in
 	let cstrs = get_constructors env indf in
-	  if Array.length cstrs <> 1 then
-            user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
-	  let cs = cstrs.(0) in
-	    if List.length nal <> cs.cs_nargs then
-              user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
-	    let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
-              (List.rev nal) cs.cs_args in
-	    let env_f = push_rels fsign env in
-	      (* Make dependencies from arity signature impossible *)
-	    let arsgn =
-	      let arsgn,_ = get_arity env indf in
-		if not !allow_anonymous_refs then
-		  List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
-		else arsgn
-	    in
+	if Array.length cstrs <> 1 then
+          user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
+	let cs = cstrs.(0) in
+	  if List.length nal <> cs.cs_nargs then
+            user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
+	let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
+          (List.rev nal) cs.cs_args in
+	let env_f = push_rels fsign env in
+	  (* Make dependencies from arity signature impossible *)
+	let arsgn =
+	  let arsgn,_ = get_arity env indf in
+	    if not !allow_anonymous_refs then
+	      List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+	    else arsgn
+	in
 	    let psign = (na,None,build_dependent_inductive env indf)::arsgn in
 	    let nar = List.length arsgn in
 	      (match po with
@@ -495,13 +495,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
 	  tycon env (* loc *) (po,tml,eqns)
 
-    | RCast(loc,c,k,t) ->
+    | RCast(loc,c,k) ->
 	let cj =
 	  match k with
 	      CastCoerce ->
 		let cj = pretype empty_tycon env isevars lvar c in
 		  evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
-	    | CastConv k ->
+	    | CastConv (k,t) ->
 		let tj = pretype_type empty_valcon env isevars lvar t in
 		let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
 		  (* User Casts are for helping pretyping, experimentally not to be kept*)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 01dee3e9..28fe6352 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -32,6 +32,7 @@ let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
 let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub"
 let lt_ref = make_ref ["Init";"Peano"] "lt"
 let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
+let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
 
 let make_ref s = Qualid (dummy_loc, qualid_of_string s)
 let sig_ref = make_ref "Init.Specif.sig"
@@ -54,6 +55,10 @@ let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal")
 let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
 let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
 
+let not_ref = lazy (init_constant ["Init"; "Logic"] "not")
+
+let and_typ = lazy (Coqlib.build_coq_and ())
+
 let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep")
 let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
 let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
@@ -61,8 +66,7 @@ let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
 
 let jmeq_ind = lazy (init_constant ["Logic";"JMeq"] "JMeq")
 let jmeq_rec = lazy (init_constant ["Logic";"JMeq"] "JMeq_rec")
-let jmeq_ind_ref = lazy (init_reference ["Logic";"JMeq"] "JMeq")
-let jmeq_refl_ref = lazy (init_reference ["Logic";"JMeq"] "JMeq_refl")
+let jmeq_refl = lazy (init_constant ["Logic";"JMeq"] "JMeq_refl")
 
 let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
 let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
@@ -126,6 +130,10 @@ let trace s =
     else ()
   else ()
 
+let rec pp_list f = function
+    [] -> mt()
+  | x :: y -> f x ++ spc () ++ pp_list f y
+
 let wf_relations = Hashtbl.create 10
 
 let std_relations () = 
@@ -145,8 +153,8 @@ let app_opt c e =
 let print_args env args = 
   Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
 
-let make_existential loc env isevars c =
-  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in
+let make_existential loc ?(opaque = true) env isevars c =
+  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
   let (key, args) = destEvar evar in
     (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
 		  print_args env args ++ str " for type: "++ 
@@ -162,25 +170,33 @@ let make_existential_expr loc env c =
 let string_of_hole_kind = function
   | ImplicitArg _ -> "ImplicitArg"
   | BinderType _ -> "BinderType"
-  | QuestionMark -> "QuestionMark"
+  | QuestionMark _ -> "QuestionMark"
   | CasesType -> "CasesType"
   | InternalHole -> "InternalHole"
   | TomatchTypeParameter _ -> "TomatchTypeParameter"
-      
-let non_instanciated_map env evd =
-  let evm = evars_of !evd in
-    List.fold_left 
-      (fun evm (key, evi) -> 
-	 let (loc,k) = evar_source key !evd in
-	   debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
-		      str (string_of_hole_kind k));
-	   match k with 
-	       QuestionMark -> Evd.add evm key evi
-	     | _ ->
+
+let evars_of_term evc init c = 
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n)
+    | Evar (n, _) -> assert(false)
+    | _ -> fold_constr evrec acc c
+  in 
+    evrec init c
+
+let non_instanciated_map env evd evm =
+  List.fold_left 
+    (fun evm (key, evi) -> 
+       let (loc,k) = evar_source key !evd in
+	 debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
+		    str (string_of_hole_kind k));
+	 match k with 
+	     QuestionMark _ -> Evd.add evm key evi
+	   | _ ->
 	       debug 2 (str " and is an implicit");
 	       Pretype_errors.error_unsolvable_implicit loc env evm k)
-      Evd.empty (Evarutil.non_instantiated evm)
-
+    Evd.empty (Evarutil.non_instantiated evm)
+    
 let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
 let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
 
@@ -247,11 +263,30 @@ let mk_ex_pi1 a b c =
 let mk_ex_pi2 a b c =
   mkApp (Lazy.force ex_pi2, [| a; b; c |])
     
-
 let mkSubset name typ prop = 
   mkApp ((Lazy.force sig_).typ,
 	 [| typ; mkLambda (name, typ, prop) |])
 
+let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |])
+
+let unsafe_fold_right f = function
+    hd :: tl -> List.fold_right f tl hd
+  | [] -> raise (Invalid_argument "unsafe_fold_right")
+
+let mk_conj l =
+  let conj_typ = Lazy.force and_typ in
+    unsafe_fold_right
+      (fun c conj ->
+	 mkApp (conj_typ, [| c ; conj |]))
+      l
+
+let mk_not c =
+  let notc = Lazy.force not_ref in
+    mkApp (notc, [| c |])
+
 let and_tac l hook =
   let andc = Coqlib.build_coq_and () in      
   let rec aux ((accid, goal, tac, extract) as acc) = function
@@ -301,291 +336,7 @@ let destruct_ex ext ex =
   in aux ex ext
 
 open Rawterm
-
-let rec concatMap f l = 
-  match l with
-      hd :: tl -> f hd @ concatMap f tl      
-    | [] -> []
 	
-let list_mapi f = 
-  let rec aux i = function 
-      hd :: tl -> f i hd :: aux (succ i) tl 
-    | [] -> []
-  in aux 0
-
-(*
-let make_discr (loc, po, tml, eqns) =
-  let mkHole = RHole (dummy_loc, InternalHole) in
-  
-  let rec vars_of_pat = function
-      RPatVar (loc, n) -> (match n with Anonymous -> [] | Name n -> [n])
-    | RPatCstr (loc, csrt, pats, _) -> 
-	concatMap vars_of_pat pats
-  in
-  let rec constr_of_pat l = function 
-      RPatVar (loc, n) -> 
-	(match n with 
-	     Anonymous -> 
-	       let n = next_name_away_from "x" l in
-		 RVar n, (n :: l)
-	   | Name n -> RVar n, l)
-    | RPatCstr (loc, csrt, pats, _) -> 
-	let (args, vars) =
-	  List.fold_left
-	    (fun (args, vars) x ->
-	       let c, vars = constr_of_pat vars x in
-		 c :: args, vars)
-	    ([], l) pats
-	in		 
-	  RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars
-  in
-  let rec constr_of_pat l = function 
-      RPatVar (loc, n) -> 
-	(match n with 
-	     Anonymous -> 
-	       let n = next_name_away_from "x" l in
-		 RVar n, (n :: l)
-	   | Name n -> RVar n, l)
-    | RPatCstr (loc, csrt, pats, _) -> 
-	let (args, vars) =
-	  List.fold_left
-	    (fun (args, vars) x ->
-	       let c, vars = constr_of_pat vars x in
-		 c :: args, vars)
-	    ([], l) pats
-	in		 
-	  RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars
-  in
-  let constrs_of_pats v l =
-    List.fold_left 
-      (fun (v, acc) x -> 
-	 let x', v' = constr_of_pat v x in
-	   (l', v' :: acc))
-      (v, []) l
-  in
-  let rec pat_of_pat l = function
-      RPatVar (loc, n) -> 
-	let n', l = match n with
-	    Anonymous -> 
-	      let n = next_name_away_from "x" l in
-		n, n :: l
-	  | Name n -> n, n :: l 
-	in
-	  RPatVar (loc, Name n'), l
-    | RPatCstr (loc, cstr, pats, (loc, alias)) ->
-	let args, vars, s = 
-	  List.fold_left (fun (args, vars) x -> 
-			    let pat', vars = pat_of_pat vars pat in
-			      pat' :: args, vars)
-	    ([], alias :: l) pats
-	in RPatCstr (loc, cstr, args, (loc, alias)), vars
-  in
-  let pats_of_pats l =
-    List.fold_left 
-      (fun (v, acc) x -> 
-	 let x', v' = pat_of_pat v x in
-	   (v', x' :: acc))
-      ([], []) l
-  in
-  let eq_of_pat p used c = 
-    let constr, vars' = constr_of_pat used p in
-    let eq = RApp (dummy_loc, RRef (dummy_loc, Lazy.force eqind_ref), [mkHole; constr; c]) in
-      vars', eq
-  in
-  let eqs_of_pats ps used cstrs =
-    List.fold_left2 
-      (fun (vars, eqs) pat c ->
-	 let (vars', eq) = eq_of_pat pat c in
-	   match eqs with 
-	       None -> Some eq 
-	     | Some eqs ->
-		 Some (RApp (dummy_loc, RRef (dummy_loc, Lazy.force and_ref), [eq, eqs])))
-      (used, None) ps cstrs
-  in
-  let quantify c l =
-    List.fold_left
-      (fun acc name -> RProd (dummy_loc, name, mkHole, acc))
-      c l
-  in
-  let quantpats = 
-    List.fold_left
-      (fun (acc, pats) ((loc, idl, cpl, c) as x) ->
-	 let vars, cpl = pats_of_pats cpl in
-	 let l', constrs = constrs_of_pats vars cpl in	   
-	 let discrs = 
-	   List.map (fun (_, _, cpl', _) -> 
-		       let qvars, eqs = eqs_of_pats cpl' l' constrs in
-		       let neg = RApp (dummy_loc, RRef (dummy_loc, Lazy.force not_ref), [out_some eqs]) in
-		       let pat_ineq = quantify qvars neg in
-			 
-		    )
-	     pats in
-	   
-			 
-
-
-	   
-	   
-
-	   (x, pat_ineq))
-  in
-    List.fold_left 
-      (fun acc ((loc, idl, cpl, c0) pat) -> 
-    
-		
-		let c' = 
-		  List.fold_left 
-		    (fun acc (n, t) ->
-		       RLambda (dummy_loc, n, mkHole, acc))
-		    c eqs_types
-		in (loc, idl, cpl, c'))
-      eqns
-  i
-*)
-(* let rewrite_cases_aux (loc, po, tml, eqns) = *)
-(*   let tml = list_mapi (fun i (c, (n, opt)) -> c,  *)
-(* 		       ((match n with *)
-(* 			    Name id -> (match c with *)
-(* 					  | RVar (_, id') when id = id' -> *)
-(* 					      Name (id_of_string (string_of_id id ^ "'")) *)
-(* 					  | _ -> n) *)
-(* 			  | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))), *)
-(* 			opt)) tml  *)
-(*   in *)
-(*   let mkHole = RHole (dummy_loc, InternalHole) in *)
-(*   (\* let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)), *\) *)
-(* (\* 		       [mkHole; c; n]) *\) *)
-(* (\*   in *\) *)
-(*   let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqdep_ind_ref)), *)
-(* 		       [mkHole; c; mkHole; n]) *)
-(*   in *)
-(*   let eqs_types =  *)
-(*     List.map *)
-(*       (fun (c, (n, _)) -> *)
-(* 	 let id = match n with Name id -> id | _ -> assert false in *)
-(* 	 let heqid = id_of_string ("Heq" ^ string_of_id id) in *)
-(* 	   Name heqid, mkeq c (RVar (dummy_loc, id))) *)
-(*       tml *)
-(*   in *)
-(*   let po =  *)
-(*     List.fold_right *)
-(*       (fun (n,t) acc -> *)
-(* 	 RProd (dummy_loc, Anonymous, t, acc)) *)
-(*       eqs_types (match po with  *)
-(* 		     Some e -> e *)
-(* 		   | None -> mkHole) *)
-(*   in *)
-(*   let eqns =    *)
-(*     List.map (fun (loc, idl, cpl, c) -> *)
-(* 		let c' =  *)
-(* 		  List.fold_left  *)
-(* 		    (fun acc (n, t) -> *)
-(* 		       RLambda (dummy_loc, n, mkHole, acc)) *)
-(* 		    c eqs_types *)
-(* 		in (loc, idl, cpl, c')) *)
-(*       eqns *)
-(*   in *)
-(*   let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), *)
-(* 			      [mkHole; c]) *)
-(*   in *)
-(*   (\*let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), *)
-(* 			      [mkHole; c]) *)
-(*   in*\) *)
-(*   let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in *)
-(*   let case = RCases (loc,Some po,tml,eqns) in *)
-(*   let app = RApp (dummy_loc, case, refls) in *)
-(*     app *)
-
-(* let rec rewrite_cases c =  *)
-(*   match c with  *)
-(*       RCases _ -> let c' = map_rawconstr rewrite_cases c in *)
-(* 	(match c' with  *)
-(* 	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w) *)
-(* 	   | _ -> assert(false)) *)
-(*     | _ -> map_rawconstr rewrite_cases c *)
-	  
-(* let rewrite_cases env c = *)
-(*   let c' = rewrite_cases c in *)
-(*   let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in *)
-(*     c' *)
-
-let list_mapi f = 
-  let rec aux i = function 
-      hd :: tl -> f i hd :: aux (succ i) tl 
-    | [] -> []
-  in aux 0
-
-open Rawterm
-
-let rewrite_cases_aux (loc, po, tml, eqns) =
-  let tml' = list_mapi (fun i (c, (n, opt)) -> c, 
-		       ((match n with
-			    Name id -> (match c with
-					  | RVar (_, id') when id = id' ->
-					      id, (id_of_string (string_of_id id ^ "Heq_id"))
-					  | RVar (_, id') ->
-					      id', id
-					  | _ -> id_of_string (string_of_id id ^ "Heq_id"), id)
-			   | Anonymous -> 
-			       let str = "Heq_id" ^ string_of_int i in
-				 id_of_string str, id_of_string (str ^ "'")),
-			opt)) tml 
-  in
-  let mkHole = RHole (dummy_loc, InternalHole) in
-  let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in
-  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eq_ind_ref)),
-		       [mkHole; c; n])
-  in
-  let eqs_types = 
-    List.map
-      (fun (c, ((id, id'), _)) ->
-	 let heqid = id_of_string ("Heq" ^ string_of_id id) in
-	   Name heqid, mkeq (RVar (dummy_loc, id')) c)
-      tml'
-  in
-  let po = 
-    List.fold_right
-      (fun (n,t) acc ->
-	 RProd (dummy_loc, Anonymous, t, acc))
-      eqs_types (match po with 
-		     Some e -> e
-		   | None -> mkHole)
-  in
-  let eqns =   
-    List.map (fun (loc, idl, cpl, c) ->
-		let c' = 
-		  List.fold_left 
-		    (fun acc (n, t) ->
-		       RLambda (dummy_loc, n, mkHole, acc))
-		    c eqs_types
-		in (loc, idl, cpl, c'))
-      eqns
-  in
-  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
-			      [mkHole; c])
-  in
-  let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in
-  let tml'' = List.map (fun (c, ((id, id'), opt)) -> c, (Name id', opt)) tml' in
-  let case = RCases (loc,Some po,tml'',eqns) in
-  let app = RApp (dummy_loc, case, refls) in
-(*   let letapp = List.fold_left (fun acc (c, ((id, id'), opt)) -> RLetIn (dummy_loc, Name id, c, acc)) *)
-(* 		 app tml' *)
-(*   in *)
-    app
-
-let rec rewrite_cases c = 
-  match c with 
-      RCases _ -> let c' = map_rawconstr rewrite_cases c in
-	(match c' with 
-	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
-	   | _ -> assert(false))
-    | _ -> map_rawconstr rewrite_cases c
-	  
-let rewrite_cases env c = c
-(*   let c' = rewrite_cases c in *)
-(*   let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in *)
-(*     c' *)
-
 let id_of_name = function
     Name n -> n
   | Anonymous -> raise (Invalid_argument "id_of_name")
@@ -601,23 +352,6 @@ let recursive_message v =
 		    spc () ++ str "are recursively defined")
 
 (* Solve an obligation using tactics, return the corresponding proof term *)
-(*
-let solve_by_tac ev t =
-  debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info ev);
-  let goal = Proof_trees.mk_goal ev.evar_hyps ev.evar_concl None in
-  debug 1 (str "Goal created");
-  let ts = Tacmach.mk_pftreestate goal in
-  debug 1 (str "Got pftreestate");
-  let solved_state = Tacmach.solve_pftreestate t ts in
-  debug 1 (str "Solved goal");
-    let _, l = Tacmach.extract_open_pftreestate solved_state in
-      List.iter (fun (_, x) -> debug 1 (str "left hole of type " ++ my_print_constr (Global.env()) x)) l;
-    let c = Tacmach.extract_pftreestate solved_state in
-    debug 1 (str "Extracted term");
-    debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c);
-    c
-    *)
-
 let solve_by_tac evi t =
   debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
   let id = id_of_string "H" in
@@ -705,3 +439,12 @@ let pr_evar_defs evd =
     if meta_list evd = [] then mt() else
       str"METAS:"++brk(0,1)++pr_meta_map evd in
   v 0 (pp_evm ++ pp_met)
+
+let subtac_utils_path =
+  make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"])
+let utils_tac s =
+  lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s))
+
+let utils_call tac args =
+  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
+
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 482640f9..5a5dd427 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -27,6 +27,7 @@ val fix_sub_ref : global_reference lazy_t
 val fix_measure_sub_ref : global_reference lazy_t
 val lt_ref : global_reference lazy_t
 val lt_wf_ref : global_reference lazy_t
+val refl_ref : global_reference lazy_t
 val sig_ref : reference
 val proj1_sig_ref : reference
 val proj2_sig_ref : reference
@@ -37,13 +38,16 @@ val eq_ind : constr lazy_t
 val eq_rec : constr lazy_t
 val eq_rect : constr lazy_t
 val eq_refl : constr lazy_t
-val eq_ind_ref : global_reference lazy_t
-val refl_equal_ref : global_reference lazy_t
+
+val not_ref : constr lazy_t
+val and_typ : constr lazy_t
 
 val eqdep_ind : constr lazy_t
 val eqdep_rec : constr lazy_t
-val eqdep_ind_ref : global_reference lazy_t
-val eqdep_intro_ref : global_reference lazy_t
+
+val jmeq_ind : constr lazy_t
+val jmeq_rec : constr lazy_t
+val jmeq_refl : constr lazy_t
 
 val boolind : constr lazy_t
 val sumboolind : constr lazy_t
@@ -79,10 +83,11 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t
 type binders = local_binder list
 val app_opt : ('a -> 'a) option -> 'a -> 'a
 val print_args : env -> constr array -> std_ppcmds
-val make_existential : loc -> env -> evar_defs ref -> types -> constr
+val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr
 val make_existential_expr : loc -> 'a -> 'b -> constr_expr
 val string_of_hole_kind : hole_kind -> string
-val non_instanciated_map : env -> evar_defs ref -> evar_map
+val evars_of_term : evar_map -> evar_map -> constr -> evar_map
+val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map
 val global_kind : logical_kind
 val goal_kind : locality_flag * goal_object_kind
 val global_proof_kind : logical_kind
@@ -95,6 +100,12 @@ val mkProj1 : constr -> constr -> constr -> constr
 val mkProj1 : constr -> constr -> constr -> constr
 val mk_ex_pi1 : constr -> constr -> constr -> constr
 val mk_ex_pi1 : constr -> constr -> constr -> constr
+val mk_eq : types -> constr -> constr -> types
+val mk_eq_refl : types -> constr -> constr
+val mk_JMeq : types -> constr-> types -> constr -> types
+val mk_JMeq_refl : types -> constr -> constr
+val mk_conj : types list -> types
+val mk_not : types -> types
 
 val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types
 val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->  
@@ -102,7 +113,6 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
 
 val destruct_ex : constr -> constr -> constr list
 
-val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
 val id_of_name : name -> identifier
 
 val definition_message : identifier -> unit
@@ -114,3 +124,7 @@ val string_of_list : string -> ('a -> string) -> 'a list -> string
 val string_of_intset : Intset.t -> string
 
 val pr_evar_defs : evar_defs -> Pp.std_ppcmds
+
+val utils_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr
+
+val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds
diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v
index 7ab720f6..97cef9a5 100644
--- a/contrib/subtac/test/ListDep.v
+++ b/contrib/subtac/test/ListDep.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import List.
 Require Import Coq.subtac.Utils.
 
@@ -21,63 +22,25 @@ Section Map_DependentRecursor.
   Variable l : list U.
   Variable f : { x : U | In x l } -> V.
 
+  Obligations Tactic := unfold sub_list in * ; 
+    subtac_simpl ; intuition.
+
   Program Fixpoint map_rec ( l' : list U | sub_list l' l )
-    { measure l' length } : { r : list V | length r = length l' } :=
+    { measure length l' } : { r : list V | length r = length l' } :=
     match l' with
     nil => nil
     | cons x tl => let tl' := map_rec tl in
 	f x :: tl'
     end.
     
-    Obligation 1.
-    intros.
-    destruct tl' ; simpl ; simpl in e.
-    subst x0 tl0.
-    rewrite <- Heql'.
-    rewrite e.
-    auto.
-    Qed.
-
-    Obligation 2.
-    simpl.
-    intros.
-    destruct l'.
-    simpl in Heql'.
-    destruct x0 ; simpl ; try discriminate.
-    inversion Heql'.
-    inversion s.
-    apply H.
-    auto with datatypes.
-    Qed.
-
-
-    Obligation 3 of map_rec.
-    simpl.
-    intros.
-    rewrite <- Heql'.
+  Next Obligation.
+    destruct_call map_rec.
+    simpl in *.
+    subst l'.
     simpl ; auto with arith.
-    Qed.
-
-    Obligation 4.
-    simpl.
-    intros.
-    destruct l'.
-    simpl in Heql'.
-    destruct x0 ; simpl ; try discriminate.
-    inversion Heql'.
-    subst x tl.
-    apply sub_list_tl with u ; auto.
-    Qed.
-  
-    Obligation 5.
-    intros.
-    rewrite <- Heql' ; auto.
-    Qed.
-    
-    Program Definition map : list V := map_rec l.
-    Obligation 1.
-      split ; auto.
-    Qed.
+  Qed.
+      
+  Program Definition map : list V := map_rec l.
     
 End Map_DependentRecursor.
 
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index b8d13fe6..3ceea173 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -70,7 +70,22 @@ Section Nth.
 
   Next Obligation.
   Proof.
-    inversion l0.
+    intros.
+    inversion H.
   Defined.
+
+  Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := 
+    match l, n with
+      | hd :: _, 0 => hd
+      | _ :: tl, S n' => nth' tl n'
+      | nil, _ => !
+    end.
+
+  Next Obligation.
+  Proof.
+    intros.
+    inversion H.
+  Defined.
+
 End Nth.
 
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index ff07c3c4..8a5967a2 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -22,8 +22,13 @@ let get_module_path_of_section_path path =
    List.filter
     (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules
   with
-     [modul] -> modul
-   | _ -> raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther
+     [] -> 
+       Pp.warning ("Modules not supported: reference to "^
+         Libnames.string_of_path path^" will be wrong");
+       dirpath
+   | [modul] -> modul
+   | _ -> 
+       raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther
 ;;
 
 (*CSC: Problem: here we are using the wrong (???) hypothesis that there do *)
@@ -652,11 +657,13 @@ print_endline "PASSATO" ; flush stdout ;
                          A.ALambdas (new_passed_lambdas, t')
                  )
            | T.LetIn (n,s,t,d) ->
-              let n' =
+              let id =
                match n with
-                  N.Anonymous -> N.Anonymous
-                | _ ->
-                  N.Name (Nameops.next_name_away n (Termops.ids_of_context env))
+                   N.Anonymous -> N.id_of_string "_X"
+                 | N.Name id -> id
+              in
+              let n' =
+               N.Name (Nameops.next_ident_away id (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                let sourcesort =
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index c7d3b4ff..cce78891 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -26,31 +26,13 @@ let cprop =
    (N.mk_label "CProp")
 ;;
 
-let whd_betadeltaiotacprop env evar_map ty =
+let whd_betadeltaiotacprop env _evar_map ty =
  let module R = Rawterm in
-  let red_exp =
-   R.Hnf  (*** Instead CProp is made Opaque ***)
-(*
-   R.Cbv
-    {R.rBeta = true ; R.rIota = true ; R.rDelta = true; R.rZeta=true ;
-     R.rConst = [Names.EvalConstRef cprop]
-    }
-*)
-  in
-Conv_oracle.set_opaque_const cprop;
-prerr_endline "###whd_betadeltaiotacprop:" ;
-let xxx =
-(*Pp.msgerr (Printer.pr_lconstr_env env ty);*)
-prerr_endline "";
-   (fst (Redexpr.reduction_of_red_expr red_exp)) env evar_map ty
-in
-prerr_endline "###FINE" ;
-(*
-Pp.msgerr (Printer.pr_lconstr_env env xxx);
-*)
-prerr_endline "";
-Conv_oracle.set_transparent_const cprop;
-xxx
+ let module C = Closure in
+ let module CR = C.RedFlags in
+ (*** CProp is made Opaque ***)
+ let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in
+ C.whd_val (C.create_clos_infos flags env) (C.inject ty)
 ;;
 
 
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index f286d2c8..01271323 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -461,11 +461,42 @@ let kind_of_constant kn =
   match Declare.constant_kind (Nametab.sp_of_global(Libnames.ConstRef kn)) with
     | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
     | DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
-    | DK.IsAssumption DK.Conjectural -> "AXIOM","Conjecture"
+    | DK.IsAssumption DK.Conjectural ->
+        Pp.warning "Conjecture not supported in dtd (used Declaration instead)";
+        "AXIOM","Declaration"
     | DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
-    | DK.IsDefinition DK.Example -> "DEFINITION","Example"
-    | DK.IsDefinition _ -> Util.anomaly "Unsupported constant kind"
-    | DK.IsProof thm -> "THEOREM",DK.string_of_theorem_kind thm
+    | DK.IsDefinition DK.Example -> 
+        Pp.warning "Example not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.Coercion ->
+        Pp.warning "Coercion not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.SubClass ->
+        Pp.warning "SubClass not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.CanonicalStructure ->
+        Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.Fixpoint ->
+        Pp.warning "Fixpoint not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.CoFixpoint ->
+        Pp.warning "CoFixpoint not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.Scheme ->
+        Pp.warning "Scheme not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.StructureComponent ->
+        Pp.warning "StructureComponent not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsDefinition DK.IdentityCoercion ->
+        Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition"
+    | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
+        "THEOREM",DK.string_of_theorem_kind thm
+    | DK.IsProof _ ->
+        Pp.warning "Unsupported theorem kind (used Theorem instead)";
+        "THEOREM",DK.string_of_theorem_kind DK.Theorem
 ;;
 
 let kind_of_global r =