Merge PR#379: Introducing evar-insensitive constrs

22 files changed, 259 insertions, 201 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index fad656223a..f9ebc42330 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -12,11 +12,12 @@ open Util
 open Names
 open Nameops
 open Term
-open Vars
 open Termops
 open Namegen
 open Environ
 open Evd
+open EConstr
+open Vars
 open Reduction
 open Reductionops
 open Tacred
@@ -43,12 +44,6 @@ type clausenv = {
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let map_clenv sub clenv =
-  { templval = map_fl sub clenv.templval;
-    templtyp = map_fl sub clenv.templtyp;
-    evd = cmap sub clenv.evd;
-    env = clenv.env }
-
 let clenv_nf_meta clenv c = nf_meta clenv.evd c
 let clenv_term clenv c = meta_instance clenv.evd c
 let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
@@ -56,9 +51,9 @@ let clenv_value clenv = meta_instance clenv.evd clenv.templval
 let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
 
 let refresh_undefined_univs clenv =
-  match kind_of_term clenv.templval.rebus with
+  match EConstr.kind clenv.evd clenv.templval.rebus with
   | Var _ -> clenv, Univ.empty_level_subst
-  | App (f, args) when isVar f -> clenv, Univ.empty_level_subst
+  | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
   | _ ->  
     let evd', subst = Evd.refresh_undefined_universes clenv.evd in
     let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
@@ -71,15 +66,18 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 
 exception NotExtensibleClause
 
+let mk_freelisted c =
+  map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c))
+
 let clenv_push_prod cl =
   let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
-  let rec clrec typ = match kind_of_term typ with
+  let rec clrec typ = match EConstr.kind cl.evd typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
 	let mv = new_meta () in
-	let dep = dependent (mkRel 1) u in
+	let dep = not (noccurn (cl_sigma cl) 1 u) in
 	let na' = if dep then na else Anonymous in
-	let e' = meta_declare mv t ~name:na' cl.evd in
+	let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in
 	let concl = if dep then subst1 (mkMeta mv) u else u in
 	let def = applist (cl.templval.rebus,[mkMeta mv]) in
 	{ templval = mk_freelisted def;
@@ -103,14 +101,17 @@ let clenv_push_prod cl =
    and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
 
 let clenv_environments evd bound t =
+  let open EConstr in
+  let open Vars in
   let rec clrec (e,metas) n t =
-    match n, kind_of_term t with
+    match n, EConstr.kind evd t with
       | (Some 0, _) -> (e, List.rev metas, t)
       | (n, Cast (t,_,_)) -> clrec (e,metas) n t
       | (n, Prod (na,t1,t2)) ->
 	  let mv = new_meta () in
-	  let dep = not (noccurn 1 t2) in
+	  let dep = not (noccurn evd 1 t2) in
 	  let na' = if dep then na else Anonymous in
+	  let t1 = EConstr.Unsafe.to_constr t1 in
 	  let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) t2) else t2)
@@ -128,11 +129,13 @@ let mk_clenv_from_env env sigma n (c,cty) =
     env = env }
 
 let mk_clenv_from_n gls n (c,cty) =
-  mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty)
+  let env = Proofview.Goal.env gls in
+  let sigma = Tacmach.New.project gls in
+  mk_clenv_from_env env sigma n (c, cty)
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t)
 
 (******************************************************************)
 
@@ -168,13 +171,13 @@ let clenv_assign mv rhs clenv =
     error "clenv_assign: circularity in unification";
   try
     if meta_defined clenv.evd mv then
-      if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+      if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
         error_incompatible_inst clenv mv
       else
 	clenv
     else
       let st = (Conv,TypeNotProcessed) in
-      {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
+      {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
   with Not_found ->
     error "clenv_assign: undefined meta"
 
@@ -219,7 +222,7 @@ let clenv_assign mv rhs clenv =
 *)
 
 let clenv_metas_in_type_of_meta evd mv =
-  (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
+  (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas
 
 let dependent_in_type_of_metas clenv mvs =
   List.fold_right
@@ -262,35 +265,38 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
-let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
-  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then
+let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
     clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
+let old_clenv_unique_resolver ?flags clenv gl =
+  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+  clenv_unique_resolver_gen ?flags clenv concl
+
+let clenv_unique_resolver ?flags clenv gl =
+  let concl = Proofview.Goal.concl gl in
+  clenv_unique_resolver_gen ?flags clenv concl
+
 let adjust_meta_source evd mv = function
   | loc,Evar_kinds.VarInstance id ->
     let rec match_name c l =
-      match kind_of_term c, l with
-      | Lambda (Name id,_,c), a::l when Constr.equal a (mkMeta mv) -> Some id
+      match EConstr.kind evd c, l with
+      | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id
       | Lambda (_,_,c), a::l -> match_name c l
       | _ -> None in
     (* This is very ad hoc code so that an evar inherits the name of the binder
        in situations like "ex_intro (fun x => P) ?ev p" *)
     let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
       if Metaset.mem mv t.freemetas then
-        let f,l = decompose_app t.rebus in
-        match kind_of_term f with
+        let f,l = decompose_app evd (EConstr.of_constr t.rebus) in
+        match EConstr.kind evd f with
         | Meta mv'' ->
           (match meta_opt_fvalue evd mv'' with
-          | Some (c,_) -> match_name c.rebus l
-          | None -> None)
-        | Evar ev ->
-          (match existential_opt_value evd ev with
-          | Some c -> match_name c l
+          | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l
           | None -> None)
         | _ -> None
       else None in
@@ -332,7 +338,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       let ty = clenv_meta_type clenv mv in
       (* Postpone the evar-ization if dependent on another meta *)
       (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta ty then fold clenv (mvs@[mv])
+      if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
@@ -404,7 +410,7 @@ type arg_bindings = constr explicit_bindings
  * of cval, ctyp. *)
 
 let clenv_independent clenv =
-  let mvs = collect_metas (clenv_value clenv) in
+  let mvs = collect_metas clenv.evd (clenv_value clenv) in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
@@ -482,7 +488,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -501,6 +507,7 @@ let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
+  let c = EConstr.Unsafe.to_constr c in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
 
 let clenv_match_args bl clenv =
@@ -513,7 +520,7 @@ let clenv_match_args bl clenv =
       (fun clenv (loc,b,c) ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
-          if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+          if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
           else error_already_defined b
         else
 	  clenv_assign_binding clenv k c)
@@ -522,7 +529,7 @@ let clenv_match_args bl clenv =
 exception NoSuchBinding
 
 let clenv_constrain_last_binding c clenv =
-  let all_mvs = collect_metas clenv.templval.rebus in
+  let all_mvs = collect_metas clenv.evd clenv.templval.rebus in
   let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
   clenv_assign_binding clenv k c
 
@@ -557,8 +564,9 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
+      let t = rename_bound_vars_as_displayed sigma [] [] t in
       let clause = mk_clenv_from_env env sigma n
-	(c,rename_bound_vars_as_displayed [] [] t)
+	(c, t)
       in clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_env env sigma n (c,t)
@@ -585,34 +593,36 @@ let pr_clenv clenv =
 (** Evar version of mk_clenv *)
 
 type hole = {
-  hole_evar : constr;
-  hole_type : types;
+  hole_evar : EConstr.constr;
+  hole_type : EConstr.types;
   hole_deps  : bool;
   hole_name : Name.t;
 }
 
 type clause = {
   cl_holes : hole list;
-  cl_concl : types;
+  cl_concl : EConstr.types;
 }
 
 let make_evar_clause env sigma ?len t =
+  let open EConstr in
+  let open Vars in
   let bound = match len with
   | None -> -1
   | Some n -> assert (0 <= n); n
   in
   (** FIXME: do the renaming online *)
-  let t = rename_bound_vars_as_displayed [] [] t in
+  let t = rename_bound_vars_as_displayed sigma [] [] t in
   let rec clrec (sigma, holes) n t =
     if n = 0 then (sigma, holes, t)
-    else match kind_of_term t with
+    else match EConstr.kind sigma t with
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
       let sigma = Sigma.Unsafe.of_evar_map sigma in
       let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
       let sigma = Sigma.to_evar_map sigma in
-      let dep = dependent (mkRel 1) t2 in
+      let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
         hole_type = t1;
@@ -667,24 +677,26 @@ let evar_of_binder holes = function
     user_err  (str "No such binder.")
 
 let define_with_type sigma env ev c =
+  let open EConstr in
   let t = Retyping.get_type_of env sigma ev in
   let ty = Retyping.get_type_of env sigma c in
   let j = Environ.make_judge c ty in
   let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
-  let (ev, _) = destEvar ev in
-  let sigma = Evd.define ev j.Environ.uj_val sigma in
+  let (ev, _) = destEvar sigma ev in
+  let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
   sigma
 
 let solve_evar_clause env sigma hyp_only clause = function
 | NoBindings -> sigma
 | ImplicitBindings largs ->
+  let open EConstr in
   let fold holes h =
     if h.hole_deps then
       (** Some subsequent term uses the hole *)
-      let (ev, _) = destEvar h.hole_evar in
-      let is_dep hole = occur_evar ev hole.hole_type in
+      let (ev, _) = destEvar sigma h.hole_evar in
+      let is_dep hole = occur_evar sigma ev hole.hole_type in
       let in_hyp = List.exists is_dep holes in
-      let in_ccl = occur_evar ev clause.cl_concl in
+      let in_ccl = occur_evar sigma ev clause.cl_concl in
       let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in
       let h = { h with hole_deps = dep } in
       h :: holes
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index e9236b1da3..4bcd50591c 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -14,6 +14,7 @@ open Names
 open Term
 open Environ
 open Evd
+open EConstr
 open Unification
 open Misctypes
 
@@ -28,8 +29,6 @@ type clausenv = {
   templtyp : constr freelisted (** its type *)}
 
 
-val map_clenv : (constr -> constr) -> clausenv -> clausenv
-
 (** subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
 
@@ -37,16 +36,16 @@ val clenv_value     : clausenv -> constr
 val clenv_type      : clausenv -> types
 
 (** substitute resolved metas *)
-val clenv_nf_meta   : clausenv -> constr -> constr
+val clenv_nf_meta   : clausenv -> EConstr.constr -> EConstr.constr
 
 (** type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
-val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv
+val mk_clenv_from : ('a, 'r) Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_n :
-  Goal.goal sigma -> int option -> constr * types -> clausenv
-val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
-val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
+  ('a, 'r) Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> clausenv
+val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
 (** Refresh the universes in a clenv *)
 val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
@@ -63,9 +62,12 @@ val clenv_unify :
   ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
 (** unifies the concl of the goal with the type of the clenv *)
-val clenv_unique_resolver :
+val old_clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
+val clenv_unique_resolver :
+  ?flags:unify_flags -> clausenv -> ('a, 'r) Proofview.Goal.t -> clausenv
+
 val clenv_dependent : clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
@@ -92,18 +94,18 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
    the optional int tells how many prods of the lemma have to be used 
    use all of them if None *)
 val make_clenv_binding_env_apply :
-  env -> evar_map -> int option -> constr * constr -> constr bindings ->
+  env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
    clausenv
 
 val make_clenv_binding_apply :
-  env -> evar_map -> int option -> constr * constr -> constr bindings ->
+  env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
    clausenv
 
 val make_clenv_binding_env :
-  env -> evar_map -> constr * constr -> constr bindings -> clausenv
+  env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
 
 val make_clenv_binding :
-  env -> evar_map -> constr * constr -> constr bindings -> clausenv
+  env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
 
 (** if the clause is a product, add an extra meta for this product *)
 exception NotExtensibleClause
@@ -134,9 +136,9 @@ val pr_clenv : clausenv -> Pp.std_ppcmds
 *)
 
 type hole = {
-  hole_evar : constr;
+  hole_evar : EConstr.constr;
   (** The hole itself. Guaranteed to be an evar. *)
-  hole_type : types;
+  hole_type : EConstr.types;
   (** Type of the hole in the current environment. *)
   hole_deps  : bool;
   (** Whether the remainder of the clause was dependent in the hole. Note that
@@ -148,10 +150,10 @@ type hole = {
 
 type clause = {
   cl_holes : hole list;
-  cl_concl : types;
+  cl_concl : EConstr.types;
 }
 
-val make_evar_clause : env -> evar_map -> ?len:int -> types ->
+val make_evar_clause : env -> evar_map -> ?len:int -> EConstr.types ->
   (evar_map * clause)
 (** An evar version of {!make_clenv_binding}. Given a type [t],
     [evar_environments env sigma ~len t bl] tries to eliminate at most [len]
@@ -159,7 +161,7 @@ val make_evar_clause : env -> evar_map -> ?len:int -> types ->
     type together with the list of holes generated. Assumes that [t] is
     well-typed in the environment. *)
 
-val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
+val solve_evar_clause : env -> evar_map -> bool -> clause -> EConstr.constr bindings ->
   evar_map
 (** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained
     in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 98b5bc8b05..0722ea0470 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -11,6 +11,7 @@ open Names
 open Term
 open Termops
 open Evd
+open EConstr
 open Refiner
 open Logic
 open Reduction
@@ -26,19 +27,19 @@ open Proofview.Notations
 
 let clenv_cast_meta clenv =
   let rec crec u =
-    match kind_of_term u with
+    match EConstr.kind clenv.evd u with
       | App _ | Case _ -> crec_hd u
-      | Cast (c,_,_) when isMeta c -> u
+      | Cast (c,_,_) when isMeta clenv.evd c -> u
       | Proj (p, c) -> mkProj (p, crec_hd c)
-      | _  -> map_constr crec u
+      | _  -> EConstr.map clenv.evd crec u
 
   and crec_hd u =
-    match kind_of_term (strip_outer_cast u) with
+    match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with
       | Meta mv ->
 	  (try
             let b = Typing.meta_type clenv.evd mv in
-	    assert (not (occur_meta b));
-	    if occur_meta b then u
+	    assert (not (occur_meta clenv.evd b));
+	    if occur_meta clenv.evd b then u
             else mkCast (mkMeta mv, DEFAULTcast, b)
 	  with Not_found -> u)
       | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
@@ -104,8 +105,8 @@ let dft = default_unify_flags
 
 let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let clenv gl = clenv_unique_resolver ~flags clenv gl in
-    clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
+    let clenv = clenv_unique_resolver ~flags clenv gl in
+    clenv_refine with_evars ~with_classes clenv
   end }
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 8a096b6457..5b7164705a 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -10,6 +10,7 @@
 
 open Term
 open Clenv
+open EConstr
 open Unification
 open Misctypes
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 509efbc5b8..8367c09b8f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -18,21 +18,23 @@ open Pp
 (* Instantiation of existential variables *)
 (******************************************)
 
-let depends_on_evar evk _ (pbty,_,t1,t2) =
-  try Evar.equal (head_evar t1) evk
+let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
+  let t1 = EConstr.of_constr t1 in
+  let t2 = EConstr.of_constr t2 in
+  try Evar.equal (head_evar sigma t1) evk
   with NoHeadEvar ->
-  try Evar.equal (head_evar t2) evk
+  try Evar.equal (head_evar sigma t2) evk
   with NoHeadEvar -> false
 
 let define_and_solve_constraints evk c env evd =
-  if Termops.occur_evar evk c then
+  if Termops.occur_evar evd evk c then
     Pretype_errors.error_occur_check env evd evk c;
-  let evd = define evk c evd in
-  let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
+  let evd = define evk (EConstr.Unsafe.to_constr c) evd in
+  let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in
   match
     List.fold_left
       (fun p (pbty,env,t1,t2) -> match p with
-	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2
+	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2)
 	| UnifFailure _ as x -> x) (Success evd)
       pbs
   with
@@ -51,11 +53,11 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
     try Pretyping.understand_ltac flags
-      env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
+      env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err ~loc 
                 (str "Instance is not well-typed in the environment of " ++
-                 pr_existential_key sigma evk ++ str ".")
+                 Termops.pr_existential_key sigma evk ++ str ".")
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index a141708c2b..9046f45341 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -49,7 +49,7 @@ module V82 = struct
   (* Access to ".evar_concl" *)
   let concl evars gl =
     let evi = Evd.find evars gl in
-    evi.Evd.evar_concl
+    EConstr.of_constr evi.Evd.evar_concl
 
   (* Access to ".evar_extra" *)
   let extra evars gl =
@@ -62,6 +62,7 @@ module V82 = struct
        be shelved. It must not appear as a future_goal, so the future
        goals are restored to their initial value after the evar is
        created. *)
+    let concl = EConstr.Unsafe.to_constr concl in
     let prev_future_goals = Evd.future_goals evars in
     let prev_principal_goal = Evd.principal_future_goal evars in
     let evi = { Evd.evar_hyps = hyps;
@@ -78,8 +79,8 @@ module V82 = struct
     let evars = Sigma.to_evar_map evars in
     let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
     let ctxt = Environ.named_context_of_val hyps in
-    let inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
-    let ev = Term.mkEvar (evk,inst) in
+    let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
+    let ev = EConstr.mkEvar (evk,inst) in
     (evk, ev, evars)
 
   (* Instantiates a goal with an open term *)
@@ -89,7 +90,7 @@ module V82 = struct
       if not (Evarutil.occur_evar_upto sigma evk c) then ()
       else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
     in
-    Evd.define evk c sigma
+    Evd.define evk (EConstr.Unsafe.to_constr c) sigma
 
   (* Instantiates a goal with an open term, using name of goal for evk' *)
   let partial_solution_to sigma evk evk' c =
@@ -145,6 +146,7 @@ module V82 = struct
 
   (* Goal represented as a type, doesn't take into account section variables *)
   let abstract_type sigma gl =
+    let open EConstr in
     let (gl,sigma) = nf_evar sigma gl in
     let env = env sigma gl in
     let genv = Global.env () in
@@ -153,6 +155,7 @@ module V82 = struct
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
 					  if is_proof_var decl then
+                                            let decl = Termops.map_named_decl EConstr.of_constr decl in
 					    mkNamedProd_or_LetIn decl t
 					  else
 					    t
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6a79c1f451..a2fa34c05e 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -38,7 +38,7 @@ module V82 : sig
   val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val
 
   (* Access to ".evar_concl" *)
-  val concl : Evd.evar_map -> goal -> Term.constr
+  val concl : Evd.evar_map -> goal -> EConstr.constr
 
   (* Access to ".evar_extra" *)
   val extra : Evd.evar_map -> goal -> Evd.Store.t
@@ -48,16 +48,16 @@ module V82 : sig
        the evar corresponding to the goal, and an updated evar_map. *)
   val mk_goal : Evd.evar_map -> 
                          Environ.named_context_val ->
-                         Term.constr ->
+                         EConstr.constr ->
                          Evd.Store.t ->
-                         goal * Term.constr * Evd.evar_map
+                         goal * EConstr.constr * Evd.evar_map
 
   (* Instantiates a goal with an open term *)
-  val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
+  val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Instantiates a goal with an open term, reusing name of goal for
      second goal *)
-  val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map
+  val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Principal part of the weak-progress tactical *)
   val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
@@ -75,6 +75,6 @@ module V82 : sig
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
   (* Goal represented as a type, doesn't take into account section variables *)
-  val abstract_type : Evd.evar_map -> goal -> Term.types 
+  val abstract_type : Evd.evar_map -> goal -> EConstr.types 
 
 end
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 44c6294841..e6024785db 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -34,7 +34,7 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
-  | MetaInType of constr
+  | MetaInType of EConstr.constr
 
   (* Errors raised by the tactics *)
   | IntroNeedsProduct
@@ -86,7 +86,7 @@ let apply_to_hyp check sign id f =
     else sign
 
 let check_typability env sigma c =
-  if !check then let _ = unsafe_type_of env sigma c in ()
+  if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
 
 (************************************************************************)
 (************************************************************************)
@@ -138,12 +138,12 @@ let find_q x (m,q) =
         else find (Id.Set.union l accs) (i::acc) itl in
   find Id.Set.empty [] q
 
-let occur_vars_in_decl env hyps d =
+let occur_vars_in_decl env sigma hyps d =
   if Id.Set.is_empty hyps then false else
-    let ohyps = global_vars_set_of_decl env d in
+    let ohyps = global_vars_set_of_decl env sigma d in
     Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps
 
-let reorder_context env sign ord =
+let reorder_context env sigma sign ord =
   let ords = List.fold_right Id.Set.add ord Id.Set.empty in
   if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then
     error "Order list has duplicates";
@@ -152,13 +152,13 @@ let reorder_context env sign ord =
       | [] -> List.rev ctxt_tail @ ctxt_head
       | top::ord' when mem_q top moved_hyps ->
           let ((d,h),mh) = find_q top moved_hyps in
-          if occur_vars_in_decl env h d then
+          if occur_vars_in_decl env sigma h d then
             user_err ~hdr:"reorder_context"
               (str "Cannot move declaration " ++ pr_id top ++ spc() ++
               str "before " ++
               pr_sequence pr_id
                 (Id.Set.elements (Id.Set.inter h
-                  (global_vars_set_of_decl env d))));
+                  (global_vars_set_of_decl env sigma d))));
           step ord' expected ctxt_head mh (d::ctxt_tail)
       | _ ->
           (match ctxt_head with
@@ -173,16 +173,18 @@ let reorder_context env sign ord =
                     ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
   step ord ords sign mt_q []
 
-let reorder_val_context env sign ord =
-  val_of_named_context (reorder_context env (named_context_of_val sign) ord)
+let reorder_val_context env sigma sign ord =
+  let open EConstr in
+  val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord)
 
 
 
 
-let check_decl_position env sign d =
+let check_decl_position env sigma sign d =
+  let open EConstr in
   let x = NamedDecl.get_id d in
-  let needed = global_vars_set_of_decl env d in
-  let deps = dependency_closure env (named_context_of_val sign) needed in
+  let needed = global_vars_set_of_decl env sigma d in
+  let deps = dependency_closure env sigma (named_context_of_val sign) needed in
   if Id.List.mem x deps then
     user_err ~hdr:"Logic.check_decl_position"
       (str "Cannot create self-referring hypothesis " ++ pr_id x);
@@ -233,12 +235,12 @@ let hyp_of_move_location = function
   | MoveBefore id -> id
   | _ -> assert false
 
-let move_hyp toleft (left,declfrom,right) hto =
+let move_hyp sigma toleft (left,declfrom,right) hto =
   let env = Global.env() in
   let test_dep d d2 =
     if toleft
-    then occur_var_in_decl env (NamedDecl.get_id d2) d
-    else occur_var_in_decl env (NamedDecl.get_id d) d2
+    then occur_var_in_decl env sigma (NamedDecl.get_id d2) d
+    else occur_var_in_decl env sigma (NamedDecl.get_id d) d2
   in
   let rec moverec first middle = function
     | [] ->
@@ -266,6 +268,7 @@ let move_hyp toleft (left,declfrom,right) hto =
       	else
 	  moverec first' middle' right
   in
+  let open EConstr in
   if toleft then
     let right =
       List.fold_right push_named_context_val right empty_named_context_val in
@@ -278,10 +281,11 @@ let move_hyp toleft (left,declfrom,right) hto =
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
-let move_hyp_in_named_context hfrom hto sign =
+let move_hyp_in_named_context sigma hfrom hto sign =
+  let open EConstr in
   let (left,right,declfrom,toleft) =
     split_sign hfrom hto (named_context_of_val sign) in
-  move_hyp toleft (left,declfrom,right) hto
+  move_hyp sigma toleft (left,declfrom,right) hto
 
 (**********************************************************************)
 
@@ -314,23 +318,26 @@ let check_meta_variables c =
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let evm, b = Reductionops.infer_conv env sigma ty conclty in
+    let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
       if b then evm 
       else raise (RefinerError (BadType (arg,ty,conclty)))
   else sigma
 
-exception Stop of constr list
-let meta_free_prefix a =
+exception Stop of EConstr.t list
+let meta_free_prefix sigma a =
   try
+    let a = Array.map EConstr.of_constr a in
     let _ = Array.fold_left (fun acc a -> 
-      if occur_meta a then raise (Stop acc)
+      if occur_meta sigma a then raise (Stop acc)
       else a :: acc) [] a
     in a
   with Stop acc -> Array.rev_of_list acc
 
 let goal_type_of env sigma c =
-  if !check then unsafe_type_of env sigma c
-  else Retyping.get_type_of env sigma c
+  if !check then
+    let (sigma,t) = type_of env sigma (EConstr.of_constr c) in
+    (sigma, EConstr.Unsafe.to_constr t)
+  else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)))
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = Goal.V82.env sigma goal in
@@ -338,17 +345,20 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
   let mk_goal hyps concl =
     Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
   in
-    if (not !check) && not (occur_meta trm) then
-      let t'ty = Retyping.get_type_of env sigma trm in
+    if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
+      let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in
+      let t'ty = EConstr.Unsafe.to_constr t'ty in
       let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
         (goalacc,t'ty,sigma,trm)
     else
       match kind_of_term trm with
       | Meta _ ->
-	let conclty = nf_betaiota sigma conclty in
-	  if !check && occur_meta conclty then
+	let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
+	  if !check && occur_meta sigma conclty then
 	    raise (RefinerError (MetaInType conclty));
 	  let (gl,ev,sigma) = mk_goal hyps conclty in
+	  let ev = EConstr.Unsafe.to_constr ev in
+	  let conclty = EConstr.Unsafe.to_constr conclty in
 	  gl::goalacc, conclty, sigma, ev
 
       | Cast (t,k, ty) ->
@@ -367,13 +377,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
       | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env f then
+	  if is_template_polymorphic env sigma (EConstr.of_constr f) then
 	    let ty = 
 	      (* Template sort-polymorphism of definition and inductive types *)
-	      let firstmeta = Array.findi (fun i x -> occur_meta x) l in
+	      let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
 	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
-	        type_of_global_reference_knowing_parameters env sigma f args
+	        type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args)
 	    in
+	    let ty = EConstr.Unsafe.to_constr ty in
 	      goalacc, ty, sigma, f
 	  else
 	    mk_hdgoals sigma goal goalacc f
@@ -386,7 +397,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | Proj (p,c) ->
 	let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
 	let c = mkProj (p, c') in
-	let ty = get_type_of env sigma c in
+	let ty = get_type_of env sigma (EConstr.of_constr c) in
+	let ty = EConstr.Unsafe.to_constr ty in
 	  (acc',ty,sigma,c)
 
       | Case (ci,p,c,lf) ->
@@ -406,9 +418,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	(acc'',conclty',sigma, ans)
 
       | _ ->
-	if occur_meta trm then
+	if occur_meta sigma (EConstr.of_constr trm) then
 	  anomaly (Pp.str "refiner called with a meta in non app/case subterm");
-	let t'ty = goal_type_of env sigma trm in
+	let (sigma, t'ty) = goal_type_of env sigma trm in
 	let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
           (goalacc,t'ty,sigma, trm)
 
@@ -423,7 +435,8 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind_of_term trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma ty) in
+	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
+	let ev = EConstr.Unsafe.to_constr ev in
 	gl::goalacc,ty,sigma,ev
 
     | Cast (t,_, ty) ->
@@ -432,10 +445,10 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env f
+	  if is_template_polymorphic env sigma (EConstr.of_constr f)
 	  then
-	    let l' = meta_free_prefix l in	      
-	   (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f)
+	    let l' = meta_free_prefix sigma l in
+	   (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
@@ -460,17 +473,20 @@ and mk_hdgoals sigma goal goalacc trm =
     | Proj (p,c) ->
          let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
 	 let c = mkProj (p, c') in
-         let ty = get_type_of env sigma c in
+         let ty = get_type_of env sigma (EConstr.of_constr c) in
+         let ty = EConstr.Unsafe.to_constr ty in
 	   (acc',ty,sigma,c)
 
     | _ ->
-	if !check && occur_meta trm then
+	if !check && occur_meta sigma (EConstr.of_constr trm) then
 	  anomaly (Pp.str "refine called with a dependent meta");
-	goalacc, goal_type_of env sigma trm, sigma, trm
+        let (sigma, ty) = goal_type_of env sigma trm in
+	goalacc, ty, sigma, trm
 
 and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
-    let t = whd_all (Goal.V82.env sigma goal) sigma funty in
+    let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
+    let t = EConstr.Unsafe.to_constr t in
     let rec collapse t = match kind_of_term t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
@@ -487,11 +503,13 @@ and mk_arggoals sigma goal goalacc funty allargs =
 and mk_casegoals sigma goal goalacc p c =
   let env = Goal.V82.env sigma goal in
   let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
+  let ct = EConstr.of_constr ct in
   let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
-  let indspec =
+  let ((ind, u), spec) =
     try Tacred.find_hnf_rectype env sigma ct
     with Not_found -> anomaly (Pp.str "mk_casegoals") in
-  let (lbrty,conclty) = type_case_branches_with_names env indspec p c in
+  let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in
+  let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')
 
 
@@ -503,17 +521,17 @@ let convert_hyp check sign sigma d =
   let sign' =
     apply_to_hyp check sign id
       (fun _ d' _ ->
-        let c = NamedDecl.get_value d' in
+        let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in
         let env = Global.env_of_context sign in
-        if check && not (is_conv env sigma (NamedDecl.get_type d) (NamedDecl.get_type d')) then
+        if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then
 	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
 	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the body of "++ pr_id id ++ str ".");
-       if check then reorder := check_decl_position env sign d;
-       d) in
-  reorder_val_context env sign' !reorder
+       if check then reorder := check_decl_position env sigma sign d;
+       map_named_decl EConstr.Unsafe.to_constr d) in
+  reorder_val_context env sigma sign' !reorder
 
 
 
@@ -528,16 +546,18 @@ let prim_refiner r sigma goal =
   let mk_goal hyps concl = 
     Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) 
   in
+  let open EConstr in
   match r with
     (* Logical rules *)
     | Cut (b,replace,id,t) ->
 (*        if !check && not (Retyping.get_sort_of env sigma t) then*)
+        let t = EConstr.of_constr t in
         let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
 	let sign,t,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
 	    let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in
-	    move_hyp false ([], LocalAssum (id,t),named_context_of_val sign)
+	    move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign)
 	      nexthyp,
 	      t,cl,sigma
 	  else
@@ -547,13 +567,14 @@ let prim_refiner r sigma goal =
 	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
-	let oterm = Term.mkNamedLetIn id ev1 t ev2 in
+	let oterm = mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in
 	let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
     | Refine c ->
+        let cl = EConstr.Unsafe.to_constr cl in
 	check_meta_variables c;
 	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
+	let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in
 	  (sgl, sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 0dba9ef1ee..f98248e4d1 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -43,7 +43,7 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
-  | MetaInType of constr
+  | MetaInType of EConstr.constr
 
   (*i Errors raised by the tactics i*)
   | IntroNeedsProduct
@@ -55,7 +55,7 @@ exception RefinerError of refiner_error
 val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
-  Context.Named.Declaration.t -> Environ.named_context_val
+  EConstr.named_declaration -> Environ.named_context_val
 
-val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location ->
+val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
   Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9995a9394a..7e8ed31d1d 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -210,6 +210,7 @@ let refine_by_tactic env sigma ty tac =
   | _ -> assert false
   in
   let ans = Reductionops.nf_evar sigma ans in
+  let ans = EConstr.Unsafe.to_constr ans in
   (** [neff] contains the freshly generated side-effects *)
   let neff = Evd.eval_side_effects sigma in
   (** Reset the old side-effects *)
@@ -238,16 +239,17 @@ let apply_implicit_tactic tac = (); fun env sigma evk ->
   match snd (evar_source evk sigma) with
   | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
       when
-	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
+	Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
       (try
         let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
+        let c = EConstr.of_constr c in
         if Evarutil.has_undefined_evars sigma c then raise Exit;
         let (ans, _, ctx) =
 	  build_by_tactic env (Evd.evar_universe_context sigma) c tac in
         let sigma = Evd.set_universe_context sigma ctx in
-        sigma, ans
+        sigma, EConstr.of_constr ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index aad719db49..f9fb0b76de 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -60,7 +60,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards
 type universe_binders = Id.t Loc.located list
 
 val start_proof :
-  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
+  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -106,7 +106,7 @@ val get_current_context : unit -> Evd.evar_map * env
 (** [current_proof_statement] *)
 
 val current_proof_statement :
-  unit -> Id.t * goal_kind * types
+  unit -> Id.t * goal_kind * EConstr.types
 
 (** {6 ... } *)
 (** [get_current_proof_name ()] return the name of the current focused
@@ -166,15 +166,15 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 
 val build_constant_by_tactic :
   Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
-  types -> unit Proofview.tactic -> 
+  EConstr.types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool *
     Evd.evar_universe_context
 
 val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
-  types -> unit Proofview.tactic -> 
+  EConstr.types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
-val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic ->
+val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
   constr * Evd.evar_map
 (** A variant of the above function that handles open terms as well.
     Caveat: all effects are purged in the returned term at the end, but other
@@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
 val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr) option
+val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr) option
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 8dc165e72e..9d38e16ad7 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -66,9 +66,9 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
 
 (*** General proof functions ***)
 
-val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
+val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
 val dependent_start : Proofview.telescope -> proof
-val initial_goals : proof -> (Term.constr * Term.types) list
+val initial_goals : proof -> (EConstr.constr * EConstr.types) list
 val initial_euctx : proof -> Evd.evar_universe_context
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
@@ -79,7 +79,7 @@ val is_done : proof -> bool
 val is_complete : proof -> bool
 
 (* Returns the list of partial proofs to initial goals. *)
-val partial_proof : proof -> Term.constr list
+val partial_proof : proof -> EConstr.constr list
 
 val compact : proof -> proof
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ca7330fdb6..e4cba6f07d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -378,6 +378,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   in
   let entries =
     Future.map2 (fun p (_, t) ->
+      let t = EConstr.Unsafe.to_constr t in
       let univstyp, body = make_body t p in
       let univs, typ = Future.force univstyp in
 	{ Entries.
@@ -407,7 +408,7 @@ let return_proof ?(allow_partial=false) () =
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
-  let proofs = List.map (fun c -> c, eff) proofs in
+  let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
     proofs, Evd.evar_universe_context evd
  end else
   let initial_goals = Proof.initial_goals proof in
@@ -431,7 +432,7 @@ let return_proof ?(allow_partial=false) () =
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
   let proofs = 
-    List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in
+    List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 97a21cf225..3b2cc6b23b 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -86,7 +86,7 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
     end of the proof to close the proof. *)
 val start_proof :
   Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
-  Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
+  Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
@@ -201,7 +201,7 @@ end
 val get_default_goal_selector : unit -> Vernacexpr.goal_selector
 
 module V82 : sig
-  val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
+  val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
   Decl_kinds.goal_kind)
 end
 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 34443b93da..0fe5c73f15 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -11,6 +11,7 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Declarations
 open Globnames
 open Genredexpr
@@ -25,9 +26,7 @@ open Misctypes
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
   let ctyp = Retyping.get_type_of env sigma c in
-  if Termops.occur_meta_or_existential c then
-    error "vm_compute does not support existential variables.";
-  Vnorm.cbv_vm env c ctyp
+  Vnorm.cbv_vm env sigma c ctyp
 
 let warn_native_compute_disabled =
   CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
@@ -45,7 +44,8 @@ let cbv_native env sigma c =
 let whd_cbn flags env sigma t =
   let (state,_) =
     (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
-  in Reductionops.Stack.zip ~refold:true state
+  in
+  Reductionops.Stack.zip ~refold:true sigma state
 
 let strong_cbn flags =
   strong (whd_cbn flags)
@@ -254,9 +254,12 @@ let reduction_of_red_expr env =
   in
     reduction_of_red_expr
 
+let subst_mps subst c =
+  EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
+
 let subst_red_expr subs =
   Miscops.map_red_expr_gen
-    (Mod_subst.subst_mps subs)
+    (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
     (Patternops.subst_pattern subs)
 
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index d4c2c4a6c9..45e4610661 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -10,6 +10,7 @@
 
 open Names
 open Term
+open EConstr
 open Pattern
 open Genredexpr
 open Reductionops
diff --git a/proofs/refine.ml b/proofs/refine.ml
index c238f731d5..1ee6e0ca5f 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -28,12 +28,12 @@ let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
-    let t = NamedDecl.get_type decl in
+    let t = EConstr.of_constr (NamedDecl.get_type decl) in
     let evdref = ref sigma in
     let _ = Typing.e_sort_of env evdref t in
     let () = match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+    | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
     in
     (!evdref, Environ.push_named decl env)
   in
@@ -42,7 +42,7 @@ let typecheck_evar ev env sigma =
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
   let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
+  let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
   !evdref
 
 let typecheck_proof c concl env sigma =
@@ -101,6 +101,7 @@ let make_refine_enter ?(unsafe = true) f =
     else Pretype_errors.error_occur_check env sigma self c
   in
   (** Proceed to the refinement *)
+  let c = EConstr.Unsafe.to_constr c in
   let sigma = match evkmain with
     | None -> Evd.define self c sigma
     | Some evk ->
diff --git a/proofs/refine.mli b/proofs/refine.mli
index a44632eff5..1a254d578c 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -21,7 +21,7 @@ val pr_constr :
 
 (** {7 Refinement primitives} *)
 
-val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
 (** In [refine ?unsafe t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
@@ -30,17 +30,17 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
     tactic failures. If [unsafe] is [false] (default is [true]) [t] is
     type-checked beforehand. *)
 
-val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
+val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
 (** A generalization of [refine] which assumes exactly one goal under focus *)
 
 (** {7 Helper functions} *)
 
 val with_type : Environ.env -> Evd.evar_map ->
-  Term.constr -> Term.types -> Evd.evar_map * Term.constr
+  EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)
 
-val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine_casted : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 9a0b56b84b..5c7659ac0e 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -22,7 +22,7 @@ let project x = x.sigma
 (* Getting env *)
 
 let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
-let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
+let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
 let refiner pr goal_sigma =
   let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
@@ -198,10 +198,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
    destruct), this is not detected by this tactical. *)
 let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     :Proof_type.goal list Evd.sigma =
-  let oldhyps:Context.Named.t = pf_hyps goal in
+  let oldhyps = pf_hyps goal in
   let rslt:Proof_type.goal list Evd.sigma = tac goal in
   let { it = gls; sigma = sigma; } = rslt in
-  let hyps:Context.Named.t list =
+  let hyps =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
   let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in
   let newhyps =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 6dcafb77a4..56f5facf89 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -10,6 +10,7 @@
 
 open Evd
 open Proof_type
+open EConstr
 
 (** The refiner (handles primitive rules and high-level tactics). *)
 
@@ -17,7 +18,7 @@ val sig_it  : 'a sigma -> 'a
 val project : 'a sigma -> evar_map
 
 val pf_env  : goal sigma -> Environ.env
-val pf_hyps : goal sigma -> Context.Named.t
+val pf_hyps : goal sigma -> named_context
 
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 030a3cbfb9..b55f8ef113 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -41,11 +41,14 @@ let project  = Refiner.project
 let pf_env   = Refiner.pf_env
 let pf_hyps  = Refiner.pf_hyps
 
+let test_conversion env sigma pb c1 c2 =
+  Reductionops.check_conv ~pb env sigma c1 c2
+
 let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
 let pf_hyps_types gls  =
   let sign = Environ.named_context (pf_env gls) in
   List.map (function LocalAssum (id,x)
-                   | LocalDef (id,_,x) -> id, x)
+                   | LocalDef (id,_,x) -> id, EConstr.of_constr x)
            sign
 
 let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id
@@ -72,7 +75,7 @@ let pf_get_new_ids ids gls =
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
 
-let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
+let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id)
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
@@ -98,15 +101,15 @@ let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
 let pf_conv_x gl                = pf_reduce test_conversion gl Reduction.CONV
 let pf_conv_x_leq gl            = pf_reduce test_conversion gl Reduction.CUMUL
-let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
+let pf_const_value              = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c))
 
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls
 
-let pf_is_matching              = pf_apply Constr_matching.is_matching_conv
-let pf_matches                  = pf_apply Constr_matching.matches_conv
+let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p c
+let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p c
 
 (********************************************)
 (* Definition of the most primitive tactics *)
@@ -115,12 +118,15 @@ let pf_matches                  = pf_apply Constr_matching.matches_conv
 let refiner = refiner
 
 let internal_cut_no_check replace id t gl =
+  let t = EConstr.Unsafe.to_constr t in
   refiner (Cut (true,replace,id,t)) gl
 
 let internal_cut_rev_no_check replace id t gl =
+  let t = EConstr.Unsafe.to_constr t in
   refiner (Cut (false,replace,id,t)) gl
 
 let refine_no_check c gl =
+  let c = EConstr.Unsafe.to_constr c in
   refiner (Refine c) gl
 
 (* Versions with consistency checks *)
@@ -136,7 +142,7 @@ open Pp
 let db_pr_goal sigma g =
   let env = Goal.V82.env sigma g in
   let penv = print_named_context env in
-  let pc = print_constr_env env (Goal.V82.concl sigma g) in
+  let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in
   str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
@@ -165,7 +171,7 @@ module New = struct
     (** We only check for the existence of an [id] in [hyps] *)
     let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
-    Constrintern.construct_reference hyps id
+    EConstr.of_constr (Constrintern.construct_reference hyps id)
 
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
@@ -194,7 +200,7 @@ module New = struct
   let pf_get_hyp id gl =
     let hyps = Proofview.Goal.env gl in
     let sign =
-      try Environ.lookup_named id hyps
+      try EConstr.lookup_named id hyps
       with Not_found -> raise (RefinerError (NoSuchHyp id))
     in
     sign
@@ -206,7 +212,7 @@ module New = struct
     let env = Proofview.Goal.env gl in
     let sign = Environ.named_context env in
     List.map (function LocalAssum (id,x)
-                     | LocalDef (id,_,x) -> id, x)
+                     | LocalDef (id,_,x) -> id, EConstr.of_constr x)
              sign
 
   let pf_last_hyp gl =
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 59f296f64e..627a8e0e7e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -9,6 +9,7 @@
 open Names
 open Term
 open Environ
+open EConstr
 open Evd
 open Proof_type
 open Redexpr
@@ -33,18 +34,18 @@ val apply_sig_tac :
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env
-val pf_hyps               : goal sigma -> Context.Named.t
+val pf_hyps               : goal sigma -> named_context
 (*i val pf_untyped_hyps       : goal sigma -> (Id.t * constr) list i*)
 val pf_hyps_types         : goal sigma -> (Id.t * types) list
 val pf_nth_hyp_id         : goal sigma -> int -> Id.t
-val pf_last_hyp           : goal sigma -> Context.Named.Declaration.t
+val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
 val pf_unsafe_type_of            : goal sigma -> constr -> types
 val pf_type_of            : goal sigma -> constr -> evar_map * types
 val pf_hnf_type_of        : goal sigma -> constr -> types
 
-val pf_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
+val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
@@ -67,8 +68,8 @@ val pf_whd_all       : goal sigma -> constr -> constr
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
 val pf_nf_betaiota             : goal sigma -> constr -> constr
-val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types
-val pf_reduce_to_atomic_ind     : goal sigma -> types -> pinductive * types
+val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types
+val pf_reduce_to_atomic_ind     : goal sigma -> types -> (inductive * EInstance.t) * types
 val pf_compute                 : goal sigma -> constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
   -> goal sigma -> constr -> constr
@@ -106,31 +107,31 @@ module New : sig
 
   val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
   val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
-  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
+  val pf_concl : ('a, 'r) Proofview.Goal.t -> types
 
   (** WRONG: To be avoided at all costs, it typechecks the term entirely but
      forgets the universe constraints necessary to retypecheck it *)
-  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
 
   (** This function does no type inference and expects an already well-typed term.
       It recomputes its type in the fastest way possible (no conversion is ever involved) *)
-  val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
 
   (** This function entirely type-checks the term and computes its type
       and the implied universe constraints. *)
-  val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
-  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool
+  val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types
+  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool
 
-  val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
+  val pf_get_new_id  : identifier -> ('a, 'r) Proofview.Goal.t -> identifier
   val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
   val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list
 
-  val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
-  val pf_get_hyp_typ        : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
-  val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
+  val pf_get_hyp : identifier -> ('a, 'r) Proofview.Goal.t -> named_declaration
+  val pf_get_hyp_typ        : identifier -> ('a, 'r) Proofview.Goal.t -> types
+  val pf_last_hyp           : ('a, 'r) Proofview.Goal.t -> named_declaration
 
   val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
-  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types
+  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> (inductive * EInstance.t) * types
 
   val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
   val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types