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

47 files changed, 1132 insertions, 877 deletions

diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 0e0eb6d2..2ff2bd38 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Ccalgo
-open Names
 open Term
 
 type rule=
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7110e5b2..8884aef1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -23,7 +23,7 @@ open Pp
 open Errors
 open Util
 
-let reference dir s = Coqlib.gen_reference "CC" dir s
+let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
 let _f_equal = reference ["Init";"Logic"] "f_equal"
 let _eq_rect = reference ["Init";"Logic"] "eq_rect"
@@ -91,7 +91,7 @@ let atom_of_constr env sigma term =
   let kot = kind_of_term wh in
     match kot with
       App (f,args)->
-	if is_global _eq f && Int.equal (Array.length args) 3
+	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	  then `Eq (args.(0),
 		   decompose_term env sigma args.(1),
 		   decompose_term env sigma args.(2))
@@ -126,7 +126,7 @@ let non_trivial = function
 let patterns_of_constr env sigma nrels term=
   let f,args=
     try destApp (whd_delta env term) with DestKO -> raise Not_found in
-	if is_global _eq f && Int.equal (Array.length args) 3
+	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
@@ -147,7 +147,7 @@ let patterns_of_constr env sigma nrels term=
 let rec quantified_atom_of_constr env sigma nrels term =
   match kind_of_term (whd_delta env term) with
       Prod (id,atom,ff) -> 
-	if is_global _False ff then
+	if is_global (Lazy.force _False) ff then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
@@ -159,7 +159,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 let litteral_of_constr env sigma term=
   match kind_of_term (whd_delta env term) with
     | Prod (id,atom,ff) -> 
-	if is_global _False ff then
+	if is_global (Lazy.force _False) ff then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
@@ -246,10 +246,10 @@ let build_projection intype outtype (cstr:pconstructor) special default gls=
 let _M =mkMeta
 
 let app_global f args k = 
-  Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_app_global f args k = 
-  Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 
@@ -375,9 +375,9 @@ let discriminate_tac (cstr,u as cstru) p =
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
     (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
     (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
-    let identity = Universes.constr_of_global _I in
+    let identity = Universes.constr_of_global (Lazy.force _I) in
     (* let trivial=pf_type_of gls identity in *)
-    let trivial = Universes.constr_of_global _True in
+    let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
     let outtype = mkSort outtype in
     let pred=mkLambda(Name xid,outtype,mkRel 1) in
@@ -493,7 +493,7 @@ let f_equal =
     in
     Proofview.tclORELSE
       begin match kind_of_term concl with
-      | App (r,[|_;t;t'|]) when Globnames.is_global _eq r ->
+      | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r ->
 	  begin match kind_of_term t, kind_of_term t' with
 	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 7467604a..3c4cacbc 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -46,23 +46,23 @@ type ('constr,'tac) casee =
     Real of 'constr
   | Virtual of ('constr statement,'constr,'tac) cut
 
-type ('hyp,'constr,'pat,'tac) bare_proof_instr =
-  | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
-  | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
-  | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
+type ('var,'constr,'pat,'tac) bare_proof_instr =
+  | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr
+  | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr
+  | Phence of ('var,'constr,'pat,'tac) bare_proof_instr
   | Pcut of ('constr or_thesis statement,'constr,'tac) cut
   | Prew of side * ('constr statement,'constr,'tac) cut
-  | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
-  | Passume of ('hyp,'constr) hyp list
-  | Plet of ('hyp,'constr) hyp list
-  | Pgiven of ('hyp,'constr) hyp list
-  | Pconsider of 'constr*('hyp,'constr) hyp list
+  | Psuffices of ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
+  | Passume of ('var,'constr) hyp list
+  | Plet of ('var,'constr) hyp list
+  | Pgiven of ('var,'constr) hyp list
+  | Pconsider of 'constr*('var,'constr) hyp list
   | Pclaim of 'constr statement
   | Pfocus of 'constr statement
-  | Pdefine of Id.t * 'hyp list * 'constr
+  | Pdefine of Id.t * 'var list * 'constr
   | Pcast of Id.t or_thesis * 'constr
-  | Psuppose of ('hyp,'constr) hyp list
-  | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
+  | Psuppose of ('var,'constr) hyp list
+  | Pcase of 'var list*'pat*(('var,'constr or_thesis) hyp list)
   | Ptake of 'constr list
   | Pper of elim_type * ('constr,'tac) casee
   | Pend of block_type
@@ -70,19 +70,19 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr =
 
 type emphasis = int
 
-type ('hyp,'constr,'pat,'tac) gen_proof_instr=
+type ('var,'constr,'pat,'tac) gen_proof_instr=
     {emph: emphasis;
-     instr: ('hyp,'constr,'pat,'tac) bare_proof_instr }
+     instr: ('var,'constr,'pat,'tac) bare_proof_instr }
 
 
 type raw_proof_instr =
-    ((Id.t*(Constrexpr.constr_expr option)) Loc.located,
+    ((Id.t * (Constrexpr.constr_expr option)) Loc.located,
      Constrexpr.constr_expr,
      Constrexpr.cases_pattern_expr,
      raw_tactic_expr) gen_proof_instr
 
 type glob_proof_instr =
-    ((Id.t*(Tacexpr.glob_constr_and_expr option)) Loc.located,
+    ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located,
      Tacexpr.glob_constr_and_expr,
      Constrexpr.cases_pattern_expr,
      Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index d169dc13..774c20c9 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -89,25 +89,22 @@ let get_info sigma gl=
 let try_get_info sigma gl =
   Store.get (Goal.V82.extra sigma gl) info
 
-let get_stack pts =
+let get_goal_stack pts =
   let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
   let info = get_info sigma (List.hd goals) in
   info.pm_stack
 
 
 let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
+let proof_cond = Proof.done_cond proof_focus
 
 let focus p =
-  let inf = get_stack p in
+  let inf = get_goal_stack p in
   Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
 
 let unfocus () =
   Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
 
-let maximal_unfocus () = 
-  Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
-
 let get_top_stack pts =
   try
     Proof.get_at_focus proof_focus pts
@@ -116,7 +113,24 @@ let get_top_stack pts =
     let info = get_info sigma gl in
     info.pm_stack
 
+let get_stack pts = Proof.get_at_focus proof_focus pts
+
 let get_last env = match Environ.named_context env with
   | (id,_,_)::_ -> id
   | [] -> error "no previous statement to use"
 
+
+let get_end_command pts =
+  match get_top_stack pts with
+  | [] -> "\"end proof\""
+  | Claim::_ -> "\"end claim\""
+  | Focus_claim::_-> "\"end focus\""
+  | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _  ->
+      begin
+	match et with
+	  Decl_expr.ET_Case_analysis ->
+	    "\"end cases\" or start a new case"
+	| Decl_expr.ET_Induction ->
+	    "\"end induction\" or start a new case"
+      end
+  | _ -> anomaly (Pp.str"lonely suppose")
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 2864ba18..fd7e15c1 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -72,8 +72,8 @@ val get_last:  Environ.env -> Id.t
 (** [get_last] raises a [UserError] when it cannot find a previous
     statement in the environment. *)
 
+val get_end_command : Proof.proof -> string
+
 val focus : Proof.proof -> unit
 
 val unfocus : unit -> unit
-
-val maximal_unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d25681d..9d0b7f34 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -131,12 +131,13 @@ let daimon_tac gls =
 
 (* post-instruction focus management *)
 
-(* spiwack: This used to fail if there was no focusing command
-   above, but I don't think it ever happened. I hope it doesn't mess
-   things up*)
 let goto_current_focus () = 
-  Decl_mode.maximal_unfocus ()
+  Decl_mode.unfocus ()
 
+(* spiwack: used to catch errors indicating lack of "focusing command"
+   in the proof tree. In the current implementation, however, entering
+   the declarative mode puts a focus first, there should, therefore,
+   never be exception raised here. *)
 let goto_current_focus_or_top () =
   goto_current_focus ()
 
@@ -1444,27 +1445,35 @@ let rec postprocess pts instr =
 				      Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
 		  anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
 	end
-    | Pend _ ->
-	goto_current_focus_or_top ()
+    | Pend (B_elim ET_Case_analysis) -> goto_current_focus ()
+    | Pend B_proof -> Proof_global.set_proof_mode "Classic"
+    | Pend _ -> ()
 
 let do_instr raw_instr pts =
   let has_tactic = preprocess pts raw_instr.instr in
-  begin
+  (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the
+     current proof (and, actually so does [do_instr] later one, so
+     it's ok to do the same here. Ideally the proof should be properly
+     threaded through the commands here, but since the are interleaved
+     with actions on the proof mode, which is attached to the global
+     proof environment, it is not possible without heavy lifting. *)
+  let pts = Proof_global.give_me_the_proof () in
+  let pts =
     if has_tactic then
             let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
       let gl = { it=List.hd gls ; sigma=sigma; } in
       let env=  pf_env gl in
-      let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in
+      let ist = {ltacvars = Id.Set.empty; genv = env} in
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
 	interp_proof_instr (get_its_info gl) env sigma glob_instr in
-      ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)))
-    else () end;
-  postprocess pts raw_instr.instr;
-  (* spiwack: this should restore a compatible semantics with
-     v8.3 where we never stayed focused on 0 goal. *)
-  Proof_global.set_proof_mode "Declarative" ;
-  Decl_mode.maximal_unfocus ()
+      let (pts',_) = Proof.run_tactic (Global.env())
+        (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in
+      pts'
+    else pts
+  in
+  Proof_global.simple_with_current_proof (fun _ _ -> pts);
+  postprocess pts raw_instr.instr
 
 let proof_instr raw_instr =
   let p = Proof_global.give_me_the_proof () in
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 03929b3b..d598e7c3 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -19,6 +19,7 @@ open Tok (* necessary for camlp4 *)
 
 open Pcoq.Constr
 open Pcoq.Tactic
+open Ppdecl_proof
 
 let pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
@@ -35,22 +36,20 @@ let pr_goal gs =
 		       str "============================" ++ fnl ()  ++
 		       thesis ++ str " " ++  pc) ++ fnl ()
 
-(* arnaud: rebrancher ça ?
-let pr_open_subgoals () =
-  let p = Proof_global.give_me_the_proof () in
-  let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
-  let close_cmd = Decl_mode.get_end_command p in
-  pr_subgoals close_cmd sigma goals
-*)
-
-let pr_raw_proof_instr _ _ _ instr =
-  Errors.anomaly (Pp.str "Cannot print a proof_instr")
-    (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller
-                     dans cette direction
-       Ppdecl_proof.pr_proof_instr (Global.env()) instr
-    *)
-let pr_proof_instr _ _ _ instr = Empty.abort instr
-let pr_glob_proof_instr _ _ _ instr = Empty.abort instr
+let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll =
+  match gll with
+  | [goal] when pr_first ->
+      pr_goal { Evd.it = goal ; sigma = sigma }
+  | _ ->
+      (* spiwack: it's not very nice to have to call proof global
+         here, a more robust solution would be to add a hook for
+         [Printer.pr_open_subgoals] in proof modes, in order to
+         compute the end command. Yet a more robust solution would be
+         to have focuses give explanations of their unfocusing
+         behaviour. *)
+      let p = Proof_global.give_me_the_proof () in
+      let close_cmd = Decl_mode.get_end_command p in
+      str "Subproof completed, now type " ++ str close_cmd ++ str "."
 
 let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
   Decl_interp.interp_proof_instr 
@@ -65,23 +64,18 @@ let vernac_decl_proof () =
   else
     begin
       Decl_proof_instr.go_to_proof_mode () ;
-      Proof_global.set_proof_mode "Declarative" ;
-      Vernacentries.print_subgoals ()
+      Proof_global.set_proof_mode "Declarative"
     end
 
 (* spiwack: some bureaucracy is not performed here *)
 let vernac_return () =
   begin
     Decl_proof_instr.return_from_tactic_mode () ;
-    Proof_global.set_proof_mode "Declarative" ;
-    Vernacentries.print_subgoals ()
+    Proof_global.set_proof_mode "Declarative"
   end
 
 let vernac_proof_instr instr =
-  begin
-    Decl_proof_instr.proof_instr instr;
-    Vernacentries.print_subgoals ()
-  end
+  Decl_proof_instr.proof_instr instr
 
 (* Before we can write an new toplevel command (see below) 
     which takes a [proof_instr] as argument, we need to declare
@@ -92,7 +86,7 @@ let vernac_proof_instr instr =
 (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *)
 
 (* Only declared at raw level, because only used in vernac commands. *)
-let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type =
+let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
   Genarg.make0 None "proof_instr"
 
 (* We create a new parser entry [proof_mode]. The Declarative proof mode
@@ -106,14 +100,16 @@ let proof_instr : raw_proof_instr Gram.entry =
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
 
-let classify_proof_instr _ = VtProofStep false, VtLater
+let classify_proof_instr = function
+  | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
+  | _ -> VtProofStep false, VtLater
 
 (* We use the VERNAC EXTEND facility with a custom non-terminal
     to populate [proof_mode] with a new toplevel interpreter.
     The "-" indicates that the rule does not start with a distinguished
     string. *)
-VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr
-  [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ]
+VERNAC proof_mode EXTEND ProofInstr
+  [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ]
 END
 
 (* It is useful to use GEXTEND directly to call grammar entries that have been
@@ -143,7 +139,8 @@ let _ =
 					 (* We substitute the goal printer, by the one we built
 					     for the proof mode. *)
 					 Printer.set_printer_pr { Printer.default_printer_pr with
-								                Printer.pr_goal = pr_goal }
+								                Printer.pr_goal = pr_goal;
+                                                                                pr_subgoals = pr_subgoals; }
 				       end ;
                                        (* function [reset] goes back to No Proof Mode from
 					   Declarative Proof Mode *)
@@ -160,7 +157,7 @@ VERNAC COMMAND EXTEND DeclProof
 [ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ]
 END
 VERNAC COMMAND EXTEND  DeclReturn
-[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ]
+[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ]
 END
 
 let none_is_empty = function
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 27308666..b3198dbf 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -12,41 +12,35 @@ open Decl_expr
 open Names
 open Nameops
 
-let pr_constr = Printer.pr_constr_env
-let pr_tac = Pptactic.pr_glob_tactic
-let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr
-
 let pr_label = function
     Anonymous -> mt ()
   | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
 
-let pr_constr env c = pr_constr env Evd.empty c
-
-let pr_justification_items env = function
+let pr_justification_items pr_constr = function
     Some [] -> mt ()
   | Some (_::_ as l) ->
       spc () ++ str "by" ++ spc () ++
-	prlist_with_sep (fun () -> str ",") (pr_constr env) l
+	prlist_with_sep (fun () -> str ",") pr_constr l
   | None -> spc () ++ str "by *"
 
-let pr_justification_method env = function
+let pr_justification_method pr_tac = function
     None -> mt ()
   | Some tac ->
-      spc () ++ str "using" ++ spc () ++ pr_tac env tac
+      spc () ++ str "using" ++ spc () ++ pr_tac tac
 
-let pr_statement pr_it env st =
-  pr_label st.st_label ++ pr_it env st.st_it
+let pr_statement pr_constr st =
+  pr_label st.st_label ++ pr_constr st.st_it
 
-let pr_or_thesis pr_this env = function
+let pr_or_thesis pr_this = function
     Thesis Plain -> str "thesis"
   | Thesis (For id) ->
       str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
-  | This c -> pr_this env c
+  | This c -> pr_this c
 
-let pr_cut pr_it env c =
-  hov 1 (pr_it env c.cut_stat) ++
-    pr_justification_items env c.cut_by ++
-    pr_justification_method env c.cut_using
+let pr_cut pr_constr pr_tac pr_it c =
+  hov 1 (pr_it c.cut_stat) ++
+    pr_justification_items pr_constr c.cut_by ++
+    pr_justification_method pr_tac c.cut_using
 
 let type_or_thesis = function
     Thesis _ -> Term.mkProp
@@ -54,128 +48,127 @@ let type_or_thesis = function
 
 let _I x = x
 
-let rec print_hyps pconstr gtyp env sep _be _have hyps =
+let rec pr_hyps pr_var pr_constr gtyp sep _be _have hyps =
   let pr_sep = if sep then str "and" ++ spc () else mt () in
     match hyps with
 	(Hvar _ ::_) as rest ->
 	  spc () ++ pr_sep ++ str _have ++
-	    print_vars pconstr gtyp env false _be _have rest
+	    pr_vars pr_var pr_constr gtyp false _be _have rest
       | Hprop st :: rest ->
 	  begin
-	    let nenv =
-	      match st.st_label with
-		  Anonymous -> env
-		| Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
-	      spc() ++ pr_sep ++ pr_statement pconstr env st ++
-		print_hyps pconstr gtyp nenv true _be _have rest
+	(* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) 
+	      spc() ++ pr_sep ++ pr_statement pr_constr st ++
+		pr_hyps pr_var pr_constr gtyp true _be _have rest
 	  end
       | [] -> mt ()
 
-and print_vars pconstr gtyp env sep _be _have vars =
+and pr_vars pr_var pr_constr gtyp sep _be _have vars =
   match vars with
     Hvar st :: rest ->
       begin
-	let nenv =
-	  match st.st_label with
-	      Anonymous -> anomaly (Pp.str "anonymous variable")
-	    | Name id -> Environ.push_named (id,None,st.st_it) env in
+	(* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) 
 	let pr_sep = if sep then pr_comma () else mt () in
 		spc() ++ pr_sep ++
-		   pr_statement pr_constr env st ++
-		  print_vars pconstr gtyp nenv true _be _have rest
+		  pr_var st ++
+		  pr_vars pr_var pr_constr gtyp true _be _have rest
       end
    | (Hprop _ :: _) as rest ->
       let _st =  if _be then
 	str "be such that"
       else
 	str "such that" in
-	spc() ++ _st ++  print_hyps pconstr gtyp env false _be _have rest
+	spc() ++ _st ++  pr_hyps pr_var pr_constr gtyp false _be _have rest
   | [] -> mt ()
 
-let pr_suffices_clause env (hyps,c) =
-    print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++
-       str "to show" ++ spc () ++ pr_or_thesis pr_constr env c
+let pr_suffices_clause pr_var pr_constr (hyps,c) =
+    pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++
+       str "to show" ++ spc () ++ pr_or_thesis pr_constr c
 
 let pr_elim_type = function
     ET_Case_analysis -> str "cases"
   | ET_Induction -> str "induction"
 
-let pr_casee env =function
-    Real c -> str "on" ++ spc () ++ pr_constr env c
-  | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut
+let pr_block_type = function
+    B_elim et -> pr_elim_type et
+  | B_proof -> str "proof"
+  | B_claim -> str "claim"
+  | B_focus -> str "focus"
+
+let pr_casee pr_constr pr_tac =function
+    Real c -> str "on" ++ spc () ++ pr_constr c
+  | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut
 
 let pr_side = function
     Lhs -> str "=~"
   | Rhs -> str "~="
 
-let rec pr_bare_proof_instr _then _thus env = function
+let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function
   | Pescape -> str "escape"
-  | Pthen i -> pr_bare_proof_instr true _thus env i
-  | Pthus i -> pr_bare_proof_instr _then true env i
-  | Phence i -> pr_bare_proof_instr true true env i
+  | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac  true _thus i
+  | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac  _then true i
+  | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i
   | Pcut c ->
       begin
 	match _then,_thus with
 	    false,false -> str "have" ++ spc () ++
-	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
 	  | false,true  -> str "thus" ++ spc () ++
-	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
 	  | true,false  -> str "then" ++ spc () ++
-	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
 	  | true,true   -> str "hence" ++ spc () ++
-	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
       end
   | Psuffices c ->
-      str "suffices" ++  pr_cut pr_suffices_clause env c
+      str "suffices" ++  pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c
   | Prew (sid,c) ->
       (if _thus then str "thus" else str "    ") ++ spc () ++
-	pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c
+	pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c
   | Passume hyps ->
-      str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps
+      str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps
   | Plet hyps ->
-      str "let" ++ print_vars pr_constr _I env false true "let" hyps
+      str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps
   | Pclaim st ->
-      str "claim" ++ spc () ++ pr_statement pr_constr env st
+      str "claim" ++ spc () ++ pr_statement pr_constr st
   | Pfocus st ->
-      str "focus on" ++ spc () ++ pr_statement pr_constr env st
+      str "focus on" ++ spc () ++ pr_statement pr_constr st
   | Pconsider (id,hyps) ->
-      str "consider" ++ print_vars pr_constr _I env false false "consider" hyps
-      ++ spc () ++ str "from " ++ pr_constr env id
+      str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps
+      ++ spc () ++ str "from " ++ pr_constr id
   | Pgiven hyps ->
-      str "given" ++ print_vars pr_constr _I env false false "given" hyps
+      str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps
   | Ptake witl ->
       str "take" ++ spc () ++
-	prlist_with_sep pr_comma (pr_constr env) witl
+	prlist_with_sep pr_comma pr_constr witl
   | Pdefine (id,args,body) ->
       str "define" ++ spc () ++ pr_id id ++ spc () ++
 	prlist_with_sep spc
 	(fun st -> str "(" ++
-	   pr_statement pr_constr env st ++ str ")") args ++ spc () ++
-	str "as" ++ (pr_constr env body)
+	   pr_var st ++ str ")") args ++ spc () ++
+	str "as" ++ (pr_constr body)
   | Pcast (id,typ) ->
       str "reconsider" ++ spc () ++
-	pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++
-	str "as" ++ spc () ++ (pr_constr env typ)
+	pr_or_thesis pr_id id ++ spc () ++
+	str "as" ++ spc () ++ (pr_constr typ)
   | Psuppose hyps ->
       str "suppose" ++
-	print_hyps pr_constr _I env false false "we have" hyps
+	pr_hyps pr_var pr_constr _I false false "we have" hyps 
   | Pcase (params,pat,hyps) ->
       str "suppose it is" ++ spc () ++ pr_pat pat ++
 	(if params = [] then mt () else
 	   (spc () ++ str "with" ++ spc () ++
 	      prlist_with_sep spc
 	      (fun st -> str "(" ++
-		 pr_statement pr_constr env st ++ str ")") params ++ spc ()))
+		 pr_var st ++ str ")") params ++ spc ()))
       ++
 	(if hyps = [] then mt () else
 	   (spc () ++ str "and" ++
-	      print_hyps (pr_or_thesis pr_constr) type_or_thesis
-	      env false false "we have" hyps))
-  | Pper (et,c) ->
+	      pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis
+	      false false "we have" hyps)) 
+  | Pper (et,c) -> 
       str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
-      pr_casee env c
-  | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
-  | _ -> anomaly (Pp.str "unprintable instruction")
+	pr_casee pr_constr pr_tac c  
+  | Pend blk -> str "end" ++ spc () ++ pr_block_type blk
 
 let pr_emph = function
     0 -> str "    "
@@ -184,7 +177,39 @@ let pr_emph = function
   | 3 -> str "*** "
   | _ -> anomaly (Pp.str "unknown emphasis")
 
-let pr_proof_instr env instr =
+let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr =
   pr_emph instr.emph ++ spc () ++
-    pr_bare_proof_instr false false env instr.instr
+    pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr
+
+
+let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) =
+   pr_gen_proof_instr
+     (fun (_,(id,otyp)) -> 
+       match otyp with
+	 None -> pr_id id
+       | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")"
+     )
+     pconstr2
+     Ppconstr.pr_cases_pattern_expr
+     (ptac Pptactic.ltop)
+     instr
+
+let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) =
+    pr_gen_proof_instr
+      (fun (_,(id,otyp)) -> 
+	match otyp with
+	  None -> pr_id id
+	| Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")")
+     pconstr2
+     Ppconstr.pr_cases_pattern_expr
+     (ptac Pptactic.ltop)
+     instr
+
+let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) =
+  pr_gen_proof_instr
+    (fun st -> pr_statement pconstr1 st)
+    pconstr2
+    (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr)
+    (ptac Pptactic.ltop)
+    instr
 
diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli
index fd6fb663..678fc076 100644
--- a/plugins/decl_mode/ppdecl_proof.mli
+++ b/plugins/decl_mode/ppdecl_proof.mli
@@ -1,2 +1,14 @@
 
-val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds
+open Decl_expr
+open Pptactic
+
+val pr_gen_proof_instr : 
+  ('var -> Pp.std_ppcmds) ->
+  ('constr -> Pp.std_ppcmds) ->
+  ('pat -> Pp.std_ppcmds) ->
+  ('tac -> Pp.std_ppcmds) ->  
+  ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds
+
+val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer
+val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer
+val pr_proof_instr : proof_instr extra_genarg_printer
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 439b1a5c..c232ae31 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -49,13 +49,13 @@ let start_deriving f suchthat lemma =
           [suchthat], respectively. *)
       let (opaque,f_def,lemma_def) =
         match com with
-        | Admitted -> Errors.error"Admitted isn't supported in Derive."
+        | Admitted _ -> Errors.error"Admitted isn't supported in Derive."
         | Proved (_,Some _,_) ->
             Errors.error"Cannot save a proof of Derive with an explicit name."
         | Proved (opaque, None, obj) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
-                opaque , f_def , lemma_def
+                opaque <> Vernacexpr.Transparent , f_def , lemma_def
             | _ -> assert false
       in
       (** The opacity of [f_def] is adjusted to be [false], as it
diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v
new file mode 100644
index 00000000..294d6102
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellBasic.v
@@ -0,0 +1,15 @@
+(** Extraction to Haskell : use of basic Haskell types *)
+
+Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
+Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
+Extract Inductive unit => "()" [ "()" ].
+Extract Inductive list => "([])" [ "([])" "(:)" ].
+Extract Inductive prod => "(,)" [ "(,)" ].
+
+Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
+Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
+Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
+
+Extract Inlined Constant andb => "(Prelude.&&)".
+Extract Inlined Constant orb => "(Prelude.||)".
+Extract Inlined Constant negb => "Prelude.not".
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index 5f653ee1..a0930f15 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -59,6 +59,7 @@ Extract Constant Compare_dec.nat_compare =>
  "fun n m -> if n=m then Eq else if n<m then Lt else Gt".
 Extract Inlined Constant Compare_dec.leb => "(<=)".
 Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)".
+Extract Inlined Constant Compare_dec.lt_dec => "(<)".
 Extract Constant Compare_dec.lt_eq_lt_dec =>
  "fun n m -> if n>m then None else Some (n<m)".
 
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 21819aa8..97f85694 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -600,6 +600,7 @@ let pp_global k r =
     let rls = List.rev ls in (* for what come next it's easier this way *)
     match lang () with
       | Scheme -> unquote s (* no modular Scheme extraction... *)
+      | JSON -> dottify (List.map unquote rls)
       | Haskell -> if modular () then pp_haskell_gen k mp rls else s
       | Ocaml -> pp_ocaml_gen k mp rls (Some l)
 
@@ -628,7 +629,7 @@ let check_extract_ascii () =
   try
     let char_type = match lang () with
       | Ocaml -> "char"
-      | Haskell -> "Char"
+      | Haskell -> "Prelude.Char"
       | _ -> raise Not_found
     in
     String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 42e69d34..0f846013 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -235,7 +235,7 @@ let rec extract_structure_spec env mp = function
 
 and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MEident mp -> Visit.add_mp_all mp; MTident mp
-  | MEwith(me',WithDef(idl,c))->
+  | MEwith(me',WithDef(idl,(c,ctx)))->
       let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in
       let mt = extract_mexpr_spec env mp1 (me_struct,me') in
       (match extract_with_type env' c with (* cb may contain some kn *)
@@ -410,6 +410,7 @@ let descr () = match lang () with
   | Ocaml -> Ocaml.ocaml_descr
   | Haskell -> Haskell.haskell_descr
   | Scheme -> Scheme.scheme_descr
+  | JSON -> Json.json_descr
 
 (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli"
    Works similarly for the other languages. *)
@@ -440,7 +441,8 @@ let mono_filename f =
 let module_filename mp =
   let f = file_of_modfile mp in
   let d = descr () in
-  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f
+  let p = d.file_naming mp ^ d.file_suffix in
+  Some p, Option.map ((^) f) d.sig_suffix, Id.of_string f
 
 (*s Extraction of one decl to stdout. *)
 
diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib
index b7f45861..ad321243 100644
--- a/plugins/extraction/extraction_plugin.mllib
+++ b/plugins/extraction/extraction_plugin.mllib
@@ -6,6 +6,7 @@ Common
 Ocaml
 Haskell
 Scheme
+Json
 Extract_env
 G_extraction
 Extraction_plugin_mod
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 3caa558f..3fe5a8c0 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -41,12 +41,14 @@ let pr_language = function
   | Ocaml -> str "Ocaml"
   | Haskell -> str "Haskell"
   | Scheme -> str "Scheme"
+  | JSON -> str "JSON"
 
 VERNAC ARGUMENT EXTEND language
 PRINTED BY pr_language
 | [ "Ocaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
+| [ "JSON" ] -> [ JSON ]
 END
 
 (* Extraction commands *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 5e08fef5..37b41420 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -26,7 +26,7 @@ let pr_upper_id id = str (String.capitalize (Id.to_string id))
 
 let keywords =
   List.fold_right (fun s -> Id.Set.add (Id.of_string s))
-  [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
+  [ "Any"; "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
@@ -38,7 +38,7 @@ let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
 let preamble mod_name comment used_modules usf =
   let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
   in
-  (if not usf.magic then mt ()
+  (if not (usf.magic || usf.tunknown) then mt ()
    else
      str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++
      str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}")
@@ -52,19 +52,36 @@ let preamble mod_name comment used_modules usf =
   str "import qualified Prelude" ++ fnl () ++
   prlist pp_import used_modules ++ fnl () ++
   (if List.is_empty used_modules then mt () else fnl ()) ++
-  (if not usf.magic then mt ()
+  (if not (usf.magic || usf.tunknown) then mt ()
    else str "\
 \n#ifdef __GLASGOW_HASKELL__\
 \nimport qualified GHC.Base\
+\nimport qualified GHC.Prim\
+\n#else\
+\n-- HUGS\
+\nimport qualified IOExts\
+\n#endif" ++ fnl2 ())
+  ++
+  (if not usf.magic then mt ()
+   else str "\
+\n#ifdef __GLASGOW_HASKELL__\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = GHC.Base.unsafeCoerce#\
 \n#else\
 \n-- HUGS\
-\nimport qualified IOExts\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = IOExts.unsafeCoerce\
 \n#endif" ++ fnl2 ())
   ++
+  (if not usf.tunknown then mt ()
+   else str "\
+\n#ifdef __GLASGOW_HASKELL__\
+\ntype Any = GHC.Prim.Any\
+\n#else\
+\n-- HUGS\
+\ntype Any = ()\
+\n#endif" ++ fnl2 ())
+  ++
   (if not usf.mldummy then mt ()
    else str "__ :: any" ++ fnl () ++
         str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
@@ -102,7 +119,7 @@ let rec pp_type par vl t =
 	pp_par par
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy _ -> str "()"
-    | Tunknown -> str "()"
+    | Tunknown -> str "Any"
     | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
  in
   hov 0 (pp_rec par t)
@@ -243,12 +260,12 @@ let pp_logical_ind packet =
 	      prvect_with_sep spc pr_id packet.ip_consnames)
 
 let pp_singleton kn packet =
+  let name = pp_global Type (IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
-  let l' = List.rev l in
-  hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++
+  hov 2 (str "type " ++ name ++ spc () ++
 	 prlist_with_sep spc pr_id l ++
 	 (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++
-	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
+	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++
 		     pr_id packet.ip_consnames.(0)))
 
@@ -346,7 +363,7 @@ and pp_module_expr = function
   | MEfunctor _ -> mt ()
       (* for the moment we simply discard unapplied functors *)
   | MEident _ | MEapply _ -> assert false
-      (* should be expansed in extract_env *)
+      (* should be expanded in extract_env *)
 
 let pp_struct =
   let pp_sel (mp,sel) =
@@ -360,6 +377,7 @@ let pp_struct =
 let haskell_descr = {
   keywords = keywords;
   file_suffix = ".hs";
+  file_naming = string_of_modfile;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
new file mode 100644
index 00000000..125dc86b
--- /dev/null
+++ b/plugins/extraction/json.ml
@@ -0,0 +1,278 @@
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Globnames
+open Table
+open Miniml
+open Mlutil
+open Common
+
+let json_str s =
+  qs s
+
+let json_int i =
+  int i
+
+let json_bool b =
+  if b then str "true" else str "false"
+
+let json_null =
+  str "null"
+
+let json_global typ ref =
+  json_str (Common.pp_global typ ref)
+
+let json_id id =
+  json_str (Id.to_string id)
+
+let json_dict_one (k, v) =
+  json_str k ++ str (": ") ++ v
+
+let json_dict_open l =
+  str ("{") ++ fnl () ++
+  str ("  ") ++ hov 0 (prlist_with_sep pr_comma json_dict_one l)
+
+let json_dict l =
+  json_dict_open l ++ fnl () ++
+  str ("}")
+
+let json_list l =
+  str ("[") ++ fnl () ++
+  str ("  ") ++ hov 0 (prlist_with_sep pr_comma (fun x -> x) l) ++ fnl () ++
+  str ("]")
+
+let json_listarr a =
+  str ("[") ++ fnl () ++
+  str ("  ") ++ hov 0 (prvect_with_sep pr_comma (fun x -> x) a) ++ fnl () ++
+  str ("]")
+
+
+let preamble mod_name comment used_modules usf =
+  (match comment with
+    | None -> mt ()
+    | Some s -> str "/* " ++ hov 0 s ++ str " */" ++ fnl ()) ++
+  json_dict_open [
+    ("what", json_str "module");
+    ("name", json_id mod_name);
+    ("need_magic", json_bool (usf.magic));
+    ("need_dummy", json_bool (usf.mldummy));
+    ("used_modules", json_list
+      (List.map (fun mf -> json_str (file_of_modfile mf)) used_modules))
+  ]
+
+
+(*s Pretty-printing of types. *)
+
+let rec json_type vl = function
+  | Tmeta _ | Tvar' _ -> assert false
+  | Tvar i -> (try
+      let varid = List.nth vl (pred i) in json_dict [
+        ("what", json_str "type:var");
+        ("name", json_id varid)
+      ]
+    with Failure _ -> json_dict [
+        ("what", json_str "type:varidx");
+        ("name", json_int i)
+      ])
+  | Tglob (r, l) -> json_dict [
+      ("what", json_str "type:glob");
+      ("name", json_global Type r);
+      ("args", json_list (List.map (json_type vl) l))
+    ]
+  | Tarr (t1,t2) -> json_dict [
+      ("what", json_str "type:arrow");
+      ("left", json_type vl t1);
+      ("right", json_type vl t2)
+    ]
+  | Tdummy _ -> json_dict [("what", json_str "type:dummy")]
+  | Tunknown -> json_dict [("what", json_str "type:unknown")]
+  | Taxiom -> json_dict [("what", json_str "type:axiom")]
+
+
+(*s Pretty-printing of expressions. *)
+
+let rec json_expr env = function
+  | MLrel n -> json_dict [
+      ("what", json_str "expr:rel");
+      ("name", json_id (get_db_name n env))
+    ]
+  | MLapp (f, args) -> json_dict [
+      ("what", json_str "expr:apply");
+      ("func", json_expr env f);
+      ("args", json_list (List.map (json_expr env) args))
+    ]
+  | MLlam _ as a ->
+    let fl, a' = collect_lams a in
+    let fl, env' = push_vars (List.map id_of_mlid fl) env in
+    json_dict [
+      ("what", json_str "expr:lambda");
+      ("argnames", json_list (List.map json_id (List.rev fl)));
+      ("body", json_expr env' a')
+    ]
+  | MLletin (id, a1, a2) ->
+    let i, env' = push_vars [id_of_mlid id] env in
+    json_dict [
+      ("what", json_str "expr:let");
+      ("name", json_id (List.hd i));
+      ("nameval", json_expr env a1);
+      ("body", json_expr env' a2)
+    ]
+  | MLglob r -> json_dict [
+      ("what", json_str "expr:global");
+      ("name", json_global Term r)
+    ]
+  | MLcons (_, r, a) -> json_dict [
+      ("what", json_str "expr:constructor");
+      ("name", json_global Cons r);
+      ("args", json_list (List.map (json_expr env) a))
+    ]
+  | MLtuple l -> json_dict [
+      ("what", json_str "expr:tuple");
+      ("items", json_list (List.map (json_expr env) l))
+    ]
+  | MLcase (typ, t, pv) -> json_dict [
+      ("what", json_str "expr:case");
+      ("expr", json_expr env t);
+      ("cases", json_listarr (Array.map (fun x -> json_one_pat env x) pv))
+    ]
+  | MLfix (i, ids, defs) ->
+    let ids', env' = push_vars (List.rev (Array.to_list ids)) env in
+    let ids' = Array.of_list (List.rev ids') in
+    json_dict [
+      ("what", json_str "expr:fix");
+      ("funcs", json_listarr (Array.map (fun (fi, ti) ->
+        json_dict [
+          ("what", json_str "fix:item");
+          ("name", json_id fi);
+          ("body", json_function env' ti)
+        ]) (Array.map2 (fun a b -> a,b) ids' defs)))
+    ]
+  | MLexn s -> json_dict [
+      ("what", json_str "expr:exception");
+      ("msg", json_str s)
+    ]
+  | MLdummy -> json_dict [("what", json_str "expr:dummy")]
+  | MLmagic a -> json_dict [
+      ("what", json_str "expr:coerce");
+      ("value", json_expr env a)
+    ]
+  | MLaxiom -> json_dict [("what", json_str "expr:axiom")]
+
+and json_one_pat env (ids,p,t) =
+  let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [
+    ("what", json_str "case");
+    ("pat", json_gen_pat (List.rev ids') env' p);
+    ("body", json_expr env' t)
+  ]
+
+and json_gen_pat ids env = function
+  | Pcons (r, l) -> json_cons_pat r (List.map (json_gen_pat ids env) l)
+  | Pusual r -> json_cons_pat r (List.map json_id ids)
+  | Ptuple l -> json_dict [
+      ("what", json_str "pat:tuple");
+      ("items", json_list (List.map (json_gen_pat ids env) l))
+    ]
+  | Pwild -> json_dict [("what", json_str "pat:wild")]
+  | Prel n -> json_dict [
+      ("what", json_str "pat:rel");
+      ("name", json_id (get_db_name n env))
+    ]
+
+and json_cons_pat r ppl = json_dict [
+    ("what", json_str "pat:constructor");
+    ("name", json_global Cons r);
+    ("argnames", json_list ppl)
+  ]
+
+and json_function env t =
+  let bl, t' = collect_lams t in
+  let bl, env' = push_vars (List.map id_of_mlid bl) env in
+  json_dict [
+    ("what", json_str "expr:lambda");
+    ("argnames", json_list (List.map json_id (List.rev bl)));
+    ("body", json_expr env' t')
+  ]
+
+
+(*s Pretty-printing of inductive types declaration. *)
+
+let json_ind ip pl cv = json_dict [
+    ("what", json_str "decl:ind");
+    ("name", json_global Type (IndRef ip));
+    ("argnames", json_list (List.map json_id pl));
+    ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [
+        ("name", json_global Cons (ConstructRef (ip, idx+1)));
+        ("argtypes", json_list (List.map (json_type pl) c))
+      ]) cv))
+  ]
+
+
+(*s Pretty-printing of a declaration. *)
+
+let pp_decl = function
+  | Dind (kn, defs) -> prvecti_with_sep pr_comma
+    (fun i p -> if p.ip_logical then str ""
+     else json_ind (kn, i) p.ip_vars p.ip_types) defs.ind_packets
+  | Dtype (r, l, t) -> json_dict [
+      ("what", json_str "decl:type");
+      ("name", json_global Type r);
+      ("argnames", json_list (List.map json_id l));
+      ("value", json_type l t)
+    ]
+  | Dfix (rv, defs, typs) -> json_dict [
+      ("what", json_str "decl:fixgroup");
+      ("fixlist", json_listarr (Array.mapi (fun i r ->
+        json_dict [
+          ("what", json_str "fixgroup:item");
+          ("name", json_global Term rv.(i));
+          ("type", json_type [] typs.(i));
+          ("value", json_function (empty_env ()) defs.(i))
+        ]) rv))
+    ]
+  | Dterm (r, a, t) -> json_dict [
+      ("what", json_str "decl:term");
+      ("name", json_global Term r);
+      ("type", json_type [] t);
+      ("value", json_function (empty_env ()) a)
+    ]
+
+let rec pp_structure_elem = function
+  | (l,SEdecl d) -> [ pp_decl d ]
+  | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr
+  | (l,SEmodtype m) -> []
+      (* for the moment we simply discard module type *)
+
+and pp_module_expr = function
+  | MEstruct (mp,sel) -> List.concat (List.map pp_structure_elem sel)
+  | MEfunctor _ -> []
+      (* for the moment we simply discard unapplied functors *)
+  | MEident _ | MEapply _ -> assert false
+      (* should be expansed in extract_env *)
+
+let pp_struct mls =
+  let pp_sel (mp,sel) =
+    push_visible mp [];
+    let p = prlist_with_sep pr_comma identity
+      (List.concat (List.map pp_structure_elem sel)) in
+    pop_visible (); p
+  in
+  str "," ++ fnl () ++
+  str "  " ++ qs "declarations" ++ str ": [" ++ fnl () ++
+  str "    " ++ hov 0 (prlist_with_sep pr_comma pp_sel mls) ++ fnl () ++
+  str "  ]" ++ fnl () ++
+  str "}" ++ fnl ()
+
+
+let json_descr = {
+  keywords = Id.Set.empty;
+  file_suffix = ".json";
+  file_naming = file_of_modfile;
+  preamble = preamble;
+  pp_struct = pp_struct;
+  sig_suffix = None;
+  sig_preamble = (fun _ _ _ _ -> mt ());
+  pp_sig = (fun _ -> mt ());
+  pp_decl = pp_decl;
+}
diff --git a/plugins/extraction/json.mli b/plugins/extraction/json.mli
new file mode 100644
index 00000000..3ba240a1
--- /dev/null
+++ b/plugins/extraction/json.mli
@@ -0,0 +1 @@
+val json_descr : Miniml.language_descr
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 1e491d36..b7dee6cb 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -197,6 +197,7 @@ type language_descr = {
 
   (* Concerning the source file *)
   file_suffix : string;
+  file_naming : module_path -> string;
   (* the second argument is a comment to add to the preamble *)
   preamble :
     Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 30ac3d3f..8c482b4b 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -634,7 +634,12 @@ and pp_module_type params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MTsig (mp, sign) ->
       push_visible mp params;
-      let l = List.map pp_specif sign in
+      let try_pp_specif l x =
+	try pp_specif x :: l with Failure "empty phrase" -> l
+      in
+      (* We cannot use fold_right here due to side effects in pp_specif *)
+      let l = List.fold_left try_pp_specif [] sign in
+      let l = List.rev l in
       pop_visible ();
       str "sig " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -707,7 +712,12 @@ and pp_module_expr params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MEstruct (mp, sel) ->
       push_visible mp params;
-      let l = List.map pp_structure_elem sel in
+      let try_pp_structure_elem l x =
+	try pp_structure_elem x :: l with Failure "empty phrase" -> l
+      in
+      (* We cannot use fold_right here due to side effects in pp_structure_elem *)
+      let l = List.fold_left try_pp_structure_elem [] sel in
+      let l = List.rev l in
       pop_visible ();
       str "struct " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -736,6 +746,7 @@ let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
 let ocaml_descr = {
   keywords = keywords;
   file_suffix = ".ml";
+  file_naming = file_of_modfile;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = Some ".mli";
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 69dea25a..cc8b6d8e 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -212,7 +212,7 @@ and pp_module_expr = function
   | MEfunctor _ -> mt ()
       (* for the moment we simply discard unapplied functors *)
   | MEident _ | MEapply _ -> assert false
-      (* should be expansed in extract_env *)
+      (* should be expanded in extract_env *)
 
 let pp_struct =
   let pp_sel (mp,sel) =
@@ -225,6 +225,7 @@ let pp_struct =
 let scheme_descr = {
   keywords = keywords;
   file_suffix = ".scm";
+  file_naming = file_of_modfile;
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 44d760cc..a57c39ee 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -554,7 +554,7 @@ let _ = declare_string_option
 
 (*s Extraction Lang *)
 
-type lang = Ocaml | Haskell | Scheme
+type lang = Ocaml | Haskell | Scheme | JSON
 
 let lang_ref = Summary.ref Ocaml ~name:"ExtrLang"
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 1acbe355..648f2321 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -142,7 +142,7 @@ val file_comment : unit -> string
 
 (*s Target language. *)
 
-type lang = Ocaml | Haskell | Scheme
+type lang = Ocaml | Haskell | Scheme | JSON
 val lang : unit -> lang
 
 (*s Extraction modes: modular or monolithic, library or minimal ?
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 1fe09f6f..f0489048 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,3 +1,4 @@
+ExtrHaskellBasic.vo
 ExtrOcamlBasic.vo
 ExtrOcamlIntConv.vo
 ExtrOcamlBigIntConv.vo
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 29ea1e77..6c7b0938 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 open Context
 open Globnames
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a88778c7..5912f0a0 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -113,24 +113,14 @@ let mk_open_instance id idc gl m t=
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
-  let rec aux n avoid=
-    if Int.equal n 0 then [] else
+  let rec aux n avoid env evmap decls =
+    if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id avoid var_id gl) in
-	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
-  let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype false [] env evmap nt in
-  let rec raux n t=
-    if Int.equal n 0 then t else
-      match t with
-	  GLambda(loc,name,k,_,t0)->
-	    let t1=raux (n-1) t0 in
-	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1)
-	| _-> anomaly (Pp.str "can't happen") in
-  let ntt=try
-    fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*)
-  with e when Errors.noncritical e ->
-    error "Untypable instance, maybe higher-order non-prenex quantification" in
-    decompose_lam_n_assum m ntt
+      let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+      let decl = (Name nid,None,c) in
+	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
+  let evmap, decls = aux m [] env evmap [] in
+    evmap, decls, revt
 
 (* tactics   *)
 
@@ -159,11 +149,15 @@ let left_instance_tac (inst,id) continue seq=
 	    if m>0 then
 	      pf_constr_of_global id (fun idc ->
 		fun gl->
-		  let (rc,ot) = mk_open_instance id idc gl m t in
+		  let evmap,rc,ot = mk_open_instance id idc gl m t in
 		  let gt=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
-		    generalize [gt] gl)
+		  let evmap, _ =
+		    try Typing.e_type_of (pf_env gl) evmap gt
+		    with e when Errors.noncritical e ->
+		      error "Untypable instance, maybe higher-order non-prenex quantification" in
+		    tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
 	    else
 	      pf_constr_of_global id (fun idc ->
 		generalize [mkApp(idc,[|t|])])
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 2f7f21e4..7d034db5 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -209,7 +209,7 @@ open Hints
 let extend_with_auto_hints l seq gl=
   let seqref=ref seq in
   let f p_a_t =
-    match p_a_t.code with
+    match repr_auto_tactic p_a_t.code with
 	Res_pf (c,_) | Give_exact (c,_)
       | Res_pf_THEN_trivial_fail (c,_) ->
 	  (try
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 8006a3e1..7a56cd66 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -16,7 +16,6 @@ open Term
 open Tactics
 open Names
 open Globnames
-open Tacticals
 open Tacmach
 open Fourier
 open Contradiction
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
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 22ddd549..8b959c27 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -34,7 +34,7 @@ Extract Inductive sumor => option [ Some None ].
    -  rightmost choice (Inright) is (None) *)
 
 
-(** To preserve its laziness, andb is normally expansed.
+(** To preserve its laziness, andb is normally expanded.
     Let's rather use the ocaml && *)
 Extract Inlined Constant andb => "(&&)".
 
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index 7400d462..a5f90dd6 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -13,10 +13,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
+(* We import what is necessary for Omega *)
 Require Export ZArith_base.
 Require Export OmegaLemmas.
 Require Export PreOmega.
+
 Declare ML Module "omega_plugin".
 
 Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
@@ -25,11 +26,6 @@ Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
 
 Require Export Zhints.
 
-(*
-(* The constant minus is required in coq_omega.ml *)
-Require Minus.
-*)
-
 Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
 Hint Extern 10 (_ <= _) => abstract omega: zarith.
 Hint Extern 10 (_ < _) => abstract omega: zarith.
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index 9e5c1484..9f101dbf 100644
--- a/plugins/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
@@ -6,4 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* To strictly import the omega tactic *)
+
+Require ZArith_base.
+Require OmegaLemmas.
+Require PreOmega.
+
 Declare ML Module "omega_plugin".
diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v
new file mode 100644
index 00000000..9f101dbf
--- /dev/null
+++ b/plugins/omega/OmegaTactic.v
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* To strictly import the omega tactic *)
+
+Require ZArith_base.
+Require OmegaLemmas.
+Require PreOmega.
+
+Declare ML Module "omega_plugin".
diff --git a/plugins/omega/vo.itarget b/plugins/omega/vo.itarget
index 9d9a77a8..842210e2 100644
--- a/plugins/omega/vo.itarget
+++ b/plugins/omega/vo.itarget
@@ -1,4 +1,5 @@
 OmegaLemmas.vo
 OmegaPlugin.vo
+OmegaTactic.vo
 Omega.vo
 PreOmega.vo
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 637e0e28..2a2ef30f 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
+          PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+      | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
   in
   aux bodyi