Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

12 files changed, 530 insertions, 674 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c8214ada..4a832435 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -7,7 +7,6 @@ open Context
 open Namegen
 open Names
 open Declarations
-open Declareops
 open Pp
 open Tacmach
 open Proof_type
@@ -16,7 +15,6 @@ open Tactics
 open Indfun_common
 open Libnames
 open Globnames
-open Misctypes
 
 (* let msgnl = Pp.msgnl *)
 
@@ -46,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 =
@@ -70,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 =
@@ -943,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 =
@@ -962,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(false,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
@@ -1007,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 ->
@@ -1020,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
@@ -1031,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
@@ -1101,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
@@ -1191,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
@@ -1205,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
@@ -1213,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 =
@@ -1250,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))
@@ -1259,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 ff98f2b9..61fce267 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 545f8931..45e5aaf5 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -6,7 +6,6 @@ open Vars
 open Context
 open Namegen
 open Names
-open Declareops
 open Pp
 open Entries
 open Tactics
@@ -106,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) =
@@ -116,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
@@ -234,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,
@@ -244,46 +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
     Lemmas.start_proof
       new_princ_name
-      (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
-      (*FIXME*) Evd.empty
-    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 (*FIXME, no poly, nothing *)
+	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,_ = Names.repr_con 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,34 +496,34 @@ 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
-      begin
-	try
-	  let id = Pfedit.get_current_proof_name () in
-	  let s = Id.to_string id in
-	  let n = String.length "___________princ_________" in
-	  if String.length s >= n
-	  then if String.equal (String.sub s 0 n) "___________princ_________"
-	  then Pfedit.delete_current_proof ()
-	  else ()
-	  else ()
-	with e when Errors.noncritical e -> ()
-      end;
-      raise (Defining_principle e)
-    end
+    with e when Errors.noncritical e ->
+       begin
+	 begin
+	   try
+	     let id = Pfedit.get_current_proof_name () in
+	     let s = Id.to_string id in
+	     let n = String.length "___________princ_________" in
+	     if String.length s >= n
+	     then if String.equal (String.sub s 0 n) "___________princ_________"
+		  then Pfedit.delete_current_proof ()
+		  else ()
+	     else ()
+	   with e when Errors.noncritical e -> ()
+	 end;
+	 raise (Defining_principle e)
+       end
 
   in
   incr i;
   let opacity =
-    let finfos = find_Function_infos this_block_funs.(0) 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 a16b834f..f6e5578d 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 fd48ab59..043d4328 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 a2577e2b..9e3f3986 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -252,7 +252,7 @@ let coq_False_ref =
 
 (*
   [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
-  (the list of expresions on which we will do the matching)
+  (the list of expressions on which we will do the matching)
  *)
 let make_discr_match_el  =
   List.map (fun e -> (e,(Anonymous,None)))
@@ -674,7 +674,7 @@ and build_entry_lc_from_case env funname make_discr
 	   match el with brl end
 	   we first compute the list of lists corresponding to [el] and
 	   combine them .
-	   Then for each elemeent of the combinations,
+	   Then for each element of the combinations,
 	   we compute the result we compute one list per branch in [brl] and
 	   finally we just concatenate those list
 	*)
@@ -720,9 +720,9 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
   match brl with
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
     | br::brl' ->
-	(* alpha convertion to prevent name clashes *)
+	(* alpha conversion to prevent name clashes *)
 	let _,idl,patl,return = alpha_br avoid br in
-	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an indentifier *)
+	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
 	(* building a list of precondition stating that we are not in this branch
 	   (will be used in the following recursive calls)
 	*)
@@ -1149,7 +1149,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty
 
 
-(* debuging wrapper *)
+(* debugging wrapper *)
 let rebuild_cons env nb_args relname args crossed_types rt =
 (*   observennl  (str "rebuild_cons : rt := "++ pr_glob_constr rt ++  *)
 (* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
@@ -1163,7 +1163,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 (* naive implementation of parameter detection.
 
    A parameter is an argument which is only preceded by parameters and whose
-   calls are all syntaxically equal.
+   calls are all syntactically equal.
 
    TODO: Find a valid way to deal with implicit arguments here!
 *)
@@ -1178,7 +1178,7 @@ let rec compute_cst_params relnames params = function
       compute_cst_params relnames t_params b
   | GCases _ ->
       params  (* If there is still cases at this point they can only be
-		 discriminitation ones *)
+		 discrimination ones *)
   | GSort _ -> params
   | GHole _ -> params
   | GIf _ | GRec _ | GCast _ ->
@@ -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,27 +1252,25 @@ 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 =
-    let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
+    let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
       let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
 	funargs
       in
@@ -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 b0a05ec3..5bb1376e 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 6dbd61cf..e211b688 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -8,7 +8,6 @@ open Libnames
 open Globnames
 open Glob_term
 open Declarations
-open Declareops
 open Misctypes
 open Decl_kinds
 
@@ -29,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 =
@@ -116,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
@@ -222,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
@@ -293,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 =
@@ -303,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
@@ -328,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)|])
 	    )
@@ -352,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
@@ -400,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
 	);
@@ -551,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 =
@@ -566,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
@@ -589,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
@@ -615,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
   ()
@@ -774,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)
 		)
 	     )
 	     ()
@@ -812,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 76f8c6d2..738ade8c 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 67ddf374..10daf6e8 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 0c7b0a0b..d10924f8 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -45,7 +45,7 @@ let pr_with_bindings prc prlc (c,bl) =
 let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds =
   pr_with_bindings prc prc  (c,bl)
 
-(* The local debuging mechanism *)
+(* The local debugging mechanism *)
 (* let msgnl = Pp.msgnl *)
 
 let observe strm =
@@ -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~:
@@ -255,12 +244,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     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 easilly computable *)
+    (* 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 funcitonnal principle is defined in the
-       environement and due to the bug #1174, we will need to pose the principle
+    (* 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
@@ -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,8 @@ 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 ->
+				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
 	  ]
       )
 	g
@@ -436,13 +386,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 +409,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,12 +419,12 @@ 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
     tclTHENSEQ
       [ 
@@ -484,10 +436,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 +448,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 easilly 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 funcitonnal principle is defined in the
-       environement 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 +464,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 +746,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       g
 
 
-
-
-let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,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 +753,28 @@ let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,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 +783,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 +869,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 +1000,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 5558556e..0999b95d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -60,7 +60,7 @@ let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
   let ce = definition_entry ~univs:ctx value (*FIXME *) in
     ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
-let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
+let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
 
 let def_of_const t =
    match (kind_of_term t) with
@@ -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 ->
@@ -1247,9 +1263,9 @@ let build_new_goal_type () =
 let is_opaque_constant c =
   let cb = Global.lookup_constant c in
   match cb.Declarations.const_body with
-    | Declarations.OpaqueDef _ -> true
-    | Declarations.Undef _ -> true
-    | Declarations.Def _ -> false
+    | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None
+    | Declarations.Undef _ -> Vernacexpr.Opaque None
+    | Declarations.Def _ -> Vernacexpr.Transparent
 
 let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
@@ -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