Merge branch 'v8.5'

34 files changed, 773 insertions, 806 deletions

diff --git a/Makefile.build b/Makefile.build
index c5b4bbfe85..8f64d1ff26 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -59,7 +59,7 @@ CURDEPS:=$(addsuffix .d, $(CURFILES))
 VERBOSE=
 NO_RECOMPILE_ML4=
 NO_RECALC_DEPS=
-READABLE_ML4=true	# non-empty means .ml of .ml4 will be ascii instead of binary
+READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
 VALIDATE=
 COQ_XML=	# is "-xml" when building XML library
 VM=		# is "-no-vm" to not use the vm"
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 792e6f6322..0d33d43345 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -174,6 +174,7 @@ val interp_context_evars :
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
 
+val locate_reference :  Libnames.qualid -> Globnames.global_reference
 val is_global : Id.t -> bool
 val construct_reference : named_context -> Id.t -> constr
 val global_reference : Id.t -> constr
diff --git a/library/universes.ml b/library/universes.ml
index 51c2b4d851..9fddc7067b 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -772,7 +772,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	      else 
 		try let lev = Option.get (Universe.level inst) in
 		      Constraint.add (lev, d, r) cstrs
-		with Option.IsNone -> assert false)
+		with Option.IsNone -> failwith "")
 	      cstrs dangling
 	    in
 	      (ctx', us, algs, insts, cstrs'), b
@@ -784,7 +784,8 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	  | None -> (* Nothing to do *)
 	    acc' (acc, (true, false, Universe.make u))
 	  | Some lbound ->
-	    acc' (instantiate_lbound lbound)
+	     try acc' (instantiate_lbound lbound) 
+	     with Failure _ -> acc' (acc, (true, false, Universe.make u))
   and aux (ctx', us, algs, seen, cstrs as acc) u =
     try acc, LMap.find u seen 
     with Not_found -> instance acc u
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index 5f653ee109..a0930f15f4 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -59,6 +59,7 @@ Extract Constant Compare_dec.nat_compare =>
  "fun n m -> if n=m then Eq else if n<m then Lt else Gt".
 Extract Inlined Constant Compare_dec.leb => "(<=)".
 Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)".
+Extract Inlined Constant Compare_dec.lt_dec => "(<)".
 Extract Constant Compare_dec.lt_eq_lt_dec =>
  "fun n m -> if n>m then None else Some (n<m)".
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 2f7f21e418..7d034db552 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -209,7 +209,7 @@ open Hints
 let extend_with_auto_hints l seq gl=
   let seqref=ref seq in
   let f p_a_t =
-    match p_a_t.code with
+    match repr_auto_tactic p_a_t.code with
 	Res_pf (c,_) | Give_exact (c,_)
       | Res_pf_THEN_trivial_fail (c,_) ->
 	  (try
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 04347537f2..4a832435f8 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -44,18 +44,20 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g
 
 let debug_queue = Stack.create ()
 
-let rec print_debug_queue b e = 
+let rec print_debug_queue e = 
   if  not (Stack.is_empty debug_queue) 
   then
     begin
       let lmsg,goal = Stack.pop debug_queue in 
-      if b then 
-	Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
-      else
-	begin
-	  Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
-	end;
-      print_debug_queue false e;
+      let _ =
+	match e with
+	| Some e ->
+	   Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+	| None ->
+	   begin
+	     Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
+	   end in
+      print_debug_queue None ;
     end
 
 let observe strm =
@@ -68,13 +70,13 @@ let do_observe_tac s tac g =
   let lmsg = (str "observation : ") ++ s in 
   Stack.push (lmsg,goal) debug_queue;
   try 
-    let v = tac g in 
+    let v = tac g in
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
     let reraise = Errors.push reraise in
     if not (Stack.is_empty debug_queue)
-    then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise));
+    then print_debug_queue (Some (fst (Cerrors.process_vernac_interp_error reraise)));
     iraise reraise
 
 let observe_tac_stream s tac g =
@@ -941,13 +943,13 @@ let revert idl =
     (generalize (List.map mkVar idl))
     (thin idl)
 
-let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
+let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num =
 (*   observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
 (*   observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
 (*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
   let f_def = Global.lookup_constant (fst (destConst f)) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
-  let f_body = Option.get (Global.body_of_constant_body f_def)in
+  let f_body = Option.get (Global.body_of_constant_body f_def) in
   let params,f_body_with_params = decompose_lam_n nb_params f_body in
   let (_,num),(_,_,bodies) = destFix f_body_with_params in
   let fnames_with_params =
@@ -960,41 +962,48 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let f_body_with_params_and_other_fun  = substl fnames_with_params bodies.(num) in
 (*   observe (str "f_body_with_params_and_other_fun " ++  pr_lconstr f_body_with_params_and_other_fun); *)
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
-(*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
-  let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args)
-    (Typeops.type_of_constant_type (Global.env ()) (*FIXME*)f_def.const_type) in
+  (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
+  let (type_ctxt,type_of_f),evd =
+    let evd,t = Typing.e_type_of ~refresh:true (Global.env ()) evd f
+    in 
+    decompose_prod_n_assum
+      (nb_params + nb_args) t,evd
+  in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
+  (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *)
   let f_id = Label.to_id (con_label (fst (destConst f))) in
   let prove_replacement =
     tclTHENSEQ
       [
 	tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro);
-	(* observe_tac "" *) (fun g ->
+	observe_tac "" (fun g ->
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
-	     [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
-	      (* observe_tac "h_case" *) (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
+	     [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
+	      observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
 	      (Proofview.V82.of_tactic intros_reflexivity)] g
 	)
       ]
   in
+  (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
   Lemmas.start_proof
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
     (mk_equation_id f_id)
-    (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
-  Evd.empty
+    (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem))
+    evd
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
-  Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))
+  Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); 
+  evd
 
 
 
 
-let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
+let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
   let equation_lemma =
     try
       let finfos = find_Function_infos (fst (destConst f)) (*FIXME*) in
@@ -1005,7 +1014,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 	Ensures by: obvious
 	i*)
       let equation_lemma_id = (mk_equation_id f_id) in
-      generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
+      evd := generate_equation_lemma !evd all_funs  f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
       let _ =
 	match e with
 	  | Option.IsNone ->
@@ -1018,9 +1027,16 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 					 )
 		}
 	  | _ -> ()
-
       in
-      Constrintern.construct_reference (pf_hyps g) equation_lemma_id
+      (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
+      let evd',res =
+	Evd.fresh_global
+	  (Global.env ()) !evd
+	  (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
+      in
+      let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' res in 
+      evd:=evd';		       
+      res
   in
   let nb_intro_to_do = nb_prod (pf_concl g) in
     tclTHEN
@@ -1029,13 +1045,17 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 	fun g' ->
 	  let just_introduced = nLastDecls nb_intro_to_do g' in
 	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
-	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) (revert just_introduced_id) g'
+	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))
+		  (revert just_introduced_id) g'
       )
       g
 
-let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic =
+let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnames all_funs _nparams : tactic =
   fun g ->
-    let princ_type = pf_concl g in
+  let princ_type = pf_concl g in
+  (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
+  (* Pp.msgnl (str "all_funs "); *)
+  (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
     let princ_info = compute_elim_sig princ_type in
     let fresh_id =
       let avoid = ref (pf_ids_of_hyps g) in
@@ -1099,17 +1119,17 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	   f_body
 	)
     in
-(*     observe (str "full_params := " ++  *)
-(* 	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
-(* 	       full_params *)
-(* 	    );  *)
-(*     observe (str "princ_params := " ++  *)
-(* 	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
-(* 	       princ_params *)
-(* 	    );  *)
-(*     observe (str "fbody_with_full_params := " ++  *)
-(* 	       pr_lconstr fbody_with_full_params *)
-(* 	    );  *)
+    observe (str "full_params := " ++
+	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+	       full_params
+	    );
+    observe (str "princ_params := " ++
+	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+	       princ_params
+	    );
+    observe (str "fbody_with_full_params := " ++
+	       pr_lconstr fbody_with_full_params
+	    );
     let all_funs_with_full_params =
       Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
     in
@@ -1189,7 +1209,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		(List.rev princ_info.predicates)
 	    in
 	    pte_to_fix,List.rev rev_info
-	| _ -> Id.Map.empty,[]
+	| _ ->
+	   Id.Map.empty,[]
     in
     let mk_fixes : tactic =
       let pre_info,infos = list_chop fun_num infos in
@@ -1203,7 +1224,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    in
 	    if List.is_empty other_fix_infos
 	    then
-	      (* observe_tac ("h_fix") *) (fix (Some this_fix_info.name) (this_fix_info.idx +1))
+	      if this_fix_info.idx + 1 = 0
+	      then tclIDTAC (* Someone  tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
+	      else
+		observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (fix (Some this_fix_info.name) (this_fix_info.idx +1))
 	    else
 	      Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
 		other_fix_infos 0
@@ -1211,10 +1235,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
     in
     let first_tac : tactic = (* every operations until fix creations *)
       tclTHENSEQ
-	[ (* observe_tac "introducing params" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params));
-	  (* observe_tac "introducing predictes" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates));
-	  (* observe_tac "introducing branches" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches));
-	  (* observe_tac "building fixes" *) mk_fixes;
+	[ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params)));
+	  observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates)));
+	  observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches)));
+	  observe_tac "building fixes" mk_fixes;
 	]
     in
     let intros_after_fixes : tactic =
@@ -1248,8 +1272,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		 in
 		 tclTHENSEQ
 		   [
-(* 		     observe_tac "do_replace"  *)
-		       (do_replace
+		     observe_tac "do_replace"
+		       (do_replace evd
 			  full_params
 			  (fix_info.idx + List.length princ_params)
 			  (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params))
@@ -1257,9 +1281,6 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 			  fix_info.num_in_block
 			  all_funs
 		       );
-(* 		     observe_tac "do_replace"  *)
-(* 		       (do_replace princ_info.params fix_info.idx args_id *)
-(* 			  (List.hd (List.rev pte_args)) fix_body); *)
 		     let do_prove =
 		       build_proof
 			 interactive_proof
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index ff98f2b97f..61fce267a3 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -2,6 +2,7 @@ open Names
 open Term
 
 val prove_princ_for_struct :
+  Evd.evar_map ref ->
   bool ->
   int -> constant array -> constr array -> int -> Tacmach.tactic
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index deaf603ef0..45e5aaf545 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -105,7 +105,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let dummy_var = mkVar (Id.of_string "________") in
   let mk_replacement c i args =
     let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in
-(*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
+    observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res);
     res
   in
   let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
@@ -115,7 +115,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	    begin
 	      try match Environ.lookup_rel n env with
 		| _,_,t when is_dom t -> raise Toberemoved
-		| _ -> pre_princ,[] with Not_found -> assert false
+		| _ -> pre_princ,[]
+	      with Not_found -> assert false
 	    end
 	| Prod(x,t,b) ->
 	    compute_new_princ_type_for_binder remove mkProd env x t b
@@ -233,7 +234,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 
 
 
-let change_property_sort toSort princ princName =
+let change_property_sort evd toSort princ princName =
   let princ_info = compute_elim_sig princ in
   let change_sort_in_predicate (x,v,t) =
     (x,None,
@@ -243,47 +244,48 @@ let change_property_sort toSort princ princName =
        compose_prod args (mkSort toSort)
     )
   in
-  let princName_as_constr = Constrintern.global_reference princName in
+  let evd,princName_as_constr =
+    Evd.fresh_global
+      (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) in
   let init =
     let nargs =  (princ_info.nparams + (List.length  princ_info.predicates)) in
     mkApp(princName_as_constr,
 	  Array.init nargs
 	    (fun i -> mkRel (nargs - i )))
   in
-  it_mkLambda_or_LetIn
+  evd,  it_mkLambda_or_LetIn
     (it_mkLambda_or_LetIn init
        (List.map change_sort_in_predicate princ_info.predicates)
     )
     princ_info.params
 
-let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
+let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
   (*   let time1 = System.get_time ()  in *)
   let new_principle_type =
     compute_new_princ_type_from_rel
-      (Array.map mkConst funs)
+      (Array.map mkConstU funs)
       sorts
       old_princ_type
   in
   (*    let time2 = System.get_time ()  in *)
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
-     observe (str "new_principle_type : " ++ pr_lconstr new_principle_type);
   let new_princ_name =
     next_ident_away_in_goal (Id.of_string "___________princ_________") []
   in
+  let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
-    let evd,_ = Typing.e_type_of ~refresh:true (Global.env ()) Evd.empty new_principle_type in
     Lemmas.start_proof
       new_princ_name
-      (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
-      evd
-    new_principle_type
+      (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))
+      !evd
+      new_principle_type
       hook
-    ;
+  ;
     (*       let _tim1 = System.get_time ()  in *)
-    ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams)));
+      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map mkConstU funs) mutr_nparams)));
     (*       let _tim2 =  System.get_time ()  in *)
     (* 	begin *)
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
@@ -294,7 +296,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
 
 
 
-let generate_functional_principle
+let generate_functional_principle (evd: Evd.evar_map ref)
     interactive_proof
     old_princ_type sorts new_princ_name funs i proof_tac
     =
@@ -311,20 +313,23 @@ let generate_functional_principle
     match new_princ_name with
       | Some (id) -> id,id
       | None ->
-	  let id_of_f = Label.to_id (con_label f) in
+	  let id_of_f = Label.to_id (con_label (fst f)) in
 	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
   in
   let names = ref [new_princ_name] in
-  let hook new_principle_type _ _ =
+  let evd' = !evd in 
+  let hook =
+    fun  new_principle_type _ _  -> 
     if Option.is_empty sorts
     then
       (*     let id_of_f = Label.to_id (con_label f) in *)
       let register_with_sort fam_sort =
 	let s = Universes.new_sort_in_family fam_sort in
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
-	let value = change_property_sort s new_principle_type new_princ_name in
-	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce = Declare.definition_entry value in 
+	let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
+	let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in
+	(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+	let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in
 	ignore(
 	  Declare.declare_constant
 	    name
@@ -338,7 +343,7 @@ let generate_functional_principle
       register_with_sort InSet
   in
   let ((id,(entry,g_kind)),hook) =
-    build_functional_principle interactive_proof old_princ_type new_sorts funs i
+    build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
     proof_tac hook
   in
   (* Pr  1278 :
@@ -441,39 +446,37 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry list =
-  let env = Global.env ()
-  and sigma = Evd.empty in
+let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list =
+  let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
-
-
-  let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical first_fun) in
+  let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical (fst first_fun)) in
   let first_fun_kn =
     try
-      fst (find_Function_infos  first_fun).graph_ind
+      fst (find_Function_infos  (fst first_fun)).graph_ind
     with Not_found -> raise No_graph_found
   in
-  let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
-  let this_block_funs = Array.map fst this_block_funs_indexes in
+  let this_block_funs_indexes = get_funs_constant funs_mp funs_dp (fst first_fun) in
+  let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
   let prop_sort = InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
     List.map
-      (function cst -> List.assoc_f Constant.equal cst this_block_funs_indexes)
+      (function cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes)
       funs
   in
   let ind_list =
     List.map
       (fun (idx) ->
 	 let ind = first_fun_kn,idx in
-	   (ind,Univ.Instance.empty)(*FIXME*),true,prop_sort
+	   (ind,snd first_fun),true,prop_sort
       )
       funs_indexes
   in
   let sigma, schemes = 
-    Indrec.build_mutual_induction_scheme env sigma ind_list
+    Indrec.build_mutual_induction_scheme env !evd ind_list
   in
+  let _ = evd := sigma in 
   let l_schemes =
     List.map (Typing.type_of env sigma) schemes
   in
@@ -484,6 +487,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	     )
       fas
   in
+  evd:=sigma;
   (* We create the first priciple by tactic *)
   let first_type,other_princ_types =
     match l_schemes with
@@ -492,12 +496,12 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
   in
   let ((_,(const,_)),_) =
     try
-      build_functional_principle false
+      build_functional_principle evd false
 	first_type
 	(Array.of_list sorts)
 	this_block_funs
 	0
-	(prove_princ_for_struct false 0 (Array.of_list funs))
+	(prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
 	(fun _ _ _ -> ())
     with e when Errors.noncritical e ->
        begin
@@ -519,7 +523,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
   in
   incr i;
   let opacity =
-    let finfos = find_Function_infos first_fun in
+    let finfos = find_Function_infos (fst first_fun) in
     try
       let equation =  Option.get finfos.equation_lemma in
       Declareops.is_opaque (Global.lookup_constant equation)
@@ -533,7 +537,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
     [const]
   else
     let other_fun_princ_types =
-      let funs = Array.map mkConst this_block_funs in
+      let funs = Array.map mkConstU this_block_funs in
       let sorts = Array.of_list sorts in
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
@@ -566,12 +570,13 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	   *)
 	     let ((_,(const,_)),_) =
 	       build_functional_principle
+		 evd
 		 false
 		 (List.nth other_princ_types (!i - 1))
 		 (Array.of_list sorts)
 		 this_block_funs
 		 !i
-		 (prove_princ_for_struct false !i (Array.of_list funs))
+		 (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
 		 (fun _ _ _ -> ())
 	     in
 	     const
@@ -589,24 +594,27 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
     in
     const::other_result
 
+	   
 let build_scheme fas =
   Dumpglob.pause ();
-  let bodies_types =
-    make_scheme
-      (List.map
+  let evd = (ref Evd.empty) in
+  let pconstants = (List.map
 	 (fun (_,f,sort) ->
 	    let f_as_constant =
 	      try
-		match Smartlocate.global_with_alias f with
-		  | Globnames.ConstRef c -> c
-		  | _ -> Errors.error "Functional Scheme can only be used with functions"
+		Smartlocate.global_with_alias f
 	      with Not_found ->
 	      	Errors.error ("Cannot find "^ Libnames.string_of_reference f)
 	    in
-	    (f_as_constant,sort)
+	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
+	    let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in 
+	    let _ = evd := evd' in 
+	    (destConst f,sort)
 	 )
 	 fas
-      )
+		   ) in
+  let bodies_types =
+    make_scheme evd pconstants      
   in
   List.iter2
     (fun (princ_id,_,_) def_entry ->
@@ -633,14 +641,10 @@ let build_case_scheme fa =
 		 with Not_found ->
 		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
   let first_fun,u = destConst  funs in
-
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
-
-
-
   let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
-  let this_block_funs = Array.map fst this_block_funs_indexes in
+  let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
   let prop_sort = InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
@@ -666,12 +670,15 @@ let build_case_scheme fa =
 	    );
   *)
     generate_functional_principle
+      (ref Evd.empty)
       false
       scheme_type
       (Some ([|sorts|]))
       (Some princ_name)
       this_block_funs
       0
-      (prove_princ_for_struct false 0 [|fst (destConst funs)|])
+      (prove_princ_for_struct (ref Evd.empty) false 0 [|fst (destConst funs)|])
   in
   ()
+ 
+
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index a16b834f89..f6e5578d2e 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -3,6 +3,7 @@ open Term
 open Misctypes
 
 val generate_functional_principle :
+  Evd.evar_map ref -> 
   (* do we accept interactive proving *)
   bool ->
   (* induction principle on rel *)
@@ -12,7 +13,7 @@ val generate_functional_principle :
   (* Name of the new principle *)
   (Id.t) option ->
   (* the compute functions to use   *)
-  constant array ->
+  pconstant array ->
   (* We prove the nth- principle *)
   int  ->
   (* The tactic to use to make the proof w.r
@@ -27,7 +28,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
 
 exception No_graph_found
 
-val make_scheme : (constant*glob_sort) list -> Entries.definition_entry list
+val make_scheme :   Evd.evar_map ref ->
+ (pconstant*glob_sort) list -> Entries.definition_entry list
 
 val build_scheme : (Id.t*Libnames.reference*glob_sort) list ->  unit
 val build_case_scheme : (Id.t*Libnames.reference*glob_sort)  ->  unit
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index fd48ab59fb..043d4328c4 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -217,7 +217,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 		    begin
 		      make_graph (Smartlocate.global_with_alias fun_name)
 		    end
-		    ;
+		  ;
 		    try Functional_principles_types.build_scheme fas
 		    with Functional_principles_types.No_graph_found ->
 		      Errors.error ("Cannot generate induction principle(s)")
@@ -386,7 +386,9 @@ let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
     (nexttac:Proof_type.tactic) g =
   let test = match oid with
     | Some id ->
-	let idconstr = mkConst (const_of_id id) in
+       let idref = const_of_id id in
+       (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *)
+       let idconstr = snd (Evd.fresh_global (Global.env ()) Evd.empty idref) in
 	(fun u -> constr_head_match u idconstr) (* select only id *)
     | None -> (fun u -> isApp u) in (* select calls to any function *)
   let info_list = find_fapp test g in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index f6a543a1c6..9e3f398633 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1233,11 +1233,11 @@ let rec rebuild_return_type rt =
 
 
 let do_build_inductive
-      mp_dp
-      funnames (funsargs: (Name.t * glob_constr * bool) list list)
+      evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * bool) list list)
       returned_types
       (rtl:glob_constr list) =
   let _time1 = System.get_time () in
+  let funnames = List.map (fun c -> Label.to_id (KerName.label (Constant.canonical (fst c)))) funconstants in
   (*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
   let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in
   let funnames = Array.of_list funnames in
@@ -1252,23 +1252,21 @@ let do_build_inductive
   let relnames = Array.map mk_rel_id funnames in
   let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in
   (* Construction of the pseudo constructors *)
-  let env =
-    Array.fold_right
-      (fun id env ->
-       let c =
-	 match mp_dp with
-	 | None -> (Constrintern.global_reference id)
-	 | Some(mp,dp) -> mkConst (make_con mp dp (Label.of_id id))
-       in
-       Environ.push_named (id,None,
-			   try
-			     Typing.type_of env Evd.empty c
-			   with Not_found ->
-			     raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint"))
-			  )  env
+  let evd,env =
+    Array.fold_right2
+      (fun id c (evd,env) ->
+       let evd,t = Typing.e_type_of env evd (mkConstU c) in
+       evd,
+       Environ.push_named (id,None,t)
+			   (* try *)
+			   (*   Typing.e_type_of env evd (mkConstU c) *)
+			   (* with Not_found -> *)
+			   (*   raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint")) *)
+			 env
       )
       funnames
-      (Global.env ())
+      (Array.of_list funconstants)
+      (evd,Global.env ())
   in
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
@@ -1426,7 +1424,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) Decl_kinds.Finite
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
@@ -1461,9 +1459,9 @@ let do_build_inductive
 
 
 
-let build_inductive mp_dp funnames funsargs returned_types rtl =
+let build_inductive evd funconstants funsargs returned_types rtl =
   try
-    do_build_inductive mp_dp funnames funsargs returned_types rtl
+    do_build_inductive evd funconstants funsargs returned_types rtl
   with e when Errors.noncritical e -> raise (Building_graph e)
 
 
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index b0a05ec322..5bb1376e26 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -7,8 +7,11 @@ open Names
 *)
 
 val build_inductive :
-  (ModPath.t * DirPath.t) option ->
-  Id.t list -> (* The list of function name *)
+(*  (ModPath.t * DirPath.t) option ->
+  Id.t list -> (* The list of function name *) 
+ *)
+  Evd.evar_map ->
+  Term.pconstant list -> 
   (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2730fd421a..e211b68837 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -28,48 +28,55 @@ let choose_dest_or_ind scheme_info =
 
 let functional_induction with_clean c princl pat =
   Dumpglob.pause ();
-  let res = let f,args = decompose_app c in
-	      fun g ->
-		let princ,bindings, princ_type =
-		  match princl with
-	| None -> (* No principle is given let's find the good one *)
-	    begin
-	      match kind_of_term f with
-		| Const (c',u) ->
-		    let princ_option =
-		      let finfo = (* we first try to find out a graph on f *)
-			try find_Function_infos c'
-			with Not_found ->
-			  errorlabstrm "" (str "Cannot find induction information on "++
-					     Printer.pr_lconstr (mkConst c') )
-		      in
-		      match Tacticals.elimination_sort_of_goal g with
-			| InProp -> finfo.prop_lemma
-			| InSet -> finfo.rec_lemma
-			| InType -> finfo.rect_lemma
-		    in
-		    let princ =  (* then we get the principle *)
-		      try mkConst (Option.get princ_option )
-		      with Option.IsNone ->
-			(*i If there is not default lemma defined then,
+  let res =
+    let f,args = decompose_app c in
+    fun g ->
+    let princ,bindings, princ_type,g' =
+      match princl with
+      | None -> (* No principle is given let's find the good one *)
+	 begin
+	   match kind_of_term f with
+	   | Const (c',u) ->
+	      let princ_option =
+		let finfo = (* we first try to find out a graph on f *)
+		  try find_Function_infos c'
+		  with Not_found ->
+		    errorlabstrm "" (str "Cannot find induction information on "++
+				       Printer.pr_lconstr (mkConst c') )
+		in
+		match Tacticals.elimination_sort_of_goal g with
+		| InProp -> finfo.prop_lemma
+		| InSet -> finfo.rec_lemma
+		| InType -> finfo.rect_lemma
+	      in
+	      let princ,g' =  (* then we get the principle *)
+		try
+		  let g',princ =
+		    Tacmach.pf_eapply (Evd.fresh_global) g  (Globnames.ConstRef (Option.get princ_option )) in
+		  princ,g'
+		with Option.IsNone ->
+		  (*i If there is not default lemma defined then,
 			  we cross our finger and try to find a lemma named f_ind
 			  (or f_rec, f_rect) i*)
-			let princ_name =
-			  Indrec.make_elimination_ident
-			    (Label.to_id (con_label c'))
-			    (Tacticals.elimination_sort_of_goal g)
-			in
-			try
-			  mkConst(const_of_id princ_name )
-			with Not_found -> (* This one is neither defined ! *)
-			  errorlabstrm "" (str "Cannot find induction principle for "
-					   ++Printer.pr_lconstr (mkConst c') )
-		    in
-		    (princ,NoBindings, Tacmach.pf_type_of g princ)
-		| _ -> raise (UserError("",str "functional induction must be used with a function" ))
-	    end
-	| Some ((princ,binding)) ->
-	    princ,binding,Tacmach.pf_type_of g princ
+		  let princ_name =
+		    Indrec.make_elimination_ident
+		      (Label.to_id (con_label c'))
+		      (Tacticals.elimination_sort_of_goal g)
+		  in
+		  try
+		    let princ_ref = const_of_id princ_name in
+		    let (a,b) = Tacmach.pf_eapply (Evd.fresh_global) g princ_ref in
+		    (b,a)
+		    (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
+		  with Not_found -> (* This one is neither defined ! *)
+		    errorlabstrm "" (str "Cannot find induction principle for "
+				     ++Printer.pr_lconstr (mkConst c') )
+	      in
+	      (princ,NoBindings, Tacmach.pf_type_of g' princ,g')
+	   | _ -> raise (UserError("",str "functional induction must be used with a function" ))
+	 end
+      | Some ((princ,binding)) ->
+	 princ,binding,Tacmach.pf_type_of g princ,g
     in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     let args_as_induction_constr =
@@ -115,7 +122,7 @@ let functional_induction with_clean c princl pat =
 	 princ_infos
 	 (args_as_induction_constr,princ')))
       subst_and_reduce
-      g
+      g'
   in
     Dumpglob.continue ();
     res
@@ -221,34 +228,54 @@ let process_vernac_interp_error e =
 
 let derive_inversion fix_names =
   try
+    let evd' = Evd.empty in 
     (* we first transform the fix_names identifier into their corresponding constant *)
-    let fix_names_as_constant =
-      List.map (fun id -> fst (destConst (Constrintern.global_reference id))) fix_names
+    let evd',fix_names_as_constant =
+      List.fold_right
+	(fun id (evd,l) ->
+	 let evd,c =
+	   Evd.fresh_global
+	     (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in 
+	 evd, destConst c::l
+	)
+	fix_names
+	(evd',[])
     in
     (*
        Then we check that the graphs have been defined
        If one of the graphs haven't been defined
        we do nothing
     *)
-    List.iter (fun c -> ignore (find_Function_infos c)) fix_names_as_constant ;
+    List.iter (fun c -> ignore (find_Function_infos (fst c))) fix_names_as_constant ;
     try
+      let evd', lind =
+	List.fold_right
+	  (fun id (evd,l) ->
+	   let evd,id = 
+	     Evd.fresh_global
+	       (Global.env ()) evd
+	       (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id)))
+	   in 
+	   evd,(fst (destInd id))::l
+	  )
+	  fix_names
+	  (evd',[])
+      in
       Invfun.derive_correctness
 	Functional_principles_types.make_scheme
 	functional_induction
 	fix_names_as_constant
-	(*i The next call to mk_rel_id is valid since we have just construct the graph
-	  Ensures by : register_built
-	  i*)
-	(List.map
-	   (fun id -> fst (destInd (Constrintern.global_reference (mk_rel_id id))))
-	   fix_names
-	)
-    with e when Errors.noncritical e ->
+	lind;
+      with e when Errors.noncritical e ->
       let e' = process_vernac_interp_error e in
       msg_warning
 	(str "Cannot build inversion information" ++
 	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
-  with e when Errors.noncritical e -> ()
+  with e when Errors.noncritical e ->
+      let e' = process_vernac_interp_error e in
+      msg_warning
+	(str "Cannot build inversion information (early)" ++
+	   if do_observe () then (fnl() ++ Errors.print e') else mt ())       
 
 let warning_error names e =
   let e = process_vernac_interp_error e in
@@ -292,7 +319,7 @@ let error_error names e =
 	     e_explain e)
     | _ -> raise e
 
-let generate_principle  mp_dp on_error
+let generate_principle (evd:Evd.evar_map ref) pconstants on_error
     is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
     (continue_proof : int -> Names.constant array -> Term.constr array -> int ->
       Tacmach.tactic) : unit =
@@ -302,7 +329,7 @@ let generate_principle  mp_dp on_error
   let funs_types =  List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
   try
     (* We then register the Inductive graphs of the functions  *)
-    Glob_term_to_relation.build_inductive mp_dp names funs_args funs_types recdefs;
+    Glob_term_to_relation.build_inductive !evd pconstants funs_args funs_types recdefs;
     if do_built
     then
       begin
@@ -327,14 +354,18 @@ let generate_principle  mp_dp on_error
 	let _ =
 	  List.map_i
 	    (fun i x ->
-	       let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
-	       let princ_type = Global.type_of_global_unsafe princ in
-	       Functional_principles_types.generate_functional_principle
+	     let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
+	     let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in
+	     let evd',princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd' uprinc in
+	     let _ = evd := evd' in 
+    	     Functional_principles_types.generate_functional_principle
+	       evd
 		 interactive_proof
 		 princ_type
 		 None
 		 None
-		 funs_kn
+		 (Array.of_list pconstants)
+		 (* funs_kn *)
 		 i
 		 (continue_proof  0 [|funs_kn.(i)|])
 	    )
@@ -351,10 +382,37 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
   match fixpoint_exprl with
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
-	Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition)
-	  bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()))
+      Command.do_definition
+	fname
+	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition)
+	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
+       let evd,rev_pconstants =
+	 List.fold_left
+	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+	    let evd,c =
+	      Evd.fresh_global
+		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
+	    evd,((destConst c)::l)
+	   )
+	   (Evd.empty,[])
+	   fixpoint_exprl
+       in
+       evd,List.rev rev_pconstants
     | _ ->
-	Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl
+       Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       let evd,rev_pconstants =
+	 List.fold_left
+	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+	    let evd,c =
+	      Evd.fresh_global
+		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
+	    evd,((destConst c)::l)
+	   )
+	   (Evd.empty,[])
+	   fixpoint_exprl
+       in
+       evd,List.rev rev_pconstants
+	   
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
@@ -399,10 +457,10 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
-  let hook (f_ref,_) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
+  let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
       nb_args relation =
     try
-      pre_hook
+      pre_hook [fconst]
 	(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
 	   functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
 	);
@@ -550,7 +608,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   fixpoint_exprl_with_new_bl
   
 
-let do_generate_principle mp_dp on_error register_built interactive_proof
+let do_generate_principle pconstants on_error register_built interactive_proof
     (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) :unit =
   List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
   let _is_struct =
@@ -565,9 +623,10 @@ let do_generate_principle mp_dp on_error register_built interactive_proof
 	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in 
-	  let pre_hook =
+	  let pre_hook pconstants =
 	    generate_principle
-	      mp_dp
+	      (ref (Evd.empty))
+	      pconstants
 	      on_error
 	      true
 	      register_built
@@ -588,9 +647,10 @@ let do_generate_principle mp_dp on_error register_built interactive_proof
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in
 	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
-	  let pre_hook =
+	  let pre_hook pconstants =
 	    generate_principle
-	      mp_dp
+	      (ref Evd.empty)
+	      pconstants
 	      on_error
 	      true
 	      register_built
@@ -614,20 +674,26 @@ let do_generate_principle mp_dp on_error register_built interactive_proof
 	let fix_names =
 	  List.map (function (((_,name),_,_,_,_),_) -> name) fixpoint_exprl
 	in
-	  (* ok all the expressions are structural *)
+	(* ok all the expressions are structural *)
   	let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	let is_rec = List.exists (is_rec fix_names) recdefs in
-	if register_built then register_struct is_rec fixpoint_exprl;
+	let evd,pconstants =
+	  if register_built
+	  then register_struct is_rec fixpoint_exprl
+	  else (Evd.empty,pconstants)
+	in
+	let evd = ref evd in 
 	generate_principle
-	  mp_dp
+	  (ref !evd)
+	  pconstants
 	  on_error
 	  false
 	  register_built
 	  fixpoint_exprl
 	  recdefs
 	  interactive_proof
-	  (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
-	if register_built then derive_inversion fix_names;
+	  (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof);
+	if register_built then begin derive_inversion fix_names; end;
 	true; 
   in
   ()
@@ -773,7 +839,7 @@ let make_graph (f_ref:global_reference) =
 	   with_full_print (fun () ->
 		(Constrextern.extern_constr false env Evd.empty body,
 		 Constrextern.extern_type false env Evd.empty
-                   ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type)
+                   ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type)
 		)
 	     )
 	     ()
@@ -811,13 +877,13 @@ let make_graph (f_ref:global_reference) =
 		 [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
 	 let mp,dp,_ = repr_con c in
-	 do_generate_principle (Some (mp,dp)) error_error  false false expr_list;
+	 do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list;
 	 (* We register the infos *)
 	 List.iter
 	   (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
 	   expr_list);
   Dumpglob.continue ()
 
-let do_generate_principle = do_generate_principle None warning_error true
+let do_generate_principle = do_generate_principle [] warning_error true
 
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 76f8c6d219..738ade8ca3 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -108,7 +108,7 @@ let const_of_id id =
   let _,princ_ref =
     qualid_of_reference (Libnames.Ident (Loc.ghost,id))
   in
-  try Nametab.locate_constant princ_ref
+  try Constrintern.locate_reference princ_ref
   with Not_found -> Errors.error ("cannot find "^ Id.to_string id)
 
 let def_of_const t =
@@ -380,9 +380,9 @@ let find_Function_of_graph ind =
   Indmap.find ind !from_graph
 
 let update_Function finfo =
-(*   Pp.msgnl (pr_info finfo); *)
+  (* Pp.msgnl (pr_info finfo); *)
   Lib.add_anonymous_leaf (in_Function finfo)
-
+			 
 
 let add_Function is_general f =
   let f_id = Label.to_id (con_label f) in
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 67ddf3741f..10daf6e848 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -42,7 +42,7 @@ val chop_rprod_n : int -> Glob_term.glob_constr ->
 val def_of_const : Term.constr -> Term.constr
 val eq : Term.constr Lazy.t
 val refl_equal : Term.constr Lazy.t
-val const_of_id: Id.t -> constant
+val const_of_id: Id.t ->  Globnames.global_reference(* constantyes *)
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0ee8877082..d9ae87ecc1 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -70,7 +70,7 @@ let do_observe_tac s tac g =
   with reraise ->
     let reraise = Errors.push reraise in
     let e = Cerrors.process_vernac_interp_error reraise in
-    msgnl (str "observation "++ s++str " raised exception " ++
+    observe (str "observation "++ s++str " raised exception " ++
 	     Errors.iprint e ++ str " on goal " ++ goal );
     iraise reraise;;
 
@@ -92,13 +92,24 @@ let nf_zeta =
     Evd.empty
 
 
-(* [id_to_constr id] finds the term associated to [id] in the global environment *)
-let id_to_constr id =
+(* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *)
+(* let id_to_constr id = *)
+(*   try *)
+(*     Constrintern.global_reference id *)
+(*   with Not_found -> *)
+(*     raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) *)
+
+
+let make_eq () =
   try
-    Constrintern.global_reference id
-  with Not_found ->
-    raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id))
+    Universes.constr_of_global (Coqlib.build_coq_eq ())
+  with _ -> assert false 
+let make_eq_refl () =
+  try
+    Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
+  with _ -> assert false
 
+	  
 (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
    (resp. g_to_f = false) where [graph]  is the graph of [f] and is the [i]th function in the block.
 
@@ -111,11 +122,13 @@ let id_to_constr id =
    res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion
  *)
 
-let generate_type g_to_f f graph i =
+let generate_type evd g_to_f f graph i =
   (*i we deduce the number of arguments of the function and its returned type from the graph i*)
-  let gr,u = destInd graph in
-  let graph_arity = Inductive.type_of_inductive (Global.env()) 
-    (Global.lookup_inductive gr, u) in
+  let evd',graph =
+    Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd graph)))
+  in
+  let evd',graph_arity = Typing.e_type_of (Global.env ()) evd' graph in
+  evd:=evd';
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -141,11 +154,10 @@ let generate_type g_to_f f graph i =
     the hypothesis [res = fv] can then be computed
     We will need to lift it by one in order to use it as a conclusion
     i*)
-  let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+  let make_eq = make_eq ()
   in
   let res_eq_f_of_args =
-    mkApp(make_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|])
+    mkApp(make_eq ,[|lift 2 res_type;mkRel 1;mkRel 2|])
   in
   (*i
     The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed
@@ -158,12 +170,12 @@ let generate_type g_to_f f graph i =
     \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,  \]
     i*)
   let pre_ctxt =
-    (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(mkConst f,args_as_rels)),res_type)::fun_ctxt
+    (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(f,args_as_rels)),res_type)::fun_ctxt
   in
   (*i and we can return the solution depending on which lemma type we are defining i*)
   if g_to_f
-  then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args)
-  else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied)
+  then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
+  else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
 
 
 (*
@@ -171,7 +183,7 @@ let generate_type g_to_f f graph i =
 
    WARNING: while convertible, [type_of body] and [type] can be non equal
 *)
-let find_induction_principle f =
+let find_induction_principle evd f =
   let f_as_constant,u =  match kind_of_term f with
     | Const c' -> c'
     | _ -> error "Must be used with a function"
@@ -180,28 +192,10 @@ let find_induction_principle f =
   match infos.rect_lemma with
     | None -> raise Not_found
     | Some rect_lemma ->
-	let rect_lemma = mkConst rect_lemma in
-	let typ = Typing.type_of (Global.env ()) Evd.empty rect_lemma in
-	rect_lemma,typ
-
-
-
-(*     let fname =  *)
-(*       match kind_of_term f with  *)
-(* 	| Const c' ->  *)
-(* 	    Label.to_id (con_label c')  *)
-(* 	| _ -> error "Must be used with a function"  *)
-(*     in *)
-
-(*     let princ_name =  *)
-(*       ( *)
-(* 	Indrec.make_elimination_ident *)
-(* 	  fname *)
-(* 	  InType *)
-(*       ) *)
-(*     in *)
-(*     let c = (\* mkConst(mk_from_const (destConst f) princ_name ) in  *\) failwith "" in  *)
-(*     c,Typing.type_of (Global.env ()) Evd.empty c *)
+       let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
+       let evd',typ = Typing.e_type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+       evd:=evd';
+       rect_lemma,typ
 
 
 let rec generate_fresh_id x avoid i =
@@ -211,11 +205,6 @@ let rec generate_fresh_id x avoid i =
     let id = Namegen.next_ident_away_in_goal x avoid in
     id::(generate_fresh_id x (id::avoid) (pred i))
 
-let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
-let make_eq_refl () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
-
 
 (* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ]
    is the tactic used to prove correctness lemma.
@@ -241,7 +230,7 @@ let make_eq_refl () =
    \end{enumerate}
 
 *)
-let prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic =
+let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic =
   fun g ->
     (* first of all we recreate the lemmas types to be used as predicates of the induction principle
        that is~:
@@ -286,46 +275,6 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     (* The tactic to prove the ith branch of the principle *)
     let prove_branche i g =
       (* We get the identifiers of this branch *)
-      (*
-	let this_branche_ids =
-	List.fold_right
-	(fun (_,pat) acc ->
-	     match pat with
-	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
-	| _ -> anomaly (Pp.str "Not an identifier")
-	)
-	(List.nth intro_pats (pred i))
-	Id.Set.empty
-      in
-	let pre_args g =
-	List.fold_right
-	  (fun (id,b,t) pre_args ->
-	    if Id.Set.mem id this_branche_ids
-	    then
-	      match b with
-		| None -> id::pre_args
-		| Some b -> pre_args
-	    else pre_args
-	  )
-	  (pf_hyps g)
-	  ([])
-      in
-      let pre_args g = List.rev (pre_args g) in 
-      let pre_tac g =
-	List.fold_right
-	  (fun (id,b,t) pre_tac ->
-	     if Id.Set.mem id this_branche_ids
-	     then
-	       match b with
-		 | None -> pre_tac
-		 | Some b ->
-		   tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac
-	     else pre_tac
-	  )
-	  (pf_hyps g)
-	  tclIDTAC
-      in
-*)     
       let pre_args =
       	List.fold_right
       	  (fun (_,pat) acc ->
@@ -345,7 +294,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	 If [hid] has another type the corresponding argument of the constructor is [hid]
       *)
       let constructor_args g =
-	List.fold_right
+	List.fold_right 
 	  (fun hid acc ->
 	     let type_of_hid = pf_type_of g (mkVar hid) in
 	     match kind_of_term type_of_hid with
@@ -358,7 +307,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 			       | App(eq,args), App(graph',_)
 				   when
 				     (eq_constr eq eq_ind) &&
-				       Array.exists  (eq_constr graph') graphs_constr ->
+				       Array.exists  (Constr.eq_constr_nounivs graph') graphs_constr ->
 				   (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
 				    ::acc)
 			       | _ -> mkVar hid ::  acc
@@ -395,7 +344,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	  end
       in
       (* we can then build the final proof term *)
-      let app_constructor g = applist((mkConstruct(constructor)),constructor_args g) in
+      let app_constructor g = applist((mkConstructU(constructor,u)),constructor_args g) in
       (* an apply the tactic *)
       let res,hres =
 	match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with
@@ -428,7 +377,9 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    (* replacing [res] with its value *)
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
-	    observe_tac "exact" (fun g -> Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
+	    observe_tac "exact" (fun g ->
+				 Pp.msgnl (str "TITI " ++ pf_apply Printer.pr_lconstr_env g (app_constructor g));
+				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
 	  ]
       )
 	g
@@ -436,13 +387,15 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     (* end of branche proof *)
     let lemmas =
       Array.map
-	(fun (_,(ctxt,concl)) ->
+	(fun ((_,(ctxt,concl))) ->
 	   match ctxt with
 	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
 	     | hres::res::(x,_,t)::ctxt ->
-		 Termops.it_mkLambda_or_LetIn
-		   (Termops.it_mkProd_or_LetIn concl [hres;res])
-		   ((x,None,t)::ctxt)
+		let res = Termops.it_mkLambda_or_LetIn
+			    (Termops.it_mkProd_or_LetIn concl [hres;res])
+			    ((x,None,t)::ctxt)
+		in
+		res
 	)
 	lemmas_types_infos
     in
@@ -457,7 +410,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (*(Loc.ghost,Glob_term.NamedHyp id,p)*)p::bindings,id::avoid
+	     p::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
 	  princ_infos.params
@@ -467,13 +420,14 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (*(Loc.ghost,Glob_term.NamedHyp id,(nf_zeta p))*) (nf_zeta p)::bindings,id::avoid)
+	     (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
       in
-      (* Glob_term.ExplicitBindings *) (params_bindings@lemmas_bindings)
+      (params_bindings@lemmas_bindings)
     in
+    Pp.msgnl (str "princ_type := " ++ pf_apply Printer.pr_lconstr_env g princ_type);
     tclTHENSEQ
       [ 
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
@@ -484,10 +438,11 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
 	tclTHEN_i
-	  (observe_tac "functional_induction" (
-	    (fun gl -> 
-	      let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-	      let gl', _ty = pf_eapply Typing.e_type_of gl term in
+	  (observe_tac
+	     "functional_induction" (
+	       (fun gl ->
+		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
+		let gl', _ty = pf_eapply (Typing.e_type_of ~refresh:true)  gl term in
 		Proofview.V82.of_tactic (apply term) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
@@ -495,230 +450,6 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       g
 
 
-(*
-let prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic =
-  fun g ->
-    (* first of all we recreate the lemmas types to be used as predicates of the induction principle
-       that is~:
-       \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun  fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
-    *)
-    let lemmas =
-      Array.map
-	(fun (_,(ctxt,concl)) ->
-	   match ctxt with
-	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
-	     | hres::res::(x,_,t)::ctxt ->
-		 Termops.it_mkLambda_or_LetIn
-		   (Termops.it_mkProd_or_LetIn concl [hres;res])
-		   ((x,None,t)::ctxt)
-	)
-	lemmas_types_infos
-    in
-    (* we the get the definition of the graphs block *)
-    let graph_ind = destInd graphs_constr.(i) in
-    let kn = fst graph_ind in
-    let mib,_ = Global.lookup_inductive graph_ind in
-    (* and the principle to use in this lemma in $\zeta$ normal form *)
-    let f_principle,princ_type = schemes.(i) in
-    let princ_type =  nf_zeta princ_type in
-    let princ_infos = Tactics.compute_elim_sig princ_type in
-    (* The number of args of the function is then easily computable *)
-    let nb_fun_args = nb_prod (pf_concl g)  - 2  in
-    let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
-    let ids = args_names@(pf_ids_of_hyps g) in
-    (* Since we cannot ensure that the functional principle is defined in the
-       environment and due to the bug #1174, we will need to pose the principle
-       using a name
-    *)
-    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
-    let ids = principle_id :: ids in
-    (* We get the branches of the principle *)
-    let branches = List.rev princ_infos.branches in
-    (* and built the intro pattern for each of them *)
-    let intro_pats =
-      List.map
-	(fun (_,_,br_type) ->
-	   List.map
-	     (fun id -> Loc.ghost, Genarg.IntroIdentifier id)
-	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
-	)
-	branches
-    in
-    (* before building the full intro pattern for the principle *)
-    let pat = Some (Loc.ghost,Genarg.IntroOrAndPattern intro_pats) in
-    let eq_ind = Coqlib.build_coq_eq () in
-    let eq_construct = mkConstruct((destInd eq_ind),1) in
-    (* The next to referencies will be used to find out which constructor to apply in each branch *)
-    let ind_number = ref 0
-    and min_constr_number = ref 0 in
-    (* The tactic to prove the ith branch of the principle *)
-    let prove_branche i g =
-      (* We get the identifiers of this branch *)
-      let this_branche_ids =
-	List.fold_right
-	  (fun (_,pat) acc ->
-	     match pat with
-	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
-	       | _ -> anomaly (Pp.str "Not an identifier")
-	  )
-	  (List.nth intro_pats (pred i))
-	  Id.Set.empty
-      in
-      (* and get the real args of the branch by unfolding the defined constant *)
-      let pre_args,pre_tac =
-	List.fold_right
-	  (fun (id,b,t) (pre_args,pre_tac) ->
-	     if Id.Set.mem id this_branche_ids
-	     then
-	       match b with
-		 | None -> (id::pre_args,pre_tac)
-		 | Some b ->
-		     (pre_args,
-		      tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac
-		     )
-	     else (pre_args,pre_tac)
-	  )
-	  (pf_hyps g)
-	  ([],tclIDTAC)
-      in
-      (*
-	 We can then recompute the arguments of the constructor.
-	 For each [hid] introduced by this branch, if [hid] has type
-	 $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are
-	 [ fv (hid fv (refl_equal fv)) ].
-	 If [hid] has another type the corresponding argument of the constructor is [hid]
-      *)
-      let constructor_args =
-	List.fold_right
-	  (fun hid acc ->
-	     let type_of_hid = pf_type_of g (mkVar hid) in
-	     match kind_of_term type_of_hid with
-	       | Prod(_,_,t') ->
-		   begin
-		     match kind_of_term t' with
-		       | Prod(_,t'',t''') ->
-			   begin
-			     match kind_of_term t'',kind_of_term t''' with
-			       | App(eq,args), App(graph',_)
-				   when
-				     (eq_constr eq eq_ind) &&
-				       Array.exists  (eq_constr graph') graphs_constr ->
-				   ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
-				    ::args.(2)::acc)
-			       | _ -> mkVar hid ::  acc
-			   end
-		       | _ -> mkVar hid :: acc
-		   end
-	       | _ -> mkVar hid :: acc
-	  ) pre_args []
-      in
-      (* in fact we must also add the parameters to the constructor args *)
-      let constructor_args =
-	let params_id = fst (List.chop princ_infos.nparams args_names) in
-	(List.map mkVar params_id)@(List.rev constructor_args)
-      in
-      (* We then get the constructor corresponding to this branch and
-	 modifies the references has needed i.e.
-	 if the constructor is the last one of the current inductive then
-	 add one the number of the inductive to take and add the number of constructor of the previous
-	 graph to the minimal constructor number
-      *)
-      let constructor =
-	let constructor_num = i - !min_constr_number in
-	let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in
-	if constructor_num <= length
-	then
-	  begin
-	    (kn,!ind_number),constructor_num
-	  end
-	else
-	  begin
-	    incr ind_number;
-	    min_constr_number := !min_constr_number + length ;
-	    (kn,!ind_number),1
-	  end
-      in
-      (* we can then build the final proof term *)
-      let app_constructor = applist((mkConstruct(constructor)),constructor_args) in
-      (* an apply the tactic *)
-      let res,hres =
-	match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with
-	  | [res;hres] -> res,hres
-	  | _ -> assert false
-      in
-      observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor);
-      (
-	tclTHENSEQ
-	  [
-	    (* unfolding of all the defined variables introduced by this branch *)
-	    observe_tac "unfolding" pre_tac;
-	    (* $zeta$ normalizing of the conclusion *)
-	    h_reduce
-	      (Glob_term.Cbv
-		 { Glob_term.all_flags with
-		     Glob_term.rDelta = false ;
-		     Glob_term.rConst = []
-		 }
-	      )
-	      onConcl;
-	    (* introducing the the result of the graph and the equality hypothesis *)
-	    observe_tac "introducing" (tclMAP h_intro [res;hres]);
-	    (* replacing [res] with its value *)
-	    observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres));
-	    (* Conclusion *)
-	    observe_tac "exact" (exact_check app_constructor)
-	  ]
-      )
-	g
-    in
-    (* end of branche proof *)
-    let param_names = fst (List.chop princ_infos.nparams args_names) in
-    let params = List.map mkVar param_names in
-    let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
-    (* The bindings of the principle
-       that is the params of the principle and the different lemma types
-    *)
-    let bindings =
-      let params_bindings,avoid =
-	List.fold_left2
-	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (Loc.ghost,Glob_term.NamedHyp id,p)::bindings,id::avoid
-	  )
-	  ([],pf_ids_of_hyps g)
-	  princ_infos.params
-	  (List.rev params)
-      in
-      let lemmas_bindings =
-	List.rev (fst  (List.fold_left2
-	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (Loc.ghost,Glob_term.NamedHyp id,(nf_zeta p))::bindings,id::avoid)
-	  ([],avoid)
-	  princ_infos.predicates
-	  (lemmas)))
-      in
-      Glob_term.ExplicitBindings (params_bindings@lemmas_bindings)
-    in
-    tclTHENSEQ
-      [ observe_tac "intro args_names" (tclMAP h_intro args_names);
-	observe_tac "principle" (assert_by
-	  (Name principle_id)
-	  princ_type
-	  (exact_check f_principle));
-	tclTHEN_i
-	  (observe_tac "functional_induction" (
-	     fun g ->
-	       observe
-		 (pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g))  (mkVar principle_id,bindings));
-	       functional_induction  false (applist(funs_constr.(i),List.map mkVar args_names))
-		 (Some (mkVar principle_id,bindings))
-		 pat g
-	   ))
-	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
-      ]
-      g
-*)
 
 
 (* [generalize_dependent_of x hyp g]
@@ -735,12 +466,9 @@ let generalize_dependent_of x hyp g =
     g
 
 
-
-
-
-    (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
+(* [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 =
@@ -1020,11 +748,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       g
 
 
-
-
-let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))
-
-
 (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
    lemmas for each function in [funs] w.r.t. [graphs]
 
@@ -1032,21 +755,28 @@ let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))
    [functional_induction] is Indfun.functional_induction (same pb)
 *)
 
-let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) =
+let derive_correctness make_scheme functional_induction (funs: pconstant list) (graphs:inductive list) =
+  assert (funs <> []);
+  assert (graphs <> []);
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
-  let funs_constr = Array.map mkConst funs  in
-  States.with_state_protection_on_exception (fun () ->
-    let graphs_constr = Array.map mkInd graphs in
-    let lemmas_types_infos =
-      Util.Array.map2_i
-	(fun i f_constr graph ->
-	   let const_of_f,u = destConst f_constr in
-	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
-	     generate_type false const_of_f graph i
-	   in
-	   let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
+  let funs_constr = Array.map mkConstU funs  in
+  States.with_state_protection_on_exception
+    (fun () ->
+     let evd = ref Evd.empty in 
+     let graphs_constr = Array.map mkInd graphs in
+     let lemmas_types_infos =
+       Util.Array.map2_i
+	 (fun i f_constr graph ->
+	 (* let const_of_f,u = destConst f_constr in *)
+	 let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
+	   generate_type evd false f_constr graph i
+	 in
+	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
+	 graphs_constr.(i) <- graph;
+	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
+	 let _ = evd := fst (Typing.e_type_of (Global.env ()) !evd type_of_lemma) in 
 	   let type_of_lemma = nf_zeta type_of_lemma in
-	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
+	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
 	)
 	funs_constr
@@ -1055,65 +785,79 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     let schemes =
       (* The functional induction schemes are computed and not saved if there is more that one function
 	 if the block contains only one function we can safely reuse [f_rect]
-      *)
+       *)
       try
 	if not (Int.equal (Array.length funs_constr) 1) then raise Not_found;
-	[| find_induction_principle funs_constr.(0) |]
+	[| find_induction_principle evd funs_constr.(0) |]
       with Not_found ->
+	(
+	
 	  Array.of_list
 	    (List.map
 	       (fun entry ->
 		  (fst (fst(Future.force entry.Entries.const_entry_body)), Option.get entry.Entries.const_entry_type )
 	       )
-	       (make_scheme (Array.map_to_list (fun const -> const,GType []) funs))
+	       (make_scheme evd (Array.map_to_list (fun const -> const,GType []) funs))
 	    )
+	)
     in
     let proving_tac =
-      prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos
+      prove_fun_correct !evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos
     in
     Array.iteri
       (fun i f_as_constant ->
-	 let f_id = Label.to_id (con_label f_as_constant) in
+	 let f_id = Label.to_id (con_label (fst f_as_constant)) in
 	 (*i The next call to mk_correct_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	 i*)
 	 let lem_id = mk_correct_id f_id in
-	 Lemmas.start_proof lem_id
-	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
-                 (*FIXME*) Evd.empty
-	 (fst lemmas_types_infos.(i))
+	 let (typ,_) = lemmas_types_infos.(i) in 
+	 Lemmas.start_proof
+	   lem_id
+	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem)))
+           !evd
+	   typ
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
-	   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
-	      (proving_tac i))));
-	 do_save ();
-	 let finfo = find_Function_infos f_as_constant in
-	 let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in
-	 update_Function {finfo with correctness_lemma = Some lem_cst}
+		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
+						      (proving_tac i))));
+	 (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+	 let finfo = find_Function_infos (fst f_as_constant) in
+	 (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
+	 let _,lem_cst_constr = Evd.fresh_global
+				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
+	 let (lem_cst,_) = destConst lem_cst_constr in
+	 update_Function {finfo with correctness_lemma = Some lem_cst};
+
       )
       funs;
+    (* let evd = ref Evd.empty in  *)
     let lemmas_types_infos =
       Util.Array.map2_i
 	(fun i f_constr graph ->
-	   let const_of_f = fst (destConst f_constr) in
-	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
-	     generate_type true  const_of_f graph i
-	   in
-	   let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	   let type_of_lemma = nf_zeta type_of_lemma in
-	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
-	   type_of_lemma,type_info
+	 let (type_of_lemma_ctxt,type_of_lemma_concl,graph)   =
+	   generate_type evd true f_constr graph i
+	 in
+	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
+	 graphs_constr.(i) <- graph;
+	 let type_of_lemma =
+	   Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
+	 in
+	 let type_of_lemma = nf_zeta type_of_lemma in
+	 observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
+	 type_of_lemma,type_info
 	)
 	funs_constr
 	graphs_constr
     in
-    let kn,_ as graph_ind  = fst (destInd graphs_constr.(0)) in
-    let  mib,mip = Global.lookup_inductive graph_ind in
+
+    let (kn,_) as graph_ind,u  = (destInd graphs_constr.(0)) in
+    let mib,mip = Global.lookup_inductive graph_ind in
     let sigma, scheme = 
-	(Indrec.build_mutual_induction_scheme (Global.env ()) Evd.empty
+	(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
 	   (Array.to_list
 	      (Array.mapi
-		 (fun i _ -> ((kn,i),Univ.Instance.empty)(*FIXME*),true,InType)
+		 (fun i _ -> ((kn,i),u(* Univ.Instance.empty *)),true,InType)
 		 mib.Declarations.mind_packets
 	      )
 	   )
@@ -1127,26 +871,27 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     in
     Array.iteri
       (fun i f_as_constant ->
-	 let f_id = Label.to_id (con_label f_as_constant) in
+	 let f_id = Label.to_id (con_label (fst f_as_constant)) in
 	 (*i The next call to mk_complete_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	   i*)
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
-	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
-                            (*FIXME*) Evd.empty
+	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))  !evd
 	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-	      (proving_tac i))));
-	 do_save ();
-	 let finfo = find_Function_infos f_as_constant in
-	 let lem_cst,u = destConst (Constrintern.global_reference lem_id) in
+	      (proving_tac i)))) ;
+	 (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+	 let finfo = find_Function_infos (fst f_as_constant) in
+	 let _,lem_cst_constr = Evd.fresh_global
+				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
+	 let (lem_cst,_) = destConst lem_cst_constr in
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs)
-  ()
+    ()
 
 (***********************************************)
 
@@ -1257,7 +1002,7 @@ let invfun qhyp f g =
   match f with
     | Some f -> invfun qhyp f g
     | None ->
-        Proofview.V82.of_tactic begin
+       Proofview.V82.of_tactic begin
 	Tactics.try_intros_until
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
 	     let hyp_typ = pf_type_of g (mkVar hid)  in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5c74d74f89..c6fab43d1c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -217,7 +217,7 @@ let rec print_debug_queue b e =
 	begin
 	  Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
 	end;
-      print_debug_queue false e;
+      (* print_debug_queue false e; *)
     end
 
 let observe strm =
@@ -246,6 +246,18 @@ let observe_tac s tac g =
   then do_observe_tac s tac g
   else tac g
 
+
+let observe_tclTHENLIST s tacl =
+  if do_observe ()
+  then
+    let rec aux n = function
+      | [] -> tclIDTAC
+      | [tac] -> observe_tac (s ++ spc () ++ int n) tac
+      | tac::tacl -> observe_tac (s ++ spc () ++ int n) (tclTHEN tac (aux (succ n) tacl))
+    in
+    aux 0 tacl
+  else tclTHENLIST tacl
+	   
 (* Conclusion tactics *)
 
 (* The boolean value is_mes expresses that the termination is expressed
@@ -256,11 +268,11 @@ let tclUSER tac is_mes l g =
       | None -> clear []
       | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l)
   in
-  tclTHENLIST
+  observe_tclTHENLIST (str "tclUSER1")
     [
       clear_tac;
       if is_mes
-      then tclTHENLIST
+      then observe_tclTHENLIST (str "tclUSER2")
         [
 	  unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
             (delayed_force Indfun_common.ltof_ref))];
@@ -378,12 +390,12 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
     ) [] rev_context in 
     let rev_ids = pf_get_new_ids (List.rev ids) g in 
     let new_b = substl (List.map mkVar rev_ids) b in 
-    tclTHENLIST 
+    observe_tclTHENLIST (str "treat_case1") 
       [
 	h_intros (List.rev rev_ids);
 	Proofview.V82.of_tactic (intro_using teq_id);
 	onLastHypId (fun heq -> 
-	  tclTHENLIST[
+	  observe_tclTHENLIST (str "treat_case2")[
 	    thin to_intros;
 	    h_intros to_intros;
 	    (fun g' -> 
@@ -508,14 +520,14 @@ let rec prove_lt hyple g =
       in
       let y =
 	List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in
-      tclTHENLIST[
+      observe_tclTHENLIST (str "prove_lt1")[
 	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
 	observe_tac (str "prove_lt") (prove_lt hyple)
       ]
     with Not_found -> 
       (
 	(
-	  tclTHENLIST[
+	  observe_tclTHENLIST (str "prove_lt2")[
 	    Proofview.V82.of_tactic (apply (delayed_force lt_S_n));
 	    (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
 	  ])
@@ -533,7 +545,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
       let h' = next_ident_away_in_goal (h'_id) ids in
       let ids = h'::ids in
       let def = next_ident_away_in_goal def_id ids in
-      tclTHENLIST[
+      observe_tclTHENLIST (str "destruct_bounds_aux1")[
 	Proofview.V82.of_tactic (split (ImplicitBindings [s_max]));
 	Proofview.V82.of_tactic (intro_then
 	  (fun id -> 
@@ -541,18 +553,18 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 	    observe_tac (str "destruct_bounds_aux") 
 	      (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id)))
 		 [
-		   tclTHENLIST[Proofview.V82.of_tactic (intro_using h_id);
+		   observe_tclTHENLIST (str "")[Proofview.V82.of_tactic (intro_using h_id);
 			       Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
 			       Proofview.V82.of_tactic default_full_auto];
-		   tclTHENLIST[
+		   observe_tclTHENLIST (str "destruct_bounds_aux2")[
 		     observe_tac (str "clearing k ") (clear [id]);
 		     h_intros [k;h';def];
 		     observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl);
 		     observe_tac (str "unfold functional")
 		       (unfold_in_concl[(Locus.OnlyOccurrences [1],
 					 evaluable_of_global_reference infos.func)]);
-		     observe_tac (str "test" ) (
-		       tclTHENLIST[
+		     (
+		       observe_tclTHENLIST (str "test")[
 			 list_rewrite true
 			   (List.fold_right 
 			      (fun e acc -> (mkVar e,true)::acc)
@@ -572,7 +584,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 	      )end))
 	  ] g
       | (_,v_bound)::l -> 
-      tclTHENLIST[
+      observe_tclTHENLIST (str "destruct_bounds_aux3")[
 	Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
 	clear [v_bound];
 	tclDO 2 (Proofview.V82.of_tactic intro);
@@ -580,7 +592,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 	  (fun p_hyp -> 
 	    (onNthHypId 2 
 	       (fun p ->  
-		 tclTHENLIST[
+		 observe_tclTHENLIST (str "destruct_bounds_aux4")[
 		   Proofview.V82.of_tactic (simplest_elim 
 		     (mkApp(delayed_force max_constr, [| bound; mkVar p|])));
 		   tclDO 3 (Proofview.V82.of_tactic intro);
@@ -604,7 +616,7 @@ let destruct_bounds infos =
 let terminate_app f_and_args expr_info continuation_tac infos = 
     if expr_info.is_final && expr_info.is_main_branch 
     then 
-      tclTHENLIST[
+      observe_tclTHENLIST (str "terminate_app1")[
 	continuation_tac infos;
 	observe_tac (str "first split") 
 	  (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
@@ -615,7 +627,7 @@ let terminate_app f_and_args expr_info continuation_tac infos =
 let terminate_others _ expr_info continuation_tac infos = 
   if expr_info.is_final && expr_info.is_main_branch 
   then 
-    tclTHENLIST[
+    observe_tclTHENLIST (str "terminate_others")[
 	    continuation_tac infos;
       observe_tac (str "first split") 
 	(Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
@@ -671,17 +683,17 @@ let mkDestructEq :
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
     pf_typel new_hyps (fun _ ->
-    tclTHENLIST
+    observe_tclTHENLIST (str "mkDestructEq")
      [Simple.generalize new_hyps;
       (fun g2 ->
 	Proofview.V82.of_tactic (change_in_concl None
-	  (fun sigma ->
+	  (fun patvars sigma ->
 	    pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
 
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
-  let b =
+  let f_is_present =
     try
       check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a;
       false
@@ -697,11 +709,11 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
   let destruct_tac,rev_to_thin_intro = 
     mkDestructEq [expr_info.rec_arg_id] a' g in 
   let to_thin_intro = List.rev rev_to_thin_intro in 
-  observe_tac (str "treating case " ++ int (Array.length l) ++ spc () ++ Printer.pr_lconstr a') 
+  observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_lconstr a') 
     (try
       (tclTHENS
 	 destruct_tac
-	 (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
+	 (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
 	 ))
     with 
       | UserError("Refiner.thensn_tac3",_) 
@@ -717,11 +729,11 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
     try 
       let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in
       let new_infos = {expr_info with info = v} in 
-      tclTHENLIST[
+      observe_tclTHENLIST (str "terminate_app_rec")[
 	continuation_tac new_infos;
 	if expr_info.is_final && expr_info.is_main_branch 
 	then
-	  tclTHENLIST[ 
+	  observe_tclTHENLIST (str "terminate_app_rec1")[ 
 	    observe_tac (str "first split")
 	      (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
 	    observe_tac (str "destruct_bounds (3)")
@@ -734,7 +746,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
       observe_tac (str "terminate_app_rec not found") (tclTHENS
 	(Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))))
 	[		
-	  tclTHENLIST[
+	  observe_tclTHENLIST (str "terminate_app_rec2")[
 	    Proofview.V82.of_tactic (intro_using rec_res_id);
 	    Proofview.V82.of_tactic intro;
 	    onNthHypId 1 
@@ -747,11 +759,11 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 			 (v,v_bound)::expr_info.values_and_bounds; 
 		       args_assoc=(args,mkVar v)::expr_info.args_assoc
 		     } in
-		     tclTHENLIST[
+		     observe_tclTHENLIST (str "terminate_app_rec3")[
 		       continuation_tac new_infos;
 		       if expr_info.is_final && expr_info.is_main_branch 
 		       then
-			 tclTHENLIST[ 
+			 observe_tclTHENLIST (str "terminate_app_rec4")[ 
 			   observe_tac (str "first split") 
 			     (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
 			   observe_tac (str "destruct_bounds (2)") 
@@ -769,7 +781,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	      (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
 	      [ 
 		observe_tac (str "assumption") (Proofview.V82.of_tactic assumption);
-		tclTHENLIST
+		observe_tclTHENLIST (str "terminate_app_rec5")
 		  [
 		    tclTRY(list_rewrite true 
 			     (List.map 
@@ -805,7 +817,7 @@ let prove_terminate = travel terminate_info
 (* Equation proof *)
 
 let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos = 
-  terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos
+  observe_tac (str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos)
 
 let rec prove_le g = 
   let x,z = 
@@ -826,7 +838,7 @@ let rec prove_le g =
 	  let _,args = decompose_app t in 
 	  List.hd (List.tl args)
 	in 
-	tclTHENLIST[
+	observe_tclTHENLIST (str "prove_le")[
 	  Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|])));
 	  observe_tac (str "prove_le (rec)") (prove_le)
 	] 
@@ -856,7 +868,7 @@ let rec make_rewrite_list expr_info max = function
 			      (f_S max)]) false) g) )
       )
       [make_rewrite_list expr_info max l;
-       tclTHENLIST[ (* x < S max proof *)
+       observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
 	 Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm));
 	 observe_tac (str "prove_le(2)") prove_le
        ]
@@ -883,7 +895,7 @@ let make_rewrite expr_info l hp max =
 			      (f_S (f_S max))]) false)) g)
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
-	 (tclTHENLIST[
+	 (observe_tclTHENLIST (str "make_rewrite")[
 	   simpl_iter Locusops.onConcl;
 	   observe_tac (str "unfold functional")
 	     (unfold_in_concl[(Locus.OnlyOccurrences [1],
@@ -891,9 +903,12 @@ let make_rewrite expr_info l hp max =
 	   
 	   (list_rewrite true 
 	      (List.map (fun e -> mkVar e,true) expr_info.eqs));
-	   (observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic intros_reflexivity))]))
+	   (observe_tac (str "h_reflexivity")
+			(Proofview.V82.of_tactic intros_reflexivity)
+	   )
+	    ]))
        ;
-	 tclTHENLIST[ (* x < S (S max) proof *)
+	 observe_tclTHENLIST (str "make_rewrite1")[ (* x < S (S max) proof *)
 	 Proofview.V82.of_tactic (apply (delayed_force le_lt_SS));
 	 observe_tac (str "prove_le (3)") prove_le
 	 ]
@@ -904,7 +919,7 @@ let rec compute_max rew_tac max l =
   match l with 
     | [] -> rew_tac max
     | (_,p,_)::l -> 
-      tclTHENLIST[
+      observe_tclTHENLIST (str "compute_max")[
 	Proofview.V82.of_tactic (simplest_elim 
 	  (mkApp(delayed_force max_constr, [| max; mkVar p|])));
 	tclDO 3 (Proofview.V82.of_tactic intro);
@@ -924,7 +939,7 @@ let rec destruct_hex expr_info acc l =
 	    observe_tac (str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl)
       end
     | (v,hex)::l -> 
-      tclTHENLIST[
+      observe_tclTHENLIST (str "destruct_hex")[
 	Proofview.V82.of_tactic (simplest_case (mkVar hex));
 	clear [hex];
 	tclDO 2 (Proofview.V82.of_tactic intro);
@@ -939,7 +954,7 @@ let rec destruct_hex expr_info acc l =
 	
 let rec intros_values_eq expr_info acc = 
   tclORELSE(
-    tclTHENLIST[
+    observe_tclTHENLIST (str "intros_values_eq")[
       tclDO 2 (Proofview.V82.of_tactic intro);
       onNthHypId 1 (fun hex -> 
 	(onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc)))
@@ -952,14 +967,15 @@ let rec intros_values_eq expr_info acc =
 let equation_others _ expr_info continuation_tac infos = 
   if expr_info.is_final && expr_info.is_main_branch 
   then 
-    tclTHEN 
+    observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_lconstr expr_info.info)
+		(tclTHEN 
       (continuation_tac infos) 
-      (intros_values_eq expr_info [])
-  else continuation_tac infos
+      (observe_tac (str "intros_values_eq equation_others "  ++ Printer.pr_lconstr expr_info.info) (intros_values_eq expr_info [])))
+  else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_lconstr expr_info.info) (continuation_tac infos)
 
 let equation_app f_and_args expr_info continuation_tac infos = 
     if expr_info.is_final && expr_info.is_main_branch 
-    then intros_values_eq expr_info []
+    then ((observe_tac (str "intros_values_eq equation_app") (intros_values_eq expr_info [])))
     else continuation_tac infos
 	    
 let equation_app_rec (f,args) expr_info continuation_tac info = 
@@ -971,13 +987,13 @@ let equation_app_rec (f,args) expr_info continuation_tac info =
     with Not_found ->
       if expr_info.is_final && expr_info.is_main_branch 
       then 
-	tclTHENLIST
+	observe_tclTHENLIST (str "equation_app_rec")
 	  [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
 	    continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
 	    observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info [])
 	  ]
       else 
-	tclTHENLIST[
+	observe_tclTHENLIST (str "equation_app_rec1")[
   	  Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
 	  observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
 	]
@@ -1089,7 +1105,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       ]
 	     ;
 	     (* rest of the proof *)
-	     tclTHENLIST
+	     observe_tclTHENLIST (str "rest of proof")
 	       [observe_tac (str "generalize")
 		  (onNLastHypsId (nargs+1)
 		     (tclMAP (fun id ->
@@ -1280,7 +1296,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     build_proof Evd.empty
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
-	   tclTHENLIST
+	   observe_tclTHENLIST (str "")
 	     [
 	       Simple.generalize [lemma];
 	       Proofview.V82.of_tactic (Simple.intro hid);
@@ -1340,7 +1356,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	       (tclFIRST
 	 	  (List.map
 	 	     (fun c ->
-	 		Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST
+	 		Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST 
 	 		  [intros;
 	 		   Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*);
 	 		   Tacticals.New.tclCOMPLETE Auto.default_auto
@@ -1402,13 +1418,13 @@ let start_equation (f:global_reference) (term_f:global_reference)
   let terminate_constr = constr_of_global term_f in
   let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in
   let x = n_x_id ids nargs in
-  tclTHENLIST [
+  observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
     h_intros x;
     unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)];
     observe_tac (str "simplest_case")
       (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
                              Array.of_list (List.map mkVar x)))));
-    observe_tac (str "prove_eq") (cont_tactic x)] g;;
+    observe_tac (str "prove_eq") (cont_tactic x)]) g;;
 
 let (com_eqn : int -> Id.t ->
        global_reference -> global_reference -> global_reference
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 009b7323e4..705e594af1 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -167,11 +167,14 @@ let pattern_of_constr env sigma t =
       | Evar_kinds.MatchingVar (b,id) ->
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
           ctx := (id,None,ty)::!ctx;
-	  keep := Evar.Set.union (evars_of_term ty) !keep;
+	  let () = ignore (pattern_of_constr env ty) in
           assert (not b); PMeta (Some id)
       | Evar_kinds.GoalEvar -> 
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
-      | _ -> PMeta None)
+      | _ -> 
+	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+	let () = ignore (pattern_of_constr env ty) in
+	 PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
 	  { cip_style = ci.ci_pp_info.style;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 45052685df..46274f8329 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -359,8 +359,7 @@ and my_find_search_delta db_list local_db hdc concl =
       	(local_db::db_list)
 
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) =
-  let tactic = 
-    match t with
+  let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
     | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
     | Give_exact (c, cl)  -> exact poly (c, cl)
@@ -378,7 +377,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
     | Extern tacast -> 
       conclPattern concl p tacast
   in
-  tclLOG dbg (fun () -> pr_autotactic t) tactic
+  tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic)
 
 and trivial_resolve dbg mod_delta db_list local_db cl =
   try
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 244f9a727d..3fafbe15a1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -221,20 +221,19 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
   in
   let tac_of_hint =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
-      let tac =
-	match t with
-	  | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
-	  | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
-	  | Give_exact c -> e_give_exact flags poly c
-	  | Res_pf_THEN_trivial_fail (term,cl) ->
-              tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
-	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])
-	  | Extern tacast ->
-	    Proofview.V82.of_tactic (conclPattern concl p tacast)
+      let tac = function
+      | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags))
+      | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+      | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
+      | Res_pf_THEN_trivial_fail (term,cl) ->
+          Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+            (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
+      | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
+      | Extern tacast -> conclPattern concl p tacast
       in
+      let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
       let tac = if complete then tclCOMPLETE tac else tac in
-	match t with
+	match repr_auto_tactic t with
 	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
 	| _ ->
 (* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 789bcd1bdd..607664486b 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -172,18 +172,18 @@ and e_my_find_search db_list local_db hdc concl =
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
       (b,
-       let tac =
-	 match t with
-	   | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
-	   | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl))
-	   | Give_exact (c,cl) -> e_exact poly st (c,cl)
-	   | Res_pf_THEN_trivial_fail (term,cl) ->
-               (Tacticals.New.tclTHEN (Proofview.V82.tactic (unify_e_resolve poly st (term,cl)))
-		 (e_trivial_fail_db db_list local_db))
-	   | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
-	   | Extern tacast -> conclPattern concl p tacast
+        let tac = function
+        | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
+        | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl))
+        | Give_exact (c,cl) -> e_exact poly st (c,cl)
+        | Res_pf_THEN_trivial_fail (term,cl) ->
+          Tacticals.New.tclTHEN (Proofview.V82.tactic (unify_e_resolve poly st (term,cl)))
+            (e_trivial_fail_db db_list local_db)
+        | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
+        | Extern tacast -> conclPattern concl p tacast
        in
-       (tac,lazy (pr_autotactic t)))
+       let tac = run_auto_tactic t tac in
+       (tac, lazy (pr_autotactic t)))
   in
   List.map tac_of_hint hintl
 
@@ -194,7 +194,7 @@ and e_trivial_resolve db_list local_db gl =
 
 let e_possible_resolve db_list local_db gl =
   let hd = try Some (decompose_app_bound gl) with Bound -> None in
-  try List.map snd (e_my_find_search db_list local_db hd gl)
+  try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl)
   with Not_found -> []
 
 let find_first_goal gls =
@@ -204,6 +204,7 @@ let find_first_goal gls =
     exploration functor [Explore.Make]. *)
 
 type search_state = {
+  priority : int;
   depth : int; (*r depth of search before failing *)
   tacres : goal list sigma;
   last_tactic : std_ppcmds Lazy.t;
@@ -231,12 +232,12 @@ module SearchProblem = struct
 (*     msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
     let rec aux = function
       | [] -> []
-      | (tac,pptac) :: tacl ->
+      | (tac, cost, pptac) :: tacl ->
 	  try
 	    let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in
 (* 	    let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
-	      (lgls,pptac) :: aux tacl
+	      (lgls, cost, pptac) :: aux tacl
 	  with e when Errors.noncritical e ->
             let e = Errors.push e in
             Refiner.catch_failerror e; aux tacl
@@ -246,8 +247,11 @@ module SearchProblem = struct
      number of remaining goals. *)
   let compare s s' =
     let d = s'.depth - s.depth in
+    let d' = Int.compare s.priority s'.priority in
     let nbgoals s = List.length (sig_it s.tacres) in
-    if not (Int.equal d 0) then d else nbgoals s - nbgoals s'
+    if not (Int.equal d' 0) then d'
+    else if not (Int.equal d 0) then d
+    else Int.compare (nbgoals s) (nbgoals s')
 
   let branching s =
     if Int.equal s.depth 0 then
@@ -258,42 +262,39 @@ module SearchProblem = struct
       let nbgl = List.length (sig_it lg) in
       assert (nbgl > 0);
       let g = find_first_goal lg in
+      let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
       let assumption_tacs =
-	let l =
-	  filter_tactics s.tacres
-	    (List.map
-	       (fun id -> (e_give_exact (mkVar id),
-			   lazy (str "exact" ++ spc () ++ pr_id id)))
-	       (pf_ids_of_hyps g))
-	in
-	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
+        let tacs = List.map map_assum (pf_ids_of_hyps g) in
+        let l = filter_tactics s.tacres tacs in
+	List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
 				    last_tactic = pp; dblist = s.dblist;
 				    localdb = List.tl s.localdb;
 				    prev = ps}) l
       in
       let intro_tac =
+        let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in
 	List.map
-	  (fun (lgls as res,pp) ->
+	  (fun (lgls, cost, pp) ->
 	     let g' = first_goal lgls in
 	     let hintl =
 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 	     in
              let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
-	     { depth = s.depth; tacres = res;
+	     { depth = s.depth; priority = cost; tacres = lgls;
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb; prev = ps })
-	  (filter_tactics s.tacres [Tactics.intro,lazy (str "intro")])
+	  l
       in
       let rec_tacs =
 	let l =
 	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
 	in
 	List.map
-	  (fun (lgls as res, pp) ->
+	  (fun (lgls, cost, pp) ->
 	     let nbgl' = List.length (sig_it lgls) in
 	     if nbgl' < nbgl then
-	       { depth = s.depth; tacres = res; last_tactic = pp; prev = ps;
-		 dblist = s.dblist; localdb = List.tl s.localdb }
+	       { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp;
+                  prev = ps; dblist = s.dblist; localdb = List.tl s.localdb }
 	     else
 	       let newlocal = 
 		 let hyps = pf_hyps g in
@@ -304,7 +305,7 @@ module SearchProblem = struct
 		       else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true [])
 		     (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
 	       in
-		 { depth = pred s.depth; tacres = res;
+		 { depth = pred s.depth; priority = cost; tacres = lgls;
 		   dblist = s.dblist; last_tactic = pp; prev = ps;
 		   localdb = newlocal @ List.tl s.localdb })
 	  l
@@ -373,6 +374,7 @@ let pr_info dbg s =
 
 let make_initial_state dbg n gl dblist localdb =
   { depth = n;
+    priority = 0;
     tacres = tclIDTAC gl;
     last_tactic = lazy (mt());
     dblist = dblist;
@@ -576,7 +578,7 @@ let autounfold_one db cl =
   in
     if did then
       match cl with
-      | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp
+      | Some hyp -> change_in_hyp None (make_change_arg c') hyp
       | None -> convert_concl_no_check c' DEFAULTcast
     else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
   end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bcfd6657e0..7ab8d0c3ba 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1493,10 +1493,10 @@ let cutSubstInHyp l2r eqn id =
   tclTHENFIRST
     (tclTHENLIST [
        (Proofview.Unsafe.tclEVARS sigma);
-       (change_in_hyp None (fun s -> s,typ) (id,InHypTypeOnly));
+       (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
        (replace_core (onHyp id) l2r eqn)
     ])
-    (change_in_hyp None (fun s -> s,expected) (id,InHypTypeOnly))
+    (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))
   end
 
 let try_rewrite tac =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 101223b570..dea47794ec 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -68,7 +68,7 @@ let decompose_app_bound t =
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
 
-type 'a auto_tactic =
+type 'a auto_tactic_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -92,18 +92,23 @@ type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
+type 'a auto_tactic = 'a auto_tactic_ast
+
 type 'a gen_auto_tactic = {
   pri  : int;            (* A number lower is higher priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
   name  : hints_path_atom; (* A potential name to refer to the hint *) 
-  code : 'a auto_tactic     (* the tactic to apply when the concl matches pat *)
+  code : 'a     (* the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) gen_auto_tactic
+type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
 
 type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) gen_auto_tactic
+  (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic
+
+let run_auto_tactic tac k = k tac
+let repr_auto_tactic tac = tac
 
 let eq_hints_path_atom p1 p2 = match p1, p2 with
 | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
@@ -156,10 +161,19 @@ module Bounded_net = Btermdn.Make(struct
 				    let compare = pri_order_int
 				  end)
 
-type search_entry = stored_data list * stored_data list * Bounded_net.t * bool array list
-
+type search_entry = {
+  sentry_nopat : stored_data list;
+  sentry_pat : stored_data list;
+  sentry_bnet : Bounded_net.t;
+  sentry_mode : bool array list;
+}
 
-let empty_se = ([],[],Bounded_net.create (),[])
+let empty_se = {
+  sentry_nopat = [];
+  sentry_pat = [];
+  sentry_bnet = Bounded_net.create ();
+  sentry_mode = [];
+}
 
 let eq_pri_auto_tactic (_, x) (_, y) =
   if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
@@ -177,27 +191,29 @@ let eq_pri_auto_tactic (_, x) (_, y) =
   else
     false
 
-let add_tac pat t st (l,l',dn,m) =
+let add_tac pat t st se =
   match pat with
   | None -> 
-    if not (List.exists (eq_pri_auto_tactic t) l) then (List.insert pri_order t l, l', dn, m) 
-    else (l, l', dn, m)
+    if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se
+    else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat }
   | Some pat -> 
-    if not (List.exists (eq_pri_auto_tactic t) l')
-    then (l, List.insert pri_order t l', Bounded_net.add st dn (pat,t), m) else (l, l', dn, m)
+    if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se
+    else { se with
+        sentry_pat = List.insert pri_order t se.sentry_pat;
+        sentry_bnet = Bounded_net.add st se.sentry_bnet (pat, t); }
 
-let rebuild_dn st ((l,l',dn,m) : search_entry) =
+let rebuild_dn st se =
   let dn' = 
     List.fold_left 
       (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
-      (Bounded_net.create ()) l'
+      (Bounded_net.create ()) se.sentry_pat
   in
-    (l, l', dn', m)
+  { se with sentry_bnet = dn' }
 
-let lookup_tacs concl st (l,l',dn) =
-  let l'  = Bounded_net.lookup st dn concl in
+let lookup_tacs concl st se =
+  let l'  = Bounded_net.lookup st se.sentry_bnet concl in
   let sl' = List.stable_sort pri_order_int l' in
-    List.merge pri_order_int l sl'
+  List.merge pri_order_int se.sentry_nopat sl'
 
 module Constr_map = Map.Make(RefOrdered)
 
@@ -411,34 +427,38 @@ module Hint_db = struct
     if List.is_empty modes then true
     else List.exists (matches_mode args) modes
 
+  let merge_entry db nopat pat =
+    let h = Sort.merge pri_order (List.map snd db.hintdb_nopat @ nopat) pat in
+    List.map realize_tac h
+
   let map_none db =
-    List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) [])
-    
+    merge_entry db [] []
+
   let map_all k db =
-    let (l,l',_,_) = find k db in
-      List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
+    let se = find k db in
+    merge_entry db se.sentry_nopat se.sentry_pat
 	
   (** Precondition: concl has no existentials *)
   let map_auto (k,args) concl db =
-    let (l,l',dn,m) = find k db in
+    let se = find k db in
     let st = if db.use_dn then  (Some db.hintdb_state) else None in
-    let l' = lookup_tacs concl st (l,l',dn) in
-      List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
+    let pat = lookup_tacs concl st se in
+    merge_entry db [] pat
 
   let map_existential (k,args) concl db =
-    let (l,l',_,m) = find k db in
-      if matches_modes args m then
-	List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
-      else List.map realize_tac (List.map snd db.hintdb_nopat)
+    let se = find k db in
+      if matches_modes args se.sentry_mode then
+        merge_entry db se.sentry_nopat se.sentry_pat
+      else merge_entry db [] []
 
   (* [c] contains an existential *)
   let map_eauto (k,args) concl db =
-    let (l,l',dn,m) = find k db in
-      if matches_modes args m then
-	let st = if db.use_dn then Some db.hintdb_state else None in
-	let l' = lookup_tacs concl st (l,l',dn) in
-	  List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
-      else List.map realize_tac (List.map snd db.hintdb_nopat)
+    let se = find k db in
+      if matches_modes args se.sentry_mode then
+        let st = if db.use_dn then Some db.hintdb_state else None in
+        let pat = lookup_tacs concl st se in
+        merge_entry db [] pat
+      else merge_entry db [] []
 
   let is_exact = function
     | Give_exact _ -> true
@@ -496,10 +516,12 @@ module Hint_db = struct
   let add_list l db = List.fold_left (fun db k -> add_one k db) db l
 
   let remove_sdl p sdl = List.smartfilter p sdl 
-  let remove_he st p (sl1, sl2, dn, m as he) =
-    let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in
-      if sl1' == sl1 && sl2' == sl2 then he
-      else rebuild_dn st (sl1', sl2', dn, m)
+
+  let remove_he st p se =
+    let sl1' = remove_sdl p se.sentry_nopat in
+    let sl2' = remove_sdl p se.sentry_pat in
+    if sl1' == se.sentry_nopat && sl2' == se.sentry_pat then se
+    else rebuild_dn st { se with sentry_nopat = sl1'; sentry_pat = sl2' }
 
   let remove_list grs db =
     let filter (_, h) =
@@ -510,13 +532,16 @@ module Hint_db = struct
 
   let remove_one gr db = remove_list [gr] db
 
+  let get_entry se = List.map realize_tac (se.sentry_nopat @ se.sentry_pat)
+
   let iter f db =
+    let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
     f None [] (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat);
-    Constr_map.iter (fun k (l,l',_,m) -> f (Some k) m (List.map realize_tac (l@l'))) db.hintdb_map
+    Constr_map.iter iter_se db.hintdb_map
 
   let fold f db accu =
     let accu = f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
-    Constr_map.fold (fun k (l,l',_,m) -> f (Some k) m (List.map snd (l@l'))) db.hintdb_map accu
+    Constr_map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
 
   let transparent_state db = db.hintdb_state
 
@@ -528,8 +553,9 @@ module Hint_db = struct
     { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) }
 
   let add_mode gr m db =
-    let (l,l',dn,ms) = find gr db in
-      { db with hintdb_map = Constr_map.add gr (l,l',dn,m :: ms) db.hintdb_map }
+    let se = find gr db in
+    let se = { se with sentry_mode = m :: se.sentry_mode } in
+    { db with hintdb_map = Constr_map.add gr se db.hintdb_map }
 
   let cut db = db.hintdb_cut
 
@@ -782,10 +808,15 @@ let add_mode dbname l m =
   let db' = Hint_db.add_mode l m db in
     searchtable_add (dbname, db')
 
-type hint_obj = bool * string * hint_action  (* locality, name, action *)
+type hint_obj = {
+  hint_local : bool;
+  hint_name : string;
+  hint_action : hint_action;
+}
 
-let cache_autohint (_,(local,name,hints)) =
-  match hints with
+let cache_autohint (_, h) =
+  let name = h.hint_name in
+  match h.hint_action with
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
   | AddTransparency (grs, b) -> add_transparency name grs b
   | AddHints hints -> add_hint name hints
@@ -793,7 +824,7 @@ let cache_autohint (_,(local,name,hints)) =
   | AddCut path -> add_cut name path
   | AddMode (l, m) -> add_mode name l m
 
-let subst_autohint (subst,(local,name,hintlist as obj)) =
+let subst_autohint (subst, obj) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
     let gr' =
@@ -835,29 +866,30 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
     in
     if k' == k && data' == data then hint else (k',data')
   in
-    match hintlist with
-    | CreateDB _ -> obj
+  let action = match obj.hint_action with
+    | CreateDB _ -> obj.hint_action
     | AddTransparency (grs, b) ->
-	let grs' = List.smartmap (subst_evaluable_reference subst) grs in
-	  if grs==grs' then obj else (local, name, AddTransparency (grs', b))
+      let grs' = List.smartmap (subst_evaluable_reference subst) grs in
+      if grs == grs' then obj.hint_action else AddTransparency (grs', b)
     | AddHints hintlist ->
-	let hintlist' = List.smartmap subst_hint hintlist in
-	  if hintlist' == hintlist then obj else
-	    (local,name,AddHints hintlist')
+      let hintlist' = List.smartmap subst_hint hintlist in
+      if hintlist' == hintlist then obj.hint_action else AddHints hintlist'
     | RemoveHints grs ->
-	let grs' = List.smartmap (subst_global_reference subst) grs in
-	  if grs==grs' then obj else (local, name, RemoveHints grs')
+      let grs' = List.smartmap (subst_global_reference subst) grs in
+      if grs == grs' then obj.hint_action else RemoveHints grs'
     | AddCut path ->
       let path' = subst_hints_path subst path in
-	if path' == path then obj else (local, name, AddCut path')
+      if path' == path then obj.hint_action else AddCut path'
     | AddMode (l,m) ->
       let l' = subst_global_reference subst l in
-	(local, name, AddMode (l', m))
+      if l' == l then obj.hint_action else AddMode (l', m)
+  in
+  if action == obj.hint_action then obj else { obj with hint_action = action }
 
-let classify_autohint ((local,name,hintlist) as obj) =
-  match hintlist with
+let classify_autohint obj =
+  match obj.hint_action with
   | AddHints [] -> Dispose
-  | _ -> if local then Dispose else Substitute obj
+  | _ -> if obj.hint_local then Dispose else Substitute obj
 
 let inAutoHint : hint_obj -> obj =
   declare_object {(default_object "AUTOHINT") with
@@ -866,14 +898,22 @@ let inAutoHint : hint_obj -> obj =
 		    subst_function = subst_autohint;
 		    classify_function = classify_autohint; }
 
+let make_hint ?(local = false) name action = {
+  hint_local = local;
+  hint_name = name;
+  hint_action = action;
+}
+
 let create_hint_db l n st b =
-  Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
+  let hint = make_hint ~local:l n (CreateDB (b, st)) in
+  Lib.add_anonymous_leaf (inAutoHint hint)
 
 let remove_hints local dbnames grs =
   let dbnames = if List.is_empty dbnames then ["core"] else dbnames in
     List.iter
       (fun dbname ->
-	 Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs)))
+        let hint = make_hint ~local dbname (RemoveHints grs) in
+        Lib.add_anonymous_leaf (inAutoHint hint))
       dbnames
 
 (**************************************************************************)
@@ -882,37 +922,42 @@ let remove_hints local dbnames grs =
 let add_resolves env sigma clist local dbnames =
   List.iter
     (fun dbname ->
-       Lib.add_anonymous_leaf
-	 (inAutoHint
-	    (local,dbname, AddHints
-     	      (List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
-	        make_resolves env sigma (true,hnf,Flags.is_verbose()) 
-		  pri poly ~name:path gr) clist)))))
+      let r =
+        List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
+          make_resolves env sigma (true,hnf,Flags.is_verbose()) 
+            pri poly ~name:path gr) clist)
+      in
+      let hint = make_hint ~local dbname (AddHints r) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_unfolds l local dbnames =
   List.iter
-    (fun dbname -> Lib.add_anonymous_leaf
-       (inAutoHint (local,dbname, AddHints (List.map make_unfold l))))
+    (fun dbname ->
+      let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_cuts l local dbnames =
   List.iter
-    (fun dbname -> Lib.add_anonymous_leaf
-       (inAutoHint (local,dbname, AddCut l)))
+    (fun dbname ->
+      let hint = make_hint ~local dbname (AddCut l) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_mode l m local dbnames =
   List.iter
-    (fun dbname -> Lib.add_anonymous_leaf
-      (let m' = make_mode l m in
-	 (inAutoHint (local,dbname, AddMode (l,m')))))
+    (fun dbname ->
+      let m' = make_mode l m in
+      let hint = make_hint ~local dbname (AddMode (l, m')) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_transparency l b local dbnames =
   List.iter
-    (fun dbname -> Lib.add_anonymous_leaf
-       (inAutoHint (local,dbname, AddTransparency (l, b))))
+    (fun dbname ->
+      let hint = make_hint ~local dbname (AddTransparency (l, b)) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_extern pri pat tacast local dbname =
@@ -920,7 +965,7 @@ let add_extern pri pat tacast local dbname =
   | None -> None
   | Some (_, pat) -> Some pat
   in
-  let hint = local, dbname, AddHints [make_extern pri pat tacast] in
+  let hint = make_hint ~local dbname (AddHints [make_extern pri pat tacast]) in
   Lib.add_anonymous_leaf (inAutoHint hint)
 
 let add_externs pri pat tacast local dbnames =
@@ -929,9 +974,9 @@ let add_externs pri pat tacast local dbnames =
 let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
-       Lib.add_anonymous_leaf (
-	 inAutoHint(local,dbname, 
-		    AddHints (List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l))))
+      let l = List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l in
+      let hint = make_hint ~local dbname (AddHints l) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let (forward_intern_tac, extern_intern_tac) = Hook.make ()
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 45cf562c05..958cca1c3b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array
 
 (** Pre-created hint databases *)
 
-type 'a auto_tactic =
+type 'a auto_tactic_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -36,26 +36,27 @@ type 'a auto_tactic =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr       (* Hint Extern *)
 
+type 'a auto_tactic
+
 type hints_path_atom = 
   | PathHints of global_reference list
   | PathAny
 
-type 'a gen_auto_tactic = {
+type 'a gen_auto_tactic = private {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
   name  : hints_path_atom; (** A potential name to refer to the hint *) 
-  code  : 'a auto_tactic; (** the tactic to apply when the concl matches pat *)
+  code  : 'a; (** the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) gen_auto_tactic
+type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
 
 type search_entry
 
 (** The head may not be bound. *)
 
-type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) gen_auto_tactic
+type hint_entry
 
 type hints_path =
   | PathAtom of hints_path_atom
@@ -196,6 +197,13 @@ val make_extern :
   int -> constr_pattern option -> Tacexpr.glob_tactic_expr
       -> hint_entry
 
+val run_auto_tactic : 'a auto_tactic ->
+  ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+
+(** This function is for backward compatibility only, not to use in newly
+    written code. *)
+val repr_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast
+
 val extern_intern_tac :
   (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f894eb8fc4..f29680e185 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2119,7 +2119,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
-        let c_interp sigma =
+        let c_interp patvars sigma =
+	  let lfun' = Id.Map.fold (fun id c lfun ->
+	    Id.Map.add id (Value.of_constr c) lfun) 
+	    patvars ist.lfun
+	  in
+	  let ist = { ist with lfun = lfun' } in
 	  if is_onhyps && is_onconcl
 	  then interp_type ist (pf_env gl) sigma c
 	  else interp_constr ist (pf_env gl) sigma c
@@ -2138,9 +2143,13 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Proofview.V82.tactic begin fun gl -> 
           let (sigma,sign,op) = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
-	  let env' = Environ.push_named_context sign env in
-          let c_interp sigma =
-	      try interp_constr ist env' sigma c
+          let c_interp patvars sigma =
+	    let lfun' = Id.Map.fold (fun id c lfun ->
+	      Id.Map.add id (Value.of_constr c) lfun) 
+	      patvars ist.lfun
+	    in
+	    let ist = { ist with lfun = lfun' } in
+	      try interp_constr ist env sigma c
 	      with e when to_catch e (* Hack *) ->
 		errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
           in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b1559da33f..7484139c68 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -584,7 +584,10 @@ let e_change_in_hyp redfun (id,where) =
       (Proofview.Goal.env gl) (Proofview.Goal.sigma gl))
     convert_hyp
 
-type change_arg = evar_map -> evar_map * constr
+type change_arg = Pattern.patvar_map -> evar_map -> evar_map * constr
+
+let make_change_arg c =
+  fun pats sigma -> (sigma, replace_vars (Id.Map.bindings pats) c)
 
 let check_types env sigma mayneedglobalcheck deep newc origc =
   let t1 = Retyping.get_type_of env sigma newc in
@@ -612,21 +615,15 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
   if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
   sigma, t'
 
-let change_and_check_subst cv_pb mayneedglobalcheck subst t env sigma c =
-  let t' sigma =
-    let sigma, t = t sigma in
-      sigma, replace_vars (Id.Map.bindings subst) t 
-  in change_and_check cv_pb mayneedglobalcheck true t' env sigma c
-
 (* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb deep t where env sigma c =
   let mayneedglobalcheck = ref false in
   let sigma,c = match where with
-  | None -> change_and_check cv_pb mayneedglobalcheck deep t env sigma c
+  | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
   | Some occl ->
       e_contextually false occl
         (fun subst ->
-          change_and_check_subst Reduction.CONV mayneedglobalcheck subst t)
+          change_and_check Reduction.CONV mayneedglobalcheck true (t subst))
         env sigma c in
   if !mayneedglobalcheck then
     begin
@@ -656,7 +653,7 @@ let change chg c cls gl =
     cls) gl
 
 let change_concl t = 
-  change_in_concl None (fun sigma -> sigma, t)
+  change_in_concl None (make_change_arg t)
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl (red_product,REVERTcast)
@@ -2769,7 +2766,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
     if Int.equal i nparams then
       let t = applist (hd, params@args) in
       Tacticals.New.tclTHEN
-        (change_in_hyp None (fun sigma -> sigma, t) (hyp0,InHypTypeOnly))
+        (change_in_hyp None (make_change_arg t) (hyp0,InHypTypeOnly))
         (tac avoid)
     else
       let c = List.nth argl (i-1) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index eea4956214..0069d100b7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -125,8 +125,9 @@ val exact_proof      : Constrexpr.constr_expr -> tactic
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
-type change_arg = evar_map -> evar_map * constr
+type change_arg = patvar_map -> evar_map -> evar_map * constr
 
+val make_change_arg   : constr -> change_arg
 val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> tactic
 val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
diff --git a/test-suite/bugs/closed/3199.v b/test-suite/bugs/closed/3199.v
new file mode 100644
index 0000000000..08bf62493d
--- /dev/null
+++ b/test-suite/bugs/closed/3199.v
@@ -0,0 +1,18 @@
+Axiom P : nat -> Prop.
+Axiom admit : forall n : nat, P n -> P n -> n = S n.
+Axiom foo : forall n, P n.
+
+Create HintDb bar.
+Hint Extern 3 => symmetry : bar.
+Hint Resolve admit : bar.
+Hint Immediate foo : bar.
+
+Lemma qux : forall n : nat, n = S n.
+Proof.
+intros n.
+eauto with bar.
+Defined.
+
+Goal True.
+pose (e := eq_refl (qux 0)); unfold qux in e.
+match type of e with context [eq_sym] => fail 1 | _ => idtac end.
diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v
index 3440f0e806..3ef9270d40 100644
--- a/test-suite/bugs/closed/3590.v
+++ b/test-suite/bugs/closed/3590.v
@@ -1,13 +1,10 @@
-Require Import TestSuite.admit.
-(* Set Primitive Projections. *)
 Set Implicit Arguments.
 Record prod A B := pair { fst : A ; snd : B }.
 Definition idS := Set.
-Goal forall x y : prod Set Set, fst x = fst y.
+Goal forall x y : prod Set Set, forall H : fst x = fst y, fst x = fst y.
   intros.
   change (@fst _ _ ?z) with (@fst Set idS z) at 2.
-  Unshelve.
-  admit.
+  apply H.
 Qed.
   
 (* Toplevel input, characters 20-58:
diff --git a/test-suite/bugs/closed/4120.v b/test-suite/bugs/closed/4120.v
new file mode 100644
index 0000000000..00db8f7f3c
--- /dev/null
+++ b/test-suite/bugs/closed/4120.v
@@ -0,0 +1,5 @@
+Definition id {T} (x : T) := x.
+Goal sigT (fun x => id x)%type.
+  change (fun x => ?f x) with f.
+  exists Type. exact Set.
+Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
new file mode 100644
index 0000000000..5f8c411ca8
--- /dev/null
+++ b/test-suite/bugs/closed/4121.v
@@ -0,0 +1,15 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *)
+(* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *)
+
+Set Universe Polymorphism.
+Class Contr_internal (A : Type) := BuildContr { center : A }.
+Arguments center A {_}.
+Class Contr (A : Type) : Type := Contr_is_trunc : Contr_internal A.
+Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
+Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A |}.
+Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}.
+Check @contr_paths_contr0@{i}.
+Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *)
+(** It should have length 1, just like contr_paths_contr0 *)
\ No newline at end of file
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 07f881721d..33891ad94c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -103,8 +103,13 @@ let instance_hook k pri global imps ?hook cst =
 
 let declare_instance_constant k pri global imps ?hook id poly uctx term termtype =
   let kind = IsDefinition Instance in
+  let uctx = 
+    let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
+				 (Universes.universes_of_constr term) in
+      Universes.restrict_universe_context uctx levels 
+  in
   let entry = 
-    Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
+    Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term
   in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
@@ -277,7 +282,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
       in
       let term = Option.map nf term in
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
-          let ctx = Evd.universe_context evm in
+          let ctx = Evd.universe_context_set evm in
 	  declare_instance_constant k pri global imps ?hook id 
             poly ctx (Option.get term) termtype
 	else if !refine_instance || Option.is_empty term then begin
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index cb88ae564d..2b7e9e4fe2 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -32,7 +32,7 @@ val declare_instance_constant :
   ?hook:(Globnames.global_reference -> unit) ->
   Id.t -> (** name *)
   bool -> (* polymorphic *)
-  Univ.universe_context -> (* Universes *)
+  Univ.universe_context_set -> (* Universes *)
   Constr.t -> (** body *)
   Term.types -> (** type *)
   Names.Id.t
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 456a6f9d0f..523134b50f 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -658,7 +658,7 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls
 	Array.mapi
 	  (fun i (n, t, l, o, d, tac) ->
             { obl_name = n ; obl_body = None; 
-	      obl_location = l; obl_type = reduce t; obl_status = o;
+	      obl_location = l; obl_type = t; obl_status = o;
 	      obl_deps = d; obl_tac = tac })
 	  obls, b
   in