- module Redinfo dans library/ pour les constantes d'élimination

 - module Tacred : fonctions de reductions utilisees dans les tactiques


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

14 files changed, 1093 insertions, 166 deletions

diff --git a/.depend b/.depend
index b65a8a206a..479b721edc 100644
--- a/.depend
+++ b/.depend
@@ -40,6 +40,7 @@ library/impargs.cmi: kernel/names.cmi
 library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi 
 library/libobject.cmi: kernel/names.cmi 
 library/nametab.cmi: kernel/names.cmi 
+library/redinfo.cmi: kernel/names.cmi kernel/term.cmi 
 library/summary.cmi: kernel/names.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/pcoq.cmi lib/pp.cmi 
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
@@ -230,6 +231,12 @@ library/library.cmx: kernel/environ.cmx library/global.cmx library/lib.cmx \
     library/library.cmi 
 library/nametab.cmo: kernel/names.cmi library/summary.cmi library/nametab.cmi 
 library/nametab.cmx: kernel/names.cmx library/summary.cmx library/nametab.cmi 
+library/redinfo.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \
+    library/global.cmi kernel/names.cmi kernel/reduction.cmi \
+    library/summary.cmi kernel/term.cmi lib/util.cmi library/redinfo.cmi 
+library/redinfo.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \
+    library/global.cmx kernel/names.cmx kernel/reduction.cmx \
+    library/summary.cmx kernel/term.cmx lib/util.cmx library/redinfo.cmi 
 library/states.cmo: library/lib.cmi library/summary.cmi lib/system.cmi \
     library/states.cmi 
 library/states.cmx: library/lib.cmx library/summary.cmx lib/system.cmx \
@@ -246,12 +253,18 @@ parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
 parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi 
+parsing/termast.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \
+    kernel/generic.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    lib/pp.cmi kernel/term.cmi lib/util.cmi parsing/termast.cmi 
+parsing/termast.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/environ.cmx \
+    kernel/generic.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    lib/pp.cmx kernel/term.cmx lib/util.cmx parsing/termast.cmi 
 proofs/clenv.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
-    kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \
+    kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \
     proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
     proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/clenv.cmi 
 proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
-    kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \
+    kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx lib/util.cmx proofs/clenv.cmi 
 proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
@@ -298,8 +311,14 @@ proofs/tacmach.cmx: parsing/ast.cmx kernel/environ.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \
     kernel/sign.cmx lib/stamps.cmx proofs/tacred.cmx kernel/term.cmx \
     proofs/typing_ev.cmx lib/util.cmx proofs/tacmach.cmi 
-proofs/tacred.cmo: proofs/tacred.cmi 
-proofs/tacred.cmx: proofs/tacred.cmi 
+proofs/tacred.cmo: kernel/closure.cmi library/declare.cmi kernel/environ.cmi \
+    kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \
+    kernel/names.cmi lib/pp.cmi library/redinfo.cmi kernel/reduction.cmi \
+    kernel/term.cmi lib/util.cmi proofs/tacred.cmi 
+proofs/tacred.cmx: kernel/closure.cmx library/declare.cmx kernel/environ.cmx \
+    kernel/generic.cmx kernel/inductive.cmx kernel/instantiate.cmx \
+    kernel/names.cmx lib/pp.cmx library/redinfo.cmx kernel/reduction.cmx \
+    kernel/term.cmx lib/util.cmx proofs/tacred.cmi 
 proofs/typing_ev.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
     kernel/typeops.cmi lib/util.cmi proofs/typing_ev.cmi 
diff --git a/Makefile b/Makefile
index beef20f270..801dc63e63 100644
--- a/Makefile
+++ b/Makefile
@@ -45,15 +45,17 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
 
 LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
 	library/global.cmo library/states.cmo library/library.cmo \
-	library/nametab.cmo library/impargs.cmo library/declare.cmo
+	library/nametab.cmo library/impargs.cmo library/redinfo.cmo \
+        library/declare.cmo
+
+PROOFS=proofs/typing_ev.cmo proofs/tacred.cmo \
+       proofs/proof_trees.cmo proofs/logic.cmo \
+       proofs/refiner.cmo proofs/evar_refiner.cmo proofs/clenv.cmo
 
 PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
 	parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \
 	parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo
 
-PROOFS=proofs/typing_ev.cmo proofs/proof_trees.cmo proofs/logic.cmo \
-       proofs/refiner.cmo proofs/evar_refiner.cmo proofs/clenv.cmo
-
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernac.cmo \
 	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7119729c7d..93243a4404 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -508,10 +508,9 @@ type 'a miota_args = {
   mcargs  : 'a list;    (* the constructor's arguments *)
   mlf     : 'a array }  (* the branch code vector *)
 		       
-let reducible_mind_case c =
-  match c with 
-    | DOPN(MutConstruct _,_) | DOPN(CoFix _,_) -> true
-    | _  -> false
+let reducible_mind_case = function
+  | DOPN(MutConstruct _,_) | DOPN(CoFix _,_) -> true
+  | _  -> false
 
 let contract_cofix = function
   | DOPN(CoFix(bodynum),bodyvect) ->
@@ -536,10 +535,8 @@ let reduce_mind_case env mia =
     | _ -> assert false
 
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
+   Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
-   Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})]
-
- *)
 let contract_fix = function 
   | DOPN(Fix(recindices,bodynum),bodyvect) -> 
       let nbodies = Array.length recindices in
@@ -552,9 +549,12 @@ let fix_recarg fix stack =
     | DOPN(Fix(recindices,bodynum),_) ->
     	if 0 <= bodynum & bodynum < Array.length recindices then
 	  let recargnum = Array.get recindices bodynum in
-          (try Some(recargnum, List.nth stack recargnum)
-           with Failure "nth" | Invalid_argument "List.nth" -> None)
-    	else None
+          (try 
+	     Some (recargnum, List.nth stack recargnum)
+           with Failure "nth" | Invalid_argument "List.nth" -> 
+	     None)
+    	else 
+	  None
     | _ -> assert false
 
 let reduce_fix whfun fix stack =
@@ -1029,79 +1029,6 @@ let decomp_n_prod env sigma n =
   in 
   decrec n []
 
-(* Special iota reduction... *)
-
-let contract_cofix_use_function f cofix =
-  match cofix with 
-    | DOPN(CoFix(bodynum),bodyvect) ->
-  	let nbodies =  (Array.length bodyvect) -1 in
-  	let make_Fi j = DOPN(CoFix(j),bodyvect) in
-  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
-  	sAPPViList bodynum (array_last bodyvect) lbodies
-    | _ -> assert false
-
-let reduce_mind_case_use_function env f mia =
-  match mia.mconstr with 
-    | DOPN(MutConstruct((indsp,tyindx),i),_) ->
-	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
-	let nparams = mind_nparams env ind in
-	let real_cargs = snd(list_chop nparams mia.mcargs) in
-	applist (mia.mlf.(i-1),real_cargs)
-    | DOPN(CoFix _,_) as cofix ->
-	let cofix_def = contract_cofix_use_function f cofix in
-	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
-    | _ -> assert false
-	  
-let special_red_case env whfun p c ci lf  =
-  let rec redrec c l = 
-    let (constr,cargs) = whfun c l in 
-    match constr with 
-      | DOPN(Const _,_) as g -> 
-          if evaluable_constant env g then
-            let gvalue = constant_value env g in
-            if reducible_mind_case  gvalue then
-              reduce_mind_case_use_function env g
-                {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
-            else 
-	      redrec gvalue cargs
-          else 
-	    raise Redelimination
-      | _ ->
-          if reducible_mind_case constr then
-            reduce_mind_case env
-              {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf}
-          else 
-	    raise Redelimination
-  in 
-  redrec c []
-
-
-(* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make 
-the reduction using this extra information *)
-
-let contract_fix_use_function f fix =
-  match fix with 
-    | DOPN(Fix(recindices,bodynum),bodyvect) ->
-  	let nbodies = Array.length recindices in
-  	let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in
-  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
-	  sAPPViList bodynum (array_last bodyvect) lbodies
-    | _ -> assert false
-
-
-let reduce_fix_use_function f whfun fix stack =
-  match fix with 
-    | DOPN (Fix(recindices,bodynum),bodyvect) ->
-	(match fix_recarg fix stack with
-           | None -> (false,(fix,stack))
-	   | Some (recargnum,recarg) ->
-               let (recarg'hd,_ as recarg')= whfun recarg [] in
-               let stack' = list_assign stack recargnum (applist recarg') in
-	       (match recarg'hd with
-                  | DOPN(MutConstruct _,_) ->
-		      (true,(contract_fix_use_function f fix,stack'))
-		  | _ -> (false,(fix,stack'))))
-    | _ -> assert false
 
 
 (* Check that c is an "elimination constant"
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 421aa9aaf2..585a573449 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -25,11 +25,14 @@ type 'a stack_reduction_function =
 val whd_stack : 'a stack_reduction_function
 
 (*s Reduction Function Operators *)
+
 val under_casts : 'a reduction_function -> 'a reduction_function
 val strong : 'a reduction_function -> 'a reduction_function
 val strong_prodspine : 'a reduction_function -> 'a reduction_function
 val stack_reduction_of_reduction : 
   'a reduction_function -> 'a stack_reduction_function
+val stacklam : (constr -> constr list -> 'a) -> constr list -> constr 
+  -> constr list -> 'a 
 
 (*s Generic Optimized Reduction Functions using Closures *)
 
@@ -57,6 +60,7 @@ val whd_betadeltaiota_stack : 'a stack_reduction_function
 
 
 (*s Head normal forms *)
+
 val whd_const_stack : section_path list -> 'a stack_reduction_function
 val whd_const : section_path list -> 'a reduction_function
 val whd_delta_stack : 'a stack_reduction_function
@@ -67,12 +71,13 @@ val whd_betadeltat_stack : 'a stack_reduction_function
 val whd_betadeltat : 'a reduction_function
 val whd_betadeltatiota_stack : 'a stack_reduction_function
 val whd_betadeltatiota : 'a reduction_function
+val whd_betadeltaeta_stack : 'a stack_reduction_function
+val whd_betadeltaeta : 'a reduction_function
 val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
 val whd_betadeltaiotaeta : 'a reduction_function
 
 val beta_applist : (constr * constr list) -> constr
 
-
 val hnf_prod_app : 
   unsafe_env -> 'a evar_map -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
@@ -91,6 +96,16 @@ val decomp_prod : unsafe_env -> 'a evar_map -> constr -> int * constr
 val decomp_n_prod : 
   unsafe_env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr
 
+type 'a miota_args = {
+  mP      : constr;     (* the result type *)
+  mconstr : constr;     (* the constructor *)
+  mci     : case_info;  (* special info to re-build pattern *)
+  mcargs  : 'a list;    (* the constructor's arguments *)
+  mlf     : 'a array }  (* the branch code vector *)
+
+val reducible_mind_case : constr -> bool
+val reduce_mind_case : unsafe_env -> constr miota_args -> constr
+
 val is_arity : unsafe_env -> 'a evar_map -> constr -> bool
 val is_info_arity : unsafe_env -> 'a evar_map -> constr -> bool
 val is_info_sort : unsafe_env -> 'a evar_map -> constr -> bool
@@ -111,6 +126,9 @@ val subst_term_occ : int list -> constr -> constr -> constr
 val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
 val compute : 'a reduction_function
 
+val fix_recarg : constr -> 'a list -> (int * 'a) option
+val reduce_fix : (constr -> 'a list -> constr * constr list) -> constr ->
+  constr list -> bool * (constr * constr list)
 
 (*s Conversion Functions (uses closures, lazy strategy) *)
 
@@ -185,4 +203,5 @@ val minductype_spec : unsafe_env -> 'a evar_map -> constr -> constr
 val mrectype_spec : unsafe_env -> 'a evar_map -> constr -> constr
 
 (* Special function, which keep the key casts under Fix and MutCase. *)
+
 val strip_all_casts : constr -> constr
diff --git a/lib/util.ml b/lib/util.ml
index 0206bf887d..30f1cbeb65 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -150,6 +150,9 @@ let rec list_uniquize = function
   | [] -> []
   | h::t -> if List.mem h t then list_uniquize t else h::(list_uniquize t)
 
+let rec list_distinct = function
+  | h::t -> (not (List.mem h t)) && list_distinct t
+  | _ -> true
 
 (* Arrays *)
 
diff --git a/lib/util.mli b/lib/util.mli
index 6f1e258727..a40a24ba41 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -45,6 +45,7 @@ val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
 val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 val list_uniquize : 'a list -> 'a list
+val list_distinct : 'a list -> bool
 
 (*s Arrays. *)
 
diff --git a/library/declare.ml b/library/declare.ml
index 64445cf5e2..d9d55da7a6 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -172,3 +172,16 @@ let global_reference id =
   let ids =  ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
 
+let mind_path = function
+  | DOPN(MutInd (sp,0),_) -> sp
+  | DOPN(MutInd (sp,tyi),_) -> 
+      let mib = Global.lookup_mind sp in
+      let mip = mind_nth_type_packet mib tyi in 
+      let (pa,_,k) = repr_path sp in 
+      Names.make_path pa (mip.mind_typename) k 
+  | DOPN(MutConstruct ((sp,tyi),ind),_) -> 
+      let mib = Global.lookup_mind sp in
+      let mip = mind_nth_type_packet mib tyi in 
+      let (pa,_,k) = repr_path sp in 
+      Names.make_path pa (mip.mind_consnames.(ind-1)) k 
+  | _ -> invalid_arg "mind_path"
diff --git a/library/declare.mli b/library/declare.mli
index 41d1e14d3f..2cb576cf1a 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -35,3 +35,5 @@ val declare_mind : mutual_inductive_entry -> unit
   environment of variables. *)
 
 val global_reference : identifier -> constr
+
+val mind_path : constr -> section_path
diff --git a/library/global.ml b/library/global.ml
index 6385e932f4..5e11a36527 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -11,6 +11,8 @@ let global_env = ref empty_environment
 
 let env () = !global_env
 
+let unsafe_env () = unsafe_env_of_env !global_env
+
 let _ = 
   declare_summary "Global environment"
     { freeze_function = (fun () -> !global_env);
diff --git a/library/global.mli b/library/global.mli
index 2e0a541df2..f292766679 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -17,6 +17,7 @@ open Typing
    operating on that global environment. *)
 
 val env : unit -> environment
+val unsafe_env : unit -> unsafe_env
 
 val universes : unit -> universes
 val context : unit -> context
diff --git a/library/redinfo.ml b/library/redinfo.ml
new file mode 100644
index 0000000000..4e6c202156
--- /dev/null
+++ b/library/redinfo.ml
@@ -0,0 +1,98 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Generic
+open Term
+open Constant
+open Reduction
+
+type constant_evaluation = 
+  | Elimination of (int * constr) list * int * bool
+  | NotAnElimination
+
+let eval_table = ref Spmap.empty
+
+(* Check that c is an "elimination constant"
+    [xn:An]..[x1:A1](<P>MutCase (Rel i) of f1..fk end g1 ..gp)
+or  [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip)) 
+    with i1..ip distinct variables not occuring in t 
+keep relevenant information ([i1,Ai1;..;ip,Aip],n,b)
+with b = true in case of a fixpoint in order to compute 
+an equivalent of Fix(f|t)[xi<-ai] as 
+[yip:Bip]..[yi1:Bi1](F bn..b1) 
+    == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel 1)..(Rel p))
+with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1] *)
+
+exception Elimconst
+
+let compute_consteval c = 
+  let rec srec n labs c =
+    match whd_betadeltaeta_stack (Global.unsafe_env()) Evd.empty c [] with 
+      | (DOP2(Lambda, t, DLAM(_,g)), []) -> 
+	  srec (n+1) (t::labs) g
+      | (DOPN(Fix (nv,i), bodies), l) -> 
+          if (List.length l) > n then raise Elimconst;
+          let li = 
+            List.map (function
+                        | Rel k ->
+                            if array_for_all (noccurn k) bodies then 
+			      (k, List.nth labs (k-1)) 
+			    else 
+			      raise Elimconst
+                        | _ -> 
+			    raise Elimconst) l
+          in 
+	  if list_distinct (List.map fst li) then 
+	    (li,n,true) 
+          else 
+	    raise Elimconst
+      | (DOPN(MutCase _,_) as mc,lapp) -> 
+          (match destCase mc with
+             | (_,_,Rel _,_) -> ([],n,false)
+             | _ -> raise Elimconst)
+      | _ -> raise Elimconst
+  in
+  try 
+    let (lv,n,b) = srec 0 [] c in 
+    Elimination (lv,n,b) 
+  with Elimconst -> 
+    NotAnElimination
+
+let constant_eval sp =
+  try
+    Spmap.find sp !eval_table
+  with Not_found -> begin
+    let v = 
+      let cb = Global.lookup_constant sp in
+      match cb.const_body with
+	| None -> NotAnElimination
+	| Some c -> compute_consteval c
+    in
+    eval_table := Spmap.add sp v !eval_table;
+    v
+  end
+
+(* Registration as global tables and roolback. *)
+
+type frozen = constant_evaluation Spmap.t
+
+let init () =
+  eval_table := Spmap.empty
+
+let freeze () =
+  !eval_table
+
+let unfreeze ct =
+  eval_table := ct
+
+let _ = 
+  Summary.declare_summary "evaluation"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
+
+let rollback f x =
+  let fs = freeze () in
+  try f x with e -> begin unfreeze fs; raise e end
diff --git a/library/redinfo.mli b/library/redinfo.mli
new file mode 100644
index 0000000000..3f71baa982
--- /dev/null
+++ b/library/redinfo.mli
@@ -0,0 +1,19 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+(*i*)
+
+(* Elimination constants. This module implements a table which associates
+   to each constant some reduction informations used by tactics like Simpl. 
+   The following table is mostly used by the module [Tacred] 
+   (section~\refsec{tacred}). *)
+
+type constant_evaluation = 
+  | Elimination of (int * constr) list * int * bool
+  | NotAnElimination
+
+val constant_eval : section_path -> constant_evaluation
+
diff --git a/parsing/termast.ml b/parsing/termast.ml
new file mode 100644
index 0000000000..edc31f2940
--- /dev/null
+++ b/parsing/termast.ml
@@ -0,0 +1,666 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Environ
+open Coqast
+open Ast
+
+(* Different strategies for renaming of bound variables *)
+
+module type RenamingStrategy = sig
+  type used_idents = identifier list
+  val concrete_name : used_idents -> unit assumptions -> name -> constr 
+    -> identifier option * used_idents 
+  val used_of : constr -> used_idents
+  val ids_of_env : unit assumptions -> used_idents
+end
+
+(* Ancienne version de renommage des variables (avant Dec 98) *)
+
+module WeakRenamingStrategy = struct
+
+  type used_idents = identifier list
+
+  let concrete_name l n c =
+    if n = Anonymous then (None,l)
+    else 
+      let fresh_id = next_name_away n l in
+      if dependent (Rel 1) c then (Some fresh_id, fresh_id::l) else (None,l)
+  let used_of = global_vars
+  let ids_of_env env =
+    map_succeed
+      (function (Name id,_) -> id | _ -> failwith "caught") (get_rels env)
+end
+
+(* Nouvelle version de renommage des variables (DEC 98) *)
+(* This is the algorithm to display distinct bound variables 
+
+    - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
+      des noms à éviter 
+    - Règle 2 : c'est la dépendance qui décide si on affiche ou pas
+
+    Exemple : 
+    si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors
+    il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
+    mais f et f0 contribue à la liste des variables à éviter (en supposant 
+    que les noms f et f0 ne sont pas déjà pris)
+    Intérêt : noms homogènes dans un but avant et après Intro *)
+
+module StrongRenamingStrategy = struct
+
+  type used_idents = identifier list
+
+  let occur_id env id0 c =
+    let rec occur n = function
+      | VAR id             -> id=id0
+      | DOPN (Const sp,cl) -> (basename sp = id0) or (exists_vect (occur n) cl)
+      | DOPN (Abst sp,cl)  -> (basename sp = id0) or (exists_vect (occur n) cl)
+      | DOPN (MutInd _, cl) as t       -> 
+	  (basename (mind_path t) = id0) or (exists_vect (occur n) cl)
+      | DOPN (MutConstruct _, cl) as t -> 
+	  (basename (mind_path t) = id0) or (exists_vect (occur n) cl)
+      | DOPN(_,cl)         -> exists_vect (occur n) cl
+      | DOP1(_,c)          -> occur n c
+      | DOP2(_,c1,c2)      -> (occur n c1) or (occur n c2)
+      | DOPL(_,cl)         -> List.exists (occur n) cl
+      | DLAM(_,c)          -> occur (n+1) c
+      | DLAMV(_,v)         -> exists_vect (occur (n+1)) v
+      | Rel p              ->
+	  p>n &
+	  (try (fst (lookup_rel (p-n) env) = Name id0)
+	   with Not_found -> false) (* Unbound indice : may happen in debug *)
+      | DOP0 _             -> false
+    in 
+    occur 1 c
+
+  let next_name_not_occuring name l env t =
+    let rec next id =
+      if List.mem id l or occur_id env id t then next (lift_ident id) else id
+    in match name with
+      | Name id   -> next id
+      | Anonymous -> id_of_string "_"
+
+  let concrete_name l env n c =
+    if n = Anonymous then
+      if dependent (Rel 1) c then anomaly "Anonymous should be non dependent"
+      else (None,l)
+    else
+      let fresh_id = next_name_not_occuring n l env c in
+      let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in
+      (idopt, fresh_id::l)
+      
+  (* Returns the list of global variables and constants in a term *)
+  let global_vars_and_consts t =
+    let rec collect acc = function
+      | VAR id             -> id::acc
+      | DOPN (Const sp,cl) -> (basename sp)::(it_vect collect acc cl)
+      | DOPN (Abst sp,cl)  -> (basename sp)::(it_vect collect acc cl)
+      | DOPN (MutInd _, cl) as t       -> 
+	  (basename (mind_path t))::(it_vect collect acc cl)
+      | DOPN (MutConstruct _, cl) as t -> 
+	  (basename (mind_path t))::(it_vect collect acc cl)
+      | DOPN(_,cl)         -> it_vect collect acc cl
+      | DOP1(_,c)          -> collect acc c
+      | DOP2(_,c1,c2)      -> collect (collect acc c1) c2
+      | DOPL(_,cl)         -> List.fold_left collect acc cl
+      | DLAM(_,c)          -> collect acc c
+      | DLAMV(_,v)         -> it_vect collect acc v
+      | _                  -> acc
+    in 
+    uniquize (collect [] t)
+	 
+  let used_of = global_vars_and_consts
+  let ids_of_env = Names.ids_of_env
+end
+
+
+(* Tools for printing of Cases                                              *)
+(* These functions implement a light form of Termenv.mind_specif_of_mind    *)
+(* specially for handle Cases printing; they respect arities but not typing *)
+
+let indsp_of_id id  =
+  let (oper,_) =
+    try let sp = Nametab.sp_of_id CCI id in global_operator sp id
+    with Not_found -> error ("Cannot find reference "^(string_of_id id))
+  in
+  match oper with
+    | MutInd(sp,tyi) -> (sp,tyi)
+    | _ -> errorlabstrm "indsp_of_id" 
+	  [< 'sTR ((string_of_id id)^" is not an inductive type") >]
+
+let mind_specif_of_mind_light (sp,tyi) =
+  let (_,mib) = mind_of_path sp in
+  (mib,Constrtypes.mind_nth_type_packet mib tyi)
+
+let rec remove_indtypes = function
+  | (1, DLAMV(_,cl)) -> cl
+  | (n, DLAM (_,c))  -> remove_indtypes (n-1, c)
+  | _                -> anomaly "remove_indtypes: bad list of constructors"
+	
+let rec remove_params n t =
+  if n = 0 then t
+  else match t with
+    | DOP2(Prod,_,DLAM(_,c)) -> remove_params (n-1) c
+    | DOP2(Cast,c,_)         -> remove_params n c
+    | _ -> anomaly "remove_params : insufficiently quantified"
+
+let rec get_params = function
+  | DOP2(Prod,_,DLAM(x,c)) -> x::(get_params c)
+  | DOP2(Cast,c,_)         -> get_params c
+  | _                      -> []
+
+let lc_of_lmis (mib,mip) =
+  let lc = remove_indtypes (mib.mINDNTYPES,mip.mINDLC) in
+  Array.map (remove_params mib.mINDNPARAMS) lc
+
+let sp_of_spi ((sp,_) as spi) =
+  let (_,mip) = mind_specif_of_mind_light spi in
+  let (pa,_,k) = repr_path sp in 
+  make_path pa (mip.mINDTYPENAME) k
+
+
+(* Parameterization of the translation from constr to ast      *)
+
+(* Tables for Cases printing under a "if" form, a "let" form,  *)
+
+let isomorphic_to_bool lc =
+  let lcparams = Array.map get_params lc in
+  Array.length lcparams = 2 & lcparams.(0) = [] & lcparams.(1) = []
+
+let isomorphic_to_tuple lc =
+  Array.length lc = 1
+
+module PrintingCasesMake =
+  functor (Test : sig 
+     val test : constr array -> bool
+     val error_message : string
+     val member_message : identifier -> bool -> string
+     val field : string
+     val title : string
+  end) ->
+  struct
+    type t = section_path * int
+    let encode = indsp_of_id
+    let check indsp =
+      if not (Test.test (lc_of_lmis (mind_specif_of_mind_light indsp)))
+      then errorlabstrm "check_encode" [< 'sTR Test.error_message >]
+    let decode = sp_of_spi
+    let key = Options.SecondaryTable ("Printing",Test.field)
+    let title = Test.title
+    let member_message = Test.member_message
+    let synchronous = true
+  end
+
+module PrintingCasesIf =
+  PrintingCasesMake (struct 
+    let test = isomorphic_to_bool
+    let error_message = "This type cannot be seen as a boolean type"
+    let field = "If"
+    let title = "Types leading to pretty-printing of Cases using a `if' form: "
+    let member_message id = function
+      | true  -> 
+	  "Cases on elements of " ^ (string_of_id id)
+	  ^ " are printed using a `if' form"
+      | false -> 
+	  "Cases on elements of " ^ (string_of_id id)
+	  ^ " are not printed using `if' form"
+  end)
+
+module PrintingCasesLet =
+  PrintingCasesMake (struct 
+    let test = isomorphic_to_tuple
+    let error_message = "This type cannot be seen as a tuple type"
+    let field = "Let"
+    let title = 
+      "Types leading to a pretty-printing of Cases using a `let' form:"
+    let member_message id = function
+      | true  -> 
+	  "Cases on elements of " ^ (string_of_id id)
+	  ^ " are printed using a `let' form"
+      | false -> 
+	  "Cases on elements of " ^ (string_of_id id)
+	  ^ " are not printed using a `let' form"
+  end)
+
+module PrintingIf  = Options.MakeTable(PrintingCasesIf)
+module PrintingLet = Options.MakeTable(PrintingCasesLet)
+
+(* Options for printing or not wildcard and synthetisable types *)
+
+open Options
+
+let wildcard_value = ref true
+let force_wildcard () = !wildcard_value
+
+let _ = 			  
+  declare_async_bool_option 
+    { optasyncname  = "the forced wildcard option";
+      optasynckey   = Options.SecondaryTable ("Printing","Wildcard");
+      optasyncread  = force_wildcard;
+      optasyncwrite = (fun v -> wildcard_value := v) }
+
+let synth_type_value = ref true
+let synthetize_type () = !synth_type_value
+
+let _ = 
+  declare_async_bool_option 
+    { optasyncname = "the synthesisablity";
+      optasynckey   = Options.SecondaryTable ("Printing","Synth");
+      optasyncread = synthetize_type;
+      optasyncwrite = (fun v -> synth_type_value := v) }
+
+(* Printing of implicit *)
+
+let print_implicits = ref false
+
+
+(* The main translation function is bdize_depcast *)
+
+module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
+
+  (* pour les implicites *)
+
+  (* l est ordonne'ee (croissant), ne garder que les elements <= n *)
+  let filter_until n l =
+    let rec aux = function
+      | [] -> []
+      | i::l -> if i > n then [] else i::(aux l)
+    in 
+    aux l
+
+  (* l est ordonne'e (de'croissant), n>=max(l), diviser l en deux listes,
+     la 2eme est la plus longue se'quence commencant par n,
+     la 1ere contient les autres elements *)
+
+  let rec div_implicits n = 
+    function 
+      | [] -> [],[]
+      | i::l -> 
+	  if i = n then 
+	    let l1,l2=(div_implicits (n-1) l) in l1,i::l2
+          else 
+	    i::l,[]
+
+  let bdize_app c al =
+    let impl =
+      match c with
+        | DOPN(MutConstruct _,_) -> mconstr_implicits c
+	| DOPN(MutInd _,_) -> mind_implicits c
+	| DOPN(Const _,_) -> constant_implicits c
+	| VAR id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
+	| _ -> []
+    in
+    if impl = [] then 
+      ope("APPLIST", al)
+    else if !print_implicits then 
+      ope("APPLIST", ope("XTRA",[str "!";List.hd al])::List.tl al)
+    else 
+      let largs = List.length al - 1 in
+      let impl = List.rev (filter_until largs impl) in
+      let impl1,impl2=div_implicits largs impl in
+      let al1 = Array.of_list al in
+      List.iter
+        (fun i -> al1.(i) <-
+           ope("XTRA", [str "!"; str "EX"; num i; al1.(i)]))
+        impl2;
+      List.iter
+        (fun i -> al1.(i) <-
+           ope("XTRA",[str "!"; num i; al1.(i)]))
+        impl1;
+      al1.(0) <- ope("XTRA",[str "!"; al1.(0)]);
+      ope("APPLIST",Array.to_list al1)
+
+  type optioncast = WithCast | WithoutCast
+
+  (* [reference_tree p] pre-computes the variables and de bruijn occurring
+     in a term to avoid a O(n2) factor when computing dependent each time *)
+
+  type ref_tree = NODE of (int list * identifier list) * ref_tree list
+
+  let combine l =
+    let rec combine_rec = function
+      | [] -> [],[]
+      | NODE ((a,b),_)::l -> 
+	  let a',b' = combine_rec l in (union a a',union b b')
+    in 
+    NODE (combine_rec l,l)
+
+  let rec reference_tree p = function
+    | VAR id -> NODE (([],[id]),[])
+    | Rel n  -> NODE (([n-p],[]),[])
+    | DOP0 op -> NODE (([],[]),[])
+    | DOP1(op,c) -> reference_tree p c
+    | DOP2(op,c1,c2) -> combine [reference_tree p c1;reference_tree p c2]
+    | DOPN(op,cl) -> combine (List.map (reference_tree p) (Array.to_list cl))
+    | DOPL(op,cl) -> combine (List.map (reference_tree p) cl)
+    | DLAM(na,c) -> reference_tree (p+1) c 
+    | DLAMV(na,cl) -> 
+	combine (List.map (reference_tree (p+1))(Array.to_list cl))
+
+  (* Auxiliary function for MutCase printing *)
+  (* [computable] tries to tell if the predicate typing the result is 
+     inferable *) 
+
+  let computable p k =
+    (* We first remove as many lambda as the arity, then we look
+       if it remains a lambda for a dependent elimination. This function
+       works for normal eta-expanded term. For non eta-expanded or
+       non-normal terms, it may affirm the pred is synthetisable
+       because of an undetected ultimate dependent variable in the second
+       clause, or else, it may affirms the pred non synthetisable
+       because of a non normal term in the fourth clause.
+       A solution could be to store, in the MutCase, the eta-expanded
+       normal form of pred to decide if it depends on its variables
+
+       Lorsque le prédicat est dépendant de manière certaine, on
+       ne déclare pas le prédicat synthétisable (même si la
+       variable dépendante ne l'est pas effectivement) parce que
+       sinon on perd la réciprocité de la synthèse (qui, lui,
+       engendrera un prédicat non dépendant) *)
+
+  let rec striprec = function
+      (0,DOP2(Lambda,_,DLAM(_,d))) -> false
+    | (0,d               )         -> noccur_bet 1 k d
+    | (n,DOP2(Lambda,_,DLAM(_,d))) -> striprec (n-1,d)
+    |  _                           -> false
+  in striprec (k,p)
+
+  (* Main translation function from constr -> ast *)
+
+  let bdize_depcast opcast at_top env t =
+    let init_avoid = if at_top then Strategy.ids_of_env env else [] in
+    let rec bdrec avoid env t = 
+      match collapse_appl t with
+        (* Not well-formed constructions *)
+	| DLAM(na,c) ->
+	    (match Strategy.concrete_name avoid env na c with
+	       | (Some id,avoid') -> 
+		   slam(Some (string_of_id id),
+			bdrec avoid' (add_rel (Name id,()) env) c)
+               | (None,avoid') -> slam(None,bdrec avoid' env (pop c)))
+	| DLAMV(na,cl) ->
+	    if not(exists_vect (dependent (Rel 1)) cl) then
+	      slam(None,ope("V$", map_vect_list 
+			      (fun c -> bdrec avoid env (pop c)) cl))
+	    else
+	      let id = next_name_away na avoid in 
+	      slam(Some (string_of_id id),
+		   ope("V$", map_vect_list 
+			 (bdrec (id::avoid) (add_rel (Name id,()) env)) cl))
+
+        (* Well-formed constructions *)
+	| regular_constr -> 
+	    (match kind_of_term regular_constr with
+	       | IsRel n ->
+		   (try match fst(lookup_rel n env) with
+		      | Name id -> nvar (string_of_id id)
+		      | Anonymous -> raise Not_found
+		    with Not_found -> ope("REL",[num n]))
+               (* TODO: Change this to subtract the current depth *)
+	       | IsMeta n -> ope("META",[num n])
+	       | IsVar id -> nvar (string_of_id id)
+	       | IsXtra (s,pl,cl) -> 
+		   ope("XTRA",((str s):: pl@(List.map (bdrec avoid env) cl)))
+	       | IsSort s ->
+		   (match s with
+		      | Prop c -> ope("PROP",[ide (str_of_contents c)])
+		      | Type u -> ope("TYPE",[path_section dummy_loc u.u_sp; 
+					      num u.u_num]))
+	       | IsImplicit -> ope("IMPLICIT",[])     
+	       | IsCast (c1,c2) ->
+		   if opcast = WithoutCast then 
+		     bdrec avoid env c1 
+		   else 
+		     ope("CAST",[bdrec avoid env c1;bdrec avoid env c2])
+	       | IsProd (Anonymous,ty,c) ->
+                   (* Anonymous product are never factorized *)
+		   ope("PROD",[bdrec [] env ty;
+			       slam(None,bdrec avoid env (pop c))])
+	       | IsProd (Name _ as na,ty,c) ->
+		   let (n,a) = factorize_binder 1 avoid env Prod na ty c in
+                   (* PROD et PRODLIST doivent être distingués à cause du cas
+		      non dépendant, pour isoler l'implication; 
+		      peut-être un constructeur ARROW serait-il 
+		      plus justifié ? *)
+		   let oper = if n=1 then "PROD" else "PRODLIST" in
+		   ope(oper,[bdrec [] env ty;a])
+	       | IsLambda (na,ty,c) ->
+		   let (_,a) = factorize_binder 1 avoid env Lambda na ty c in
+                   (* LAMBDA et LAMBDALIST se comportent pareil *)
+		   ope("LAMBDALIST",[bdrec [] env ty;a])
+	       | IsAppL (f,args) ->
+		   bdize_app f (List.map (bdrec avoid env) (f::args))
+
+	       | IsConst (sp,cl) ->
+		   ope("CONST",((path_section dummy_loc sp)::
+				(map_vect_list (bdrec avoid env) cl)))
+	       | IsAbst (sp,cl) ->
+		   ope("ABST",((path_section dummy_loc sp)::
+			       (map_vect_list (bdrec avoid env) cl)))
+	       | IsMutInd (sp,tyi,cl) ->
+		   ope("MUTIND",((path_section dummy_loc sp)::(num tyi)::
+				 (map_vect_list (bdrec avoid env) cl)))
+	       | IsMutConstruct (sp,tyi,n,cl) ->
+		   ope("MUTCONSTRUCT",
+		       ((path_section dummy_loc sp)::(num tyi)::(num n)::
+			(map_vect_list (bdrec avoid env) cl)))
+	       | IsMutCase (annot,p,c,bl) ->
+		   let synth_type = synthetize_type () in
+		   let tomatch = bdrec avoid env c in
+		   begin match annot with
+		     | None -> 
+			 (* Pas d'annotation --> affichage avec vieux Case *)
+			 let pred = bdrec avoid env p in
+			 let bl' = map_vect_list (bdrec avoid env) bl in
+			 ope("MUTCASE",pred::tomatch::bl')
+		     | Some indsp ->
+			 let (mib,mip as lmis) = 
+			   mind_specif_of_mind_light indsp in
+			 let lc = lc_of_lmis lmis in
+			 let lcparams = Array.map get_params lc in
+			 let k = 
+			   (nb_prod mip.mINDARITY.body) - mib.mINDNPARAMS in
+			 let pred = 
+			   if synth_type & computable p k & lcparams <> [||]
+			   then ope("XTRA", [str "SYNTH"])
+			   else bdrec avoid env p 
+			 in
+			 if PrintingIf.active indsp then 
+			   ope("FORCEIF", [ pred; tomatch;
+					    bdrec avoid env bl.(0); 
+					    bdrec avoid env bl.(1) ])
+			 else
+			   let idconstructs = mip.mINDCONSNAMES in
+			   let asttomatch = 
+			     ope("XTRA",[str "TOMATCH"; tomatch]) in
+			   let eqnv = 
+			     map3_vect (bdize_eqn avoid env) idconstructs 
+			       lcparams bl in
+			   let eqnl = Array.to_list eqnv in
+			   let tag =
+			     if PrintingLet.active indsp then 
+			       "FORCELET" 
+			     else 
+			       "MULTCASE"
+			   in 
+			   ope("XTRA", (str tag)::pred::asttomatch::eqnl)
+		   end
+
+	       | IsFix (nv,n,cl,lfn,vt) ->
+		   let lfi = 
+		     List.map (fun na -> next_name_away na avoid) lfn in
+		   let def_env = 
+		     List.fold_left
+		       (fun env id -> add_rel (Name id,()) env) env lfi in
+		   let def_avoid = lfi@avoid in
+		   let f = List.nth lfi n in
+		   let rec split_lambda binds env avoid = function
+		       (0, t) -> 
+			 binds,bdrec avoid env t
+		     | (n, DOP2(Cast,t,_)) -> 
+			 split_lambda binds env avoid (n,t)
+		     | (n, DOP2(Lambda,t,DLAM(na,b))) ->
+			 let ast = bdrec avoid env t in
+			 let id = next_name_away na avoid in
+			 let ast_of_bind = 
+			   ope("BINDER",[ast;nvar (string_of_id id)]) in
+			 let new_env = add_rel (Name id,()) env in
+			 split_lambda (ast_of_bind::binds) 
+			   new_env (id::avoid) (n-1,b)
+		     | _ -> error "split_lambda" 
+		   in
+		   let rec split_product env avoid = function
+		     | (0, t) -> bdrec avoid env t
+		     | (n, DOP2(Cast,t,_)) -> split_product env avoid (n,t)
+		     | (n, DOP2(Prod,t,DLAM(na,b))) ->
+			 let ast = bdrec avoid env t in
+			 let id = next_name_away na avoid in
+			 let new_env = add_rel (Name id,()) env in
+			 split_product new_env (id::avoid) (n-1,b)
+		     | _ -> error "split_product" 
+		   in
+		   let listdecl = 
+		     map_i
+		       (fun i fi ->
+			  let (lparams,ast_of_def) =
+			    split_lambda [] def_env def_avoid 
+			      (nv.(i)+1,vt.(i)) in
+			  let ast_of_typ = 
+			    split_product env avoid (nv.(i)+1,cl.(i)) in
+			  ope("FDECL",
+			      [ nvar (string_of_id fi); 
+				ope ("BINDERS",List.rev lparams);
+				ast_of_typ; ast_of_def ]))
+		       0 lfi 
+		   in 
+		   ope("FIX", (nvar (string_of_id f))::listdecl)
+
+	       | IsCoFix (n,cl,lfn,vt) ->
+		   let lfi = 
+		     List.map (fun na -> next_name_away na avoid) lfn in
+		   let def_env =
+		     List.fold_left 
+		       (fun env id -> add_rel (Name id,()) env) env lfi in
+		   let def_avoid = lfi@avoid in
+		   let f = List.nth lfi n in
+		   let listdecl =
+		     map_i (fun i fi -> ope("CFDECL",
+					    [nvar (string_of_id fi);
+					     bdrec avoid env cl.(i);
+					     bdrec def_avoid def_env vt.(i)]))
+		       0 lfi
+		   in 
+		   ope("COFIX", (nvar (string_of_id f))::listdecl))
+
+    and bdize_eqn avoid env constructid construct_params branch =
+      let print_underscore = force_wildcard () in
+      let cnvar = nvar (string_of_id constructid) in
+      let rec buildrec nvarlist avoid env = function
+	| _::l, DOP2(Lambda,_,DLAM(x,b)) -> 
+	    let x'=
+              if not print_underscore or (dependent (Rel 1) b) then x 
+              else Anonymous in
+            let id = next_name_away x' avoid in
+            let new_env = (add_rel (Name id,()) env) in
+            let new_avoid = id::avoid in
+            let new_nvarlist = (nvar (string_of_id id))::nvarlist in
+            buildrec new_nvarlist new_avoid new_env (l,b)
+	      
+	| l, DOP2(Cast,b,_) -> 
+	    (* Oui, il y a parfois des cast *)
+	    buildrec nvarlist avoid env (l,b)
+	      
+	| x::l, b -> 
+	    (* eta-expansion : n'arrivera plus lorsque tous les
+	       termes seront construits à partir de la syntaxe Cases
+	       nommage de la nouvelle variable *)
+            let id = next_name_away_with_default "x" x avoid in
+	    let new_nvarlist = (nvar (string_of_id id))::nvarlist in
+            let new_env = (add_rel (Name id,()) env) in
+            let new_avoid = id::avoid in
+            let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
+            buildrec new_nvarlist new_avoid new_env (l,new_b)
+
+	| [], b	-> 
+	    let pattern =
+              if nvarlist = [] then cnvar
+              else ope ("APPLIST", cnvar::(List.rev nvarlist)) in
+	    let action = bdrec avoid env b in
+	    ope("XTRA", [str "EQN"; action; pattern])
+      in 
+      buildrec [] avoid env (construct_params,branch)
+
+    and factorize_binder n avoid env oper na ty c =
+      let (env2, avoid2,na2) =
+	match Strategy.concrete_name avoid env na c with
+	  | (Some id,l') -> 
+	      add_rel (Name id,()) env, l', Some (string_of_id id) 
+	  | (None,l') -> 
+	      add_rel (Anonymous,()) env, l', None
+      in
+      let (p,body) = match c with
+	| DOP2(oper',ty',DLAM(na',c')) 
+	    when (oper = oper')
+	      & eq_constr (lift 1 ty) ty'
+	      & not (na' = Anonymous & oper = Prod)
+	      -> factorize_binder (n+1) avoid2 env2 oper na' ty' c'
+	| _ -> (n,bdrec avoid2 env2 c)
+      in 
+      (p,slam(na2, body))
+    in
+    bdrec init_avoid env t
+
+  let bdize  = bdize_depcast WithCast
+  let bdize_no_casts = bdize_depcast WithoutCast
+
+  let lookup_name_as_renamed env t s =
+    let rec lookup avoid env n = function
+      | DOP2(Prod,_,DLAM(name,c')) ->
+	  (match Strategy.concrete_name avoid env name c' with
+             | (Some id,avoid') -> 
+		 if id=s then (Some n) 
+		 else lookup avoid' (add_rel (Name id,()) env) (n+1) c'
+	     | (None,avoid') -> lookup avoid' env (n+1) (pop c'))
+      | DOP2(Cast,c,_) -> lookup avoid env n c
+      | _ -> None
+    in 
+    lookup (Strategy.ids_of_env env) env 1 t
+
+  let lookup_index_as_renamed t n =
+    let rec lookup n d = function
+      | DOP2(Prod,_,DLAM(name,c')) -> 
+	  (match Strategy.concrete_name [] (gLOB nil_sign) name c' with
+             | (Some _,_) -> lookup n (d+1) c'
+             | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+      | DOP2(Cast,c,_) -> lookup n d c
+      | _ -> None
+    in 
+    lookup n 1 t
+
+end (* of functor MakeTermAst *)
+
+(* This old version are currently no longer used.
+
+Until V6.2.4, similar names were allowed in hypothesis and quatified
+variables of a goal. This behaviour can still be recovered by using
+the functions available in the WeakTermAst module.
+
+module WeakTermAst = MakeTermAst(WeakRenamingStrategy)
+
+let bdize = WeakTermAst.bdize
+let bdize_no_casts = WeakTermAst.bdize_no_casts
+let lookup_name_as_renamed = WeakTermAst.lookup_name_as_renamed
+let lookup_index_as_renamed = WeakTermAst.lookup_index_as_renamed
+*)
+
+module StrongTermAst = MakeTermAst(StrongRenamingStrategy)
+
+let bdize = StrongTermAst.bdize
+let bdize_no_casts = StrongTermAst.bdize_no_casts
+let lookup_name_as_renamed = StrongTermAst.lookup_name_as_renamed
+let lookup_index_as_renamed = StrongTermAst.lookup_index_as_renamed
diff --git a/proofs/tacred.ml b/proofs/tacred.ml
index a532e8cbcc..16ea6c5896 100644
--- a/proofs/tacred.ml
+++ b/proofs/tacred.ml
@@ -1,104 +1,190 @@
 
 (* $Id$ *)
 
-let is_elim env sigma c =
-  let (sp, cl) = destConst c in
-  if (evaluable_constant env c) && (defined_constant env c) then begin
-    let cb = lookup_constant sp env in 
-    (match cb.cONSTEVAL with
-       | Some _ -> ()
-       | None -> 
-	   (match cb.cONSTBODY with
-	      | Some{contents=COOKED b} ->
-		  cb.cONSTEVAL <- Some(compute_consteval b)
-	      | Some{contents=RECIPE _} ->
-		  anomalylabstrm "Reduction.is_elim"
-		    [< 'sTR"Found an uncooked transparent constant,"; 'sPC ;
-		       'sTR"which is supposed to be impossible" >]
-	      | _ -> assert false));
-    (match (cb.cONSTEVAL) with
-       | Some (Some x) -> x
-       | Some None -> raise Elimconst
-       | _ -> assert false)
-  end else 
-    raise Elimconst
-
-let make_elim_fun sigma f largs =
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Inductive
+open Environ
+open Reduction
+open Instantiate
+open Redinfo
+
+exception Elimconst
+exception Redelimination
+
+let is_elim c =
+  let (sp, _) = destConst c in
+  match constant_eval sp with
+    | NotAnElimination -> raise Elimconst
+    | Elimination (lv,n,b) -> (lv,n,b)
+
+let rev_firstn_liftn fn ln = 
+  let rec rfprec p res l = 
+    if p = 0 then 
+      res 
+    else
+      match l with
+        | [] -> invalid_arg "Reduction.rev_firstn_liftn"
+        | a::rest -> rfprec (p-1) ((lift ln a)::res) rest
+  in 
+  rfprec fn []
+
+let make_elim_fun f largs =
   try 
-    let (lv,n,b) = is_elim sigma f 
+    let (lv,n,b) = is_elim f 
     and ll = List.length largs in 
     if ll < n then raise Redelimination;
     if b then
-      let labs,_ = chop_list n largs in
+      let labs,_ = list_chop n largs in
       let p = List.length lv in
-      let la' = map_i (fun q aq ->
-			 try (Rel (p+1-(index (n+1-q) (List.map fst lv)))) 
-			 with Failure _ -> aq) 1
+      let la' = list_map_i 
+		  (fun q aq ->
+		     try (Rel (p+1-(list_index (n+1-q) (List.map fst lv)))) 
+		     with Failure _ -> aq) 1
                   (List.map (lift p) labs) 
       in
-      it_list_i (fun i c (k,a) -> 
-                   DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
-                   	DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv
+      list_fold_left_i 
+	(fun i c (k,a) -> 
+           DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
+                DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv
     else 
       f
   with Elimconst | Failure _ -> 
     raise Redelimination
 
+let mind_nparams env i =
+  let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
+
+(* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make 
+   the reduction using this extra information *)
+
+let contract_fix_use_function f fix =
+  match fix with 
+    | DOPN(Fix(recindices,bodynum),bodyvect) ->
+  	let nbodies = Array.length recindices in
+  	let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in
+  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
+	  sAPPViList bodynum (array_last bodyvect) lbodies
+    | _ -> assert false
+
+let reduce_fix_use_function f whfun fix stack =
+  match fix with 
+    | DOPN (Fix(recindices,bodynum),bodyvect) ->
+	(match fix_recarg fix stack with
+           | None -> (false,(fix,stack))
+	   | Some (recargnum,recarg) ->
+               let (recarg'hd,_ as recarg')= whfun recarg [] in
+               let stack' = list_assign stack recargnum (applist recarg') in
+	       (match recarg'hd with
+                  | DOPN(MutConstruct _,_) ->
+		      (true,(contract_fix_use_function f fix,stack'))
+		  | _ -> (false,(fix,stack'))))
+    | _ -> assert false
+
+let contract_cofix_use_function f cofix =
+  match cofix with 
+    | DOPN(CoFix(bodynum),bodyvect) ->
+  	let nbodies =  (Array.length bodyvect) -1 in
+  	let make_Fi j = DOPN(CoFix(j),bodyvect) in
+  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
+  	sAPPViList bodynum (array_last bodyvect) lbodies
+    | _ -> assert false
+
+let reduce_mind_case_use_function env f mia =
+  match mia.mconstr with 
+    | DOPN(MutConstruct((indsp,tyindx),i),_) ->
+	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
+	let nparams = mind_nparams env ind in
+	let real_cargs = snd(list_chop nparams mia.mcargs) in
+	applist (mia.mlf.(i-1),real_cargs)
+    | DOPN(CoFix _,_) as cofix ->
+	let cofix_def = contract_cofix_use_function f cofix in
+	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
+    | _ -> assert false
+	  
+let special_red_case env whfun p c ci lf  =
+  let rec redrec c l = 
+    let (constr,cargs) = whfun c l in 
+    match constr with 
+      | DOPN(Const _,_) as g -> 
+          if evaluable_constant env g then
+            let gvalue = constant_value env g in
+            if reducible_mind_case gvalue then
+              reduce_mind_case_use_function env g
+                {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
+            else 
+	      redrec gvalue cargs
+          else 
+	    raise Redelimination
+      | _ ->
+          if reducible_mind_case constr then
+            reduce_mind_case env
+              {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf}
+          else 
+	    raise Redelimination
+  in 
+  redrec c []
+
 let rec red_elim_const env sigma k largs =
   if not (evaluable_constant env k) then raise Redelimination;
-  let f = make_elim_fun sigma k largs in
-  match whd_betadeltaeta_stack sigma (const_value sigma k) largs with
+  let f = make_elim_fun k largs in
+  match whd_betadeltaeta_stack env sigma (constant_value env k) largs with
     | (DOPN(MutCase _,_) as mc,lrest) ->
         let (ci,p,c,lf) = destCase mc in
-        (special_red_case sigma (construct_const sigma) p c ci lf, lrest)
+        (special_red_case env (construct_const env sigma) p c ci lf, lrest)
     | (DOPN(Fix _,_) as fix,lrest) -> 
         let (b,(c,rest)) = 
-	  reduce_fix_use_function f (construct_const sigma) fix lrest
+	  reduce_fix_use_function f (construct_const env sigma) fix lrest
         in 
-	if b then (nf_beta c, rest) else raise Redelimination
+	if b then (nf_beta env sigma c, rest) else raise Redelimination
     | _ -> assert false
 
-and construct_const sigma c stack = 
+and construct_const env sigma c stack = 
   let rec hnfstack x stack =
     match x with
       | (DOPN(Const _,_)) as k  ->
           (try
-             let (c',lrest) = red_elim_const sigma k stack in hnfstack c' lrest
+             let (c',lrest) = red_elim_const env sigma k stack in 
+	     hnfstack c' lrest
            with Redelimination ->
-             if evaluable_const sigma k then 
-	       let cval = const_value sigma k in
+             if evaluable_constant env k then 
+	       let cval = constant_value env k in
 	       (match cval with
                   | DOPN (CoFix _,_) -> (k,stack)
-                  | _                -> hnfstack cval stack) 
+                  | _ -> hnfstack cval stack) 
              else 
 	       raise Redelimination)
       | (DOPN(Abst _,_) as a) ->
-          if evaluable_abst a then 
-	    hnfstack (abst_value a) stack
+          if evaluable_abst env a then 
+	    hnfstack (abst_value env a) stack
           else 
 	    raise Redelimination
-      | DOP2(Cast,c,_)   -> hnfstack c stack
-      | DOPN(AppL,cl)    -> hnfstack (hd_vect cl) (app_tl_vect cl stack)
+      | DOP2(Cast,c,_) -> hnfstack c stack
+      | DOPN(AppL,cl) -> hnfstack (array_hd cl) (array_app_tl cl stack)
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match stack with 
              | [] -> assert false
              | c'::rest -> stacklam hnfstack [c'] c rest)
-    | DOPN(MutCase _,_) as c_0 ->
-        let (ci,p,c,lf) = destCase c_0 in
-        hnfstack (special_red_case sigma (construct_const sigma) p c ci lf) 
-	  stack
-    | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
-    | DOPN(CoFix _,_) as c_0 -> c_0,stack
-    | DOPN(Fix (_) ,_) as fix -> 
-        let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack in 
-	if reduced then hnfstack fix stack' else raise Redelimination
-    | _ -> raise Redelimination
+      | DOPN(MutCase _,_) as c_0 ->
+          let (ci,p,c,lf) = destCase c_0 in
+          hnfstack 
+	    (special_red_case env (construct_const env sigma) p c ci lf) 
+	    stack
+      | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
+      | DOPN(CoFix _,_) as c_0 -> c_0,stack
+      | DOPN(Fix (_) ,_) as fix -> 
+          let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack in 
+	  if reduced then hnfstack fix stack' else raise Redelimination
+      | _ -> raise Redelimination
   in 
   hnfstack c stack
 
 (* Hnf reduction tactic: *)
 
-let hnf_constr sigma c = 
+let hnf_constr env sigma c = 
   let rec redrec x largs =
     match x with
       | DOP2(Lambda,t,DLAM(n,c)) ->
@@ -108,60 +194,61 @@ let hnf_constr sigma c =
       | DOPN(AppL,cl)   -> redrec (array_hd cl) (array_app_tl cl largs)
       | DOPN(Const _,_) ->
           (try
-             let (c',lrest) = red_elim_const sigma x largs in 
+             let (c',lrest) = red_elim_const env sigma x largs in 
 	     redrec c' lrest
            with Redelimination ->
-             if evaluable_const sigma x then
-               let c = const_value sigma x in
+             if evaluable_constant env x then
+               let c = constant_value env x in
 	       (match c with 
                   | DOPN(CoFix _,_) -> applist(x,largs)
 		  | _ ->  redrec c largs)
              else 
 	       applist(x,largs))
       | DOPN(Abst _,_) ->
-          if evaluable_abst x then 
-	    redrec (abst_value x) largs
+          if evaluable_abst env x then 
+	    redrec (abst_value env x) largs
           else 
 	    applist(x,largs)
       | DOP2(Cast,c,_) -> redrec c largs
       | DOPN(MutCase _,_) ->
           let (ci,p,c,lf) = destCase x in
           (try
-             redrec (special_red_case sigma (whd_betadeltaiota_stack sigma) 
-		       p c ci lf) largs
+             redrec 
+	       (special_red_case env (whd_betadeltaiota_stack env sigma) 
+		  p c ci lf) largs
            with Redelimination -> 
 	     applist(x,largs))
       | (DOPN(Fix _,_)) ->
           let (reduced,(fix,stack)) = 
-            reduce_fix (whd_betadeltaiota_stack sigma) x largs
+            reduce_fix (whd_betadeltaiota_stack env sigma) x largs
           in 
 	  if reduced then redrec fix stack else applist(x,largs)
-      | _         -> applist(x,largs)
+      | _ -> applist(x,largs)
   in 
   redrec c []
 
 (* Simpl reduction tactic: same as simplify, but also reduces
    elimination constants *)
 
-let whd_nf sigma c = 
+let whd_nf env sigma c = 
   let rec nf_app c stack =
     match c with
       | DOP2(Lambda,c1,DLAM(name,c2))    ->
           (match stack with
              | [] -> (c,[])
              | a1::rest -> stacklam nf_app [a1] c2 rest)
-      | DOPN(AppL,cl) -> nf_app (hd_vect cl) (app_tl_vect cl stack)
+      | DOPN(AppL,cl) -> nf_app (array_hd cl) (array_app_tl cl stack)
       | DOP2(Cast,c,_) -> nf_app c stack
       | DOPN(Const _,_) ->
           (try
-             let (c',lrest) = red_elim_const sigma c stack in 
+             let (c',lrest) = red_elim_const env sigma c stack in 
 	     nf_app c' lrest
            with Redelimination -> 
 	     (c,stack))
       | DOPN(MutCase _,_) ->
           let (ci,p,d,lf) = destCase c in
           (try
-             nf_app (special_red_case sigma nf_app p d ci lf) stack
+             nf_app (special_red_case env nf_app p d ci lf) stack
            with Redelimination -> 
 	     (c,stack))
       | DOPN(Fix _,_) ->
@@ -171,7 +258,7 @@ let whd_nf sigma c =
   in 
   applist (nf_app c [])
 
-let nf sigma c = strong (whd_nf sigma) c
+let nf env sigma c = strong whd_nf env sigma c
 
 (* Generic reduction: reduction functions used in reduction tactics *)
 
@@ -179,8 +266,8 @@ type red_expr =
   | Red
   | Hnf
   | Simpl
-  | Cbv of flags
-  | Lazy of flags
+  | Cbv of Closure.flags
+  | Lazy of Closure.flags
   | Unfold of (int list * section_path) list
   | Fold of constr list
   | Change of constr
@@ -194,5 +281,73 @@ let reduction_of_redexp = function
   | Lazy f -> clos_norm_flags f
   | Unfold ubinds -> unfoldn ubinds
   | Fold cl -> fold_commands cl
-  | Change t -> (fun _ _ -> t)
-  | Pattern lp -> (fun _ -> pattern_occs lp)
+  | Change t -> (fun _ _ _ -> t)
+  | Pattern lp -> pattern_occs lp
+
+(* Used in several tactics. *)
+
+let one_step_reduce env sigma = 
+  let rec redrec largs x =
+    match x with
+      | DOP2(Lambda,t,DLAM(n,c))  ->
+          (match largs with
+             | []      -> error "Not reducible 1"
+             | a::rest -> applistc (subst1 a c) rest)
+      | DOPN(AppL,cl) -> redrec (array_app_tl cl largs) (array_hd cl)
+      | DOPN(Const _,_) ->
+          (try
+             let (c',l) = red_elim_const env sigma x largs in applistc c' l
+           with Redelimination ->
+             if evaluable_constant env x then
+               applistc (constant_value env x) largs
+             else error "Not reductible 1")
+      | DOPN(Abst _,_) ->
+          if evaluable_abst env x then applistc (abst_value env x) largs
+          else error "Not reducible 0"
+      | DOPN(MutCase _,_) ->
+          let (ci,p,c,lf) = destCase x in
+          (try
+	     applistc 
+	       (special_red_case env (whd_betadeltaiota_stack env sigma) 
+		  p c ci lf) largs 
+           with Redelimination -> error "Not reducible 2")
+      | DOPN(Fix _,_) ->
+          let (reduced,(fix,stack)) = 
+	    reduce_fix (whd_betadeltaiota_stack env sigma) x largs
+          in 
+	  if reduced then applistc fix stack else error "Not reducible 3"
+      | DOP2(Cast,c,_) -> redrec largs c
+      | _ -> error "Not reducible 3"
+  in 
+  redrec []
+
+(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
+   return name, B and t' *)
+
+let reduce_to_mind env sigma t = 
+  let rec elimrec t l = 
+    match whd_castapp_stack t [] with
+      | (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l)
+      | (DOPN(Const _,_),_) -> 
+          (try 
+	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
+	     elimrec t' l
+           with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
+               [< 'sTR"Not an inductive product : it is a constant." >])
+      | (DOPN(MutCase _,_),_) ->
+          (try 
+	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
+	     elimrec t' l
+           with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
+               [< 'sTR"Not an inductive product:"; 'sPC;
+		  'sTR"it is a case analysis term" >])
+      | (DOP2(Cast,c,_),[]) -> elimrec c l
+      | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
+      | _ -> error "Not an inductive product"
+ in 
+ elimrec t []
+
+let reduce_to_ind env sigma t =
+  let (mind,redt,c) = reduce_to_mind env sigma t in 
+  (Declare.mind_path mind, redt, c)
+