25 files changed, 195 insertions, 305 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5ef7fac81..16798a1d5 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -154,7 +154,7 @@ let error_incompatible_inst clenv mv  =
       Name id ->
         user_err ~hdr:"clenv_assign"
           (str "An incompatible instantiation has already been found for " ++
-           pr_id id)
+           Id.print id)
     | _ ->
         anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.")
 
@@ -417,7 +417,7 @@ let check_bindings bl =
   match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with
     | NamedHyp s :: _ ->
 	user_err 
-	  (str "The variable " ++ pr_id s ++
+	  (str "The variable " ++ Id.print s ++
 	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
 	user_err 
@@ -435,12 +435,12 @@ let explain_no_such_bound_variable evd id =
   in
   let mvl = List.fold_left fold [] (Evd.meta_list evd) in
   user_err ~hdr:"Evd.meta_with_name"
-    (str"No such bound variable " ++ pr_id id ++
+    (str"No such bound variable " ++ Id.print id ++
      (if mvl == [] then str " (no bound variables at all in the expression)."
       else
         (str" (possible name" ++
          str (if List.length mvl == 1 then " is: " else "s are: ") ++
-         pr_enum pr_id mvl ++ str").")))
+         pr_enum Id.print mvl ++ str").")))
 
 let meta_with_name evd id =
   let na = Name id in
@@ -460,7 +460,7 @@ let meta_with_name evd id =
         n
     | _  ->
         user_err ~hdr:"Evd.meta_with_name"
-          (str "Binder name \"" ++ pr_id id ++
+          (str "Binder name \"" ++ Id.print id ++
            strbrk "\" occurs more than once in clause.")
 
 let meta_of_binder clause loc mvs = function
@@ -474,7 +474,7 @@ let error_already_defined b =
   match b with
     | NamedHyp id ->
         user_err 
-          (str "Binder name \"" ++ pr_id id ++
+          (str "Binder name \"" ++ Id.print id ++
            str"\" already defined with incompatible value.")
     | AnonHyp n ->
         anomaly
@@ -639,10 +639,10 @@ let explain_no_such_bound_variable holes id =
   let mvl = List.fold_right fold holes [] in
   let expl = match mvl with
   | [] -> str " (no bound variables at all in the expression)."
-  | [id] -> str "(possible name is: " ++ pr_id id ++ str ")."
-  | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")."
+  | [id] -> str "(possible name is: " ++ Id.print id ++ str ")."
+  | _ -> str "(possible names are: " ++ pr_enum Id.print mvl ++ str ")."
   in
-  user_err  (str "No such bound variable " ++ pr_id id ++ expl)
+  user_err  (str "No such bound variable " ++ Id.print id ++ expl)
 
 let evar_with_name holes id =
   let map h = match h.hole_name with
@@ -655,7 +655,7 @@ let evar_with_name holes id =
   | [h] -> h.hole_evar
   | _ ->
     user_err 
-      (str "Binder name \"" ++ pr_id id ++
+      (str "Binder name \"" ++ Id.print id ++
         str "\" occurs more than once in clause.")
 
 let evar_of_binder holes = function
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 9c69995f4..9a2026dd3 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -11,7 +11,7 @@
     evar-based clauses. *)
 
 open Names
-open Term
+open Constr
 open Environ
 open Evd
 open EConstr
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 4a92c3856..8bd5d98cb 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -54,9 +54,10 @@ let clenv_value_cast_meta clenv =
 
 let clenv_pose_dependent_evars with_evars clenv =
   let dep_mvs = clenv_dependent clenv in
+  let env, sigma = clenv.env, clenv.evd in
   if not (List.is_empty dep_mvs) && not with_evars then
     raise
-      (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
+      (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
 (** Use our own fast path, more informative than from Typeclasses *)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index a0e3b718a..d90cff572 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -14,5 +14,5 @@ open Ltac_pretype
 
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 
-val w_refine : evar * evar_info ->
+val w_refine : Evar.t * evar_info ->
   glob_constr_ltac_closure -> evar_map -> evar_map
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 61f3e4a02..d5bc7e0ce 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -16,7 +16,7 @@ module NamedDecl = Context.Named.Declaration
    evar is defined in the current evar_map, should not be accessed. *)
 
 (* type of the goals *)
-type goal = Evd.evar
+type goal = Evar.t
 
 let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e)
 
@@ -99,7 +99,7 @@ module V82 = struct
   let same_goal evars1 gl1 evars2 gl2 =
     let evi1 = Evd.find evars1 gl1 in
     let evi2 = Evd.find evars2 gl2 in
-    Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
+    Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl &&
     Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
 
   let weak_progress glss gls =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index ad968cdfb..37dd9d3c0 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -58,7 +58,7 @@ module V82 : sig
 
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-    
+
  (* Principal part of tclNOTSAMEGOAL *)
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 20d075ae1..1d86a0909 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -11,7 +11,7 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Term
+open Constr
 open Vars
 open Termops
 open Environ
@@ -40,7 +40,7 @@ type refiner_error =
   | DoesNotOccurIn of constr * Id.t
   | NoSuchHyp of Id.t
 
-exception RefinerError of refiner_error
+exception RefinerError of Environ.env * Evd.evar_map * refiner_error
 
 open Pretype_errors
 
@@ -69,7 +69,7 @@ let catchable_exception = function
   | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e 
   | _ -> false
 
-let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id))
+let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id))
 
 (* Tells if the refiner should check that the submitted rules do not
    produce invalid subgoals *)
@@ -78,10 +78,10 @@ let with_check = Flags.with_option check
 
 (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
    returns [tail::(f head (id,_,_) (rev tail))] *)
-let apply_to_hyp check sign id f =
+let apply_to_hyp env sigma check sign id f =
   try apply_to_hyp sign id f
   with Hyp_not_found ->
-    if check then error_no_such_hypothesis id
+    if check then error_no_such_hypothesis env sigma id
     else sign
 
 let check_typability env sigma c =
@@ -139,15 +139,15 @@ let reorder_context env sigma sign ord =
           let ((d,h),mh) = find_q top moved_hyps in
           if occur_vars_in_decl env sigma h d then
             user_err ~hdr:"reorder_context"
-              (str "Cannot move declaration " ++ pr_id top ++ spc() ++
+              (str "Cannot move declaration " ++ Id.print top ++ spc() ++
               str "before " ++
-              pr_sequence pr_id
+              pr_sequence Id.print
                 (Id.Set.elements (Id.Set.inter h
                   (global_vars_set_of_decl env sigma d))));
           step ord' expected ctxt_head mh (d::ctxt_tail)
       | _ ->
           (match ctxt_head with
-            | [] -> error_no_such_hypothesis (List.hd ord)
+            | [] -> error_no_such_hypothesis env sigma (List.hd ord)
             | d :: ctxt ->
                 let x = NamedDecl.get_id d in
                 if Id.Set.mem x expected then
@@ -172,7 +172,7 @@ let check_decl_position env sigma sign d =
   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);
+      (str "Cannot create self-referring hypothesis " ++ Id.print x);
   x::deps
 
 (* Auxiliary functions for primitive MOVE tactic
@@ -190,9 +190,9 @@ let move_location_eq m1 m2 = match m1, m2 with
 | MoveFirst, MoveFirst -> true
 | _ -> false
 
-let split_sign hfrom hto l =
+let split_sign env sigma hfrom hto l =
   let rec splitrec left toleft = function
-    | [] -> error_no_such_hypothesis hfrom
+    | [] -> error_no_such_hypothesis env sigma hfrom
     | d :: right ->
         let hyp = NamedDecl.get_id d in
       	if Id.equal hyp hfrom then
@@ -222,7 +222,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
   let rec moverec first middle = function
     | [] ->
 	if match hto with MoveFirst | MoveLast -> false | _ -> true then
-	  error_no_such_hypothesis (hyp_of_move_location hto);
+          error_no_such_hypothesis env sigma (hyp_of_move_location hto);
 	List.rev first @ List.rev middle
     | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
 	List.rev first @ List.rev middle @ right
@@ -233,10 +233,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
-	        Miscprint.pr_move_location pr_id hto ++
+	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
+	        Miscprint.pr_move_location Id.print hto ++
 	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
-	        ++ pr_id hyp ++ str ".")
+	        ++ Id.print hyp ++ str ".")
           else
 	    (d::first, middle)
 	in
@@ -258,10 +258,10 @@ let move_hyp sigma 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 sigma hfrom hto sign =
+let move_hyp_in_named_context env sigma hfrom hto sign =
   let open EConstr in
   let (left,right,declfrom,toleft) =
-    split_sign hfrom hto (named_context_of_val sign) in
+    split_sign env sigma hfrom hto (named_context_of_val sign) in
   move_hyp sigma toleft (left,declfrom,right) hto
 
 let insert_decl_in_named_context sigma decl hto sign =
@@ -284,24 +284,24 @@ let error_unsupported_deep_meta c =
     strbrk "supported; try \"refine\" instead.")
 
 let collect_meta_variables c =
-  let rec collrec deep acc c = match kind_of_term c with
+  let rec collrec deep acc c = match kind c with
     | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
     | Cast(c,_,_) -> collrec deep acc c
-    | (App _| Case _) -> Term.fold_constr (collrec deep) acc c
+    | (App _| Case _) -> Constr.fold (collrec deep) acc c
     | Proj (_, c) -> collrec deep acc c
-    | _ -> Term.fold_constr (collrec true) acc c
+    | _ -> Constr.fold (collrec true) acc c
   in
   List.rev (collrec false [] c)
 
-let check_meta_variables c =
+let check_meta_variables env sigma c =
   if not (List.distinct_f Int.compare (collect_meta_variables c)) then
-    raise (RefinerError (NonLinearProof c))
+    raise (RefinerError (env, sigma, NonLinearProof c))
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
     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 raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
   else sigma
 
 exception Stop of EConstr.t list
@@ -332,11 +332,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       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
+      match kind trm with
       | Meta _ ->
 	let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
 	  if !check && occur_meta sigma conclty then
-	    raise (RefinerError (MetaInType conclty));
+            raise (RefinerError (env, sigma, 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
@@ -372,7 +372,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
         let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
-        let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+        let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
         (acc'',conclty',sigma, ans)
 
       | Proj (p,c) ->
@@ -394,7 +394,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else Term.mkCase (ci,p',c',lf')
+          else mkCase (ci,p',c',lf')
         in
 	(acc'',conclty',sigma, ans)
 
@@ -413,7 +413,7 @@ and mk_hdgoals sigma goal goalacc trm =
   let hyps = Goal.V82.hyps sigma goal in
   let mk_goal hyps concl = 
     Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
-  match kind_of_term trm with
+  match kind trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
 	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
@@ -433,7 +433,7 @@ and mk_hdgoals sigma goal goalacc trm =
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
-        let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+        let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
 	(acc'',conclty',sigma, ans)
 
     | Case (ci,p,c,lf) ->
@@ -447,7 +447,7 @@ and mk_hdgoals sigma goal goalacc trm =
 	let lf' = Array.rev_of_list rbranches in
 	let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else Term.mkCase (ci,p',c',lf')
+          else mkCase (ci,p',c',lf')
 	in
 	(acc'',conclty',sigma, ans)
 
@@ -468,16 +468,18 @@ and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
     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
+    let rec collapse t = match kind t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
     in
     let t = collapse t in
-    match kind_of_term t with
+    match kind t with
     | Prod (_, c1, b) ->
       let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in
       (acc, subst1 harg b, sigma), arg
-    | _ -> raise (RefinerError (CannotApply (t, harg)))
+    | _ ->
+      let env = Goal.V82.env sigma goal in
+      raise (RefinerError (env,sigma,CannotApply (t, harg)))
   in
   Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs
 
@@ -497,36 +499,35 @@ and mk_casegoals sigma goal goalacc p c =
 let convert_hyp check sign sigma d =
   let id = NamedDecl.get_id d in
   let b = NamedDecl.get_value d in
-  let env = Global.env() in
+  let env = Global.env () in
   let reorder = ref [] in
   let sign' =
-    apply_to_hyp check sign id
+    apply_to_hyp env sigma check sign id
       (fun _ d' _ ->
         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) (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 ".");
+            (str "Incorrect change of the type of " ++ Id.print 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 ".");
+            (str "Incorrect change of the body of "++ Id.print id ++ str ".");
        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
 
-
-
 (************************************************************************)
 (************************************************************************)
 (* Primitive tactics are handled here *)
 
 let prim_refiner r sigma goal =
+  let env = Goal.V82.env sigma goal in
   let cl = Goal.V82.concl sigma goal in
   match r with
     (* Logical rules *)
     | Refine c ->
         let cl = EConstr.Unsafe.to_constr cl in
-	check_meta_variables c;
+        check_meta_variables env sigma 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 (EConstr.of_constr oterm) in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 9d0756b33..afd1ecf70 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -9,7 +9,7 @@
 (** Legacy proof engine. Do not use in newly written code. *)
 
 open Names
-open Term
+open Constr
 open Evd
 open Proof_type
 
@@ -50,16 +50,16 @@ type refiner_error =
   | DoesNotOccurIn of constr * Id.t
   | NoSuchHyp of Id.t
 
-exception RefinerError of refiner_error
+exception RefinerError of Environ.env * evar_map * refiner_error
 
-val error_no_such_hypothesis : Id.t -> 'a
+val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
 
 val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   EConstr.named_declaration -> Environ.named_context_val
 
-val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
+val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
   Environ.named_context_val -> Environ.named_context_val
 
 val insert_decl_in_named_context : Evd.evar_map ->
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index 5d37c8a02..92b58b409 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -6,8 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Misctypes
 open Pp
+open Names
+open Misctypes
 
 (** Printing of [intro_pattern] *)
 
@@ -18,8 +19,8 @@ let rec pr_intro_pattern prc (_,pat) = match pat with
   | IntroAction p -> pr_intro_pattern_action prc p
 
 and pr_intro_pattern_naming = function
-  | IntroIdentifier id -> Nameops.pr_id id
-  | IntroFresh id -> str "?" ++ Nameops.pr_id id
+  | IntroIdentifier id -> Id.print id
+  | IntroFresh id -> str "?" ++ Id.print id
   | IntroAnonymous -> str "?"
 
 and pr_intro_pattern_action prc = function
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 469e1a011..6b503a011 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -51,9 +51,8 @@ end
 
 let get_nth_V82_goal i =
   let p = Proof_global.give_me_the_proof () in
-  let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
-  try
-          { it=(List.nth goals (i-1)) ; sigma=sigma; }
+  let goals,_,_,_,sigma = Proof.proof p in
+  try { it = List.nth goals (i-1) ; sigma }
   with Failure _ -> raise NoSuchGoal
 
 let get_goal_context_gen i =
@@ -141,7 +140,8 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     Proof_global.discard_current ();
-    const, status, fst univs
+    let univs = UState.demote_seff_univs const univs in
+    const, status, univs
   with reraise ->
     let reraise = CErrors.push reraise in
     Proof_global.discard_current ();
@@ -230,31 +230,3 @@ let apply_implicit_tactic tac = (); fun env sigma evk ->
 let solve_by_implicit_tactic () = match !implicit_tactic with
 | None -> None
 | Some tac -> Some (apply_implicit_tactic tac)
-
-(** Deprecated functions  *)
-let refining = Proof_global.there_are_pending_proofs
-let check_no_pending_proofs = Proof_global.check_no_pending_proof
-
-let get_current_proof_name = Proof_global.get_current_proof_name
-let get_all_proof_names = Proof_global.get_all_proof_names
-
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-
-let delete_proof = Proof_global.discard
-let delete_current_proof = Proof_global.discard_current
-let delete_all_proofs = Proof_global.discard_all
-
-let get_pftreestate () =
-  Proof_global.give_me_the_proof ()
-
-let set_end_tac tac =
-  Proof_global.set_endline_tactic tac
-
-let set_used_variables l =
-  Proof_global.set_used_variables l
-
-let get_used_variables () =
-  Proof_global.get_used_variables ()
-
-let get_universe_decl () =
-  Proof_global.get_universe_decl ()
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6e4ecd13b..5a317a956 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -8,9 +8,8 @@
 
 (** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
 
-open Loc
 open Names
-open Term
+open Constr
 open Environ
 open Decl_kinds
 
@@ -36,11 +35,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 (** {6 ... } *)
 (** [get_goal_context n] returns the context of the [n]th subgoal of
@@ -75,7 +74,7 @@ val current_proof_statement :
 
 val solve : ?with_end_tac:unit Proofview.tactic ->
       Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
-      Proof.proof -> Proof.proof*bool
+      Proof.t -> Proof.t * bool
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
     focused proof or raises a UserError if there is no focused proof or
@@ -96,14 +95,14 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
     tactic. *)
 
 val build_constant_by_tactic :
-  Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
+  Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
   EConstr.types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool *
-    Evd.evar_universe_context
+    UState.t
 
-val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
+val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
   EConstr.types -> unit Proofview.tactic -> 
-  constr * bool * Evd.evar_universe_context
+  constr * bool * UState.t
 
 val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
   constr * Evd.evar_map
@@ -122,84 +121,3 @@ val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
 val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
-
-(** {5 Deprecated functions in favor of [Proof_global]} *)
-
-(** {6 ... } *)
-(** Several proofs can be opened simultaneously but at most one is
-   focused at some time. The following functions work by side-effect
-   on current set of open proofs. In this module, ``proofs'' means an
-   open proof (something started by vernacular command [Goal], [Lemma]
-   or [Theorem]), and ``goal'' means a subgoal of the current focused
-   proof *)
-
-(** [refining ()] tells if there is some proof in progress, even if a not
-   focused one *)
-
-val refining : unit -> bool
-[@@ocaml.deprecated "use Proof_global.there_are_pending_proofs"]
-
-(** [check_no_pending_proofs ()] fails if there is still some proof in
-   progress *)
-
-val check_no_pending_proofs : unit -> unit
-[@@ocaml.deprecated "use Proof_global.check_no_pending_proofs"]
-
-(** {6 ... } *)
-(** [delete_proof name] deletes proof of name [name] or fails if no proof
-    has this name *)
-
-val delete_proof : Id.t located -> unit
-[@@ocaml.deprecated "use Proof_global.discard"]
-
-(** [delete_current_proof ()] deletes current focused proof or fails if
-    no proof is focused *)
-
-val delete_current_proof : unit -> unit
-[@@ocaml.deprecated "use Proof_global.discard_current"]
-
-(** [delete_all_proofs ()] deletes all open proofs if any *)
-val delete_all_proofs : unit -> unit
-[@@ocaml.deprecated "use Proof_global.discard_all"]
-
-(** [get_pftreestate ()] returns the current focused pending proof.
-   @raise NoCurrentProof if there is no pending proof. *)
-
-val get_pftreestate : unit -> Proof.proof
-[@@ocaml.deprecated "use Proof_global.give_me_the_proof"]
-
-(** {6 ... } *)
-(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
-    by [solve] *)
-
-val set_end_tac : Genarg.glob_generic_argument -> unit
-[@@ocaml.deprecated "use Proof_global.set_endline_tactic"]
-
-(** {6 ... } *)
-(** [set_used_variables l] declares that section variables [l] will be
-    used in the proof *)
-val set_used_variables :
-  Id.t list -> Context.Named.t * Names.Id.t Loc.located list
-[@@ocaml.deprecated "use Proof_global.set_used_variables"]
-
-val get_used_variables : unit -> Context.Named.t option
-[@@ocaml.deprecated "use Proof_global.get_used_variables"]
-
-(** {6 Universe binders } *)
-val get_universe_decl : unit -> Univdecls.universe_decl
-[@@ocaml.deprecated "use Proof_global.get_universe_decl"]
-
-(** {6 ... } *)
-(** [get_current_proof_name ()] return the name of the current focused
-    proof or failed if no proof is focused *)
-val get_current_proof_name : unit -> Id.t
-[@@ocaml.deprecated "use Proof_global.get_current_proof_name"]
-
-(** [get_all_proof_names ()] returns the list of all pending proof names.
-    The first name is the current proof, the other names may come in
-    any order. *)
-val get_all_proof_names : unit -> Id.t list
-[@@ocaml.deprecated "use Proof_global.get_all_proof_names"]
-
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-[@@ocaml.deprecated "use Proof_global.lemma_possible_guards"]
diff --git a/proofs/proof.ml b/proofs/proof.ml
index ba4980b66..04e707cd6 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -98,7 +98,7 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
    are under control of the undo mechanism *)
-type proof = {
+type t = {
   (* Current focused proofview *)
   proofview: Proofview.proofview;
   (* Entry for the proofview *)
@@ -112,9 +112,11 @@ type proof = {
   (* List of goals that have been given up *)
   given_up : Goal.goal list;
   (* The initial universe context (for the statement) *)
-  initial_euctx : Evd.evar_universe_context
+  initial_euctx : UState.t
 }
 
+type proof = t
+
 (*** General proof functions ***)
 
 let proof p =
@@ -163,6 +165,7 @@ let map_structured_proof pfts process_goal: 'a pre_goals =
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
+
 (* spiwack: a proof is considered completed even if its still focused, if the focus
    doesn't hide any goal.
    Unfocusing is handled in {!return}. *)
@@ -391,10 +394,12 @@ let pr_proof p =
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
   let subgoals p =
-    Proofview.V82.goals p.proofview
+    let it, sigma = Proofview.proofview p.proofview in
+    Evd.{ it; sigma }
 
   let background_subgoals p =
-    Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
+    let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in
+    Evd.{ it; sigma }
 
   let top_goal p =
     let { Evd.it=gls ; sigma=sigma; } =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 698aa48b0..0b5e771ef 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -30,7 +30,9 @@
 *)
 
 (* Type of a proof. *)
-type proof
+type t
+type proof = t
+[@@ocaml.deprecated "please use [Proof.t]"]
 
 (* Returns a stylised view of a proof for use by, for instance,
    ide-s. *)
@@ -42,7 +44,7 @@ type proof
    shelf (the list of goals on the shelf), a representation of the
    given up goals (the list of the given up goals) and the underlying
    evar_map *)
-val proof : proof ->
+val proof : t ->
   Goal.goal list
   * (Goal.goal list * Goal.goal list) list
   * Goal.goal list
@@ -61,27 +63,26 @@ type 'a pre_goals = {
   (** List of the goals that have been given up *)
 }
 
-val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
+val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
 
 
 (*** General proof functions ***)
-
-val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
-val dependent_start : Proofview.telescope -> proof
-val initial_goals : proof -> (EConstr.constr * EConstr.types) list
-val initial_euctx : proof -> Evd.evar_universe_context
+val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t
+val dependent_start : Proofview.telescope -> t
+val initial_goals : t -> (EConstr.constr * EConstr.types) list
+val initial_euctx : t -> UState.t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
-val is_done : proof -> bool
+val is_done : t -> bool
 
 (* Like is_done, but this time it really means done (i.e. nothing left to do) *)
-val is_complete : proof -> bool
+val is_complete : t -> bool
 
 (* Returns the list of partial proofs to initial goals. *)
-val partial_proof : proof -> EConstr.constr list
+val partial_proof : t -> EConstr.constr list
 
-val compact : proof -> proof
+val compact : t -> t
 
 (* Returns the proofs (with their type) of the initial goals.
     Raises [UnfinishedProof] is some goals remain to be considered.
@@ -92,7 +93,7 @@ exception UnfinishedProof
 exception HasShelvedGoals
 exception HasGivenUpGoals
 exception HasUnresolvedEvar
-val return : proof -> Evd.evar_map
+val return : t -> Evd.evar_map
 
 (*** Focusing actions ***)
 
@@ -132,7 +133,7 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
 (* focus command (focuses on the [i]th subgoal) *)
 (* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
    a need for it? *)
-val focus : 'a focus_condition -> 'a -> int -> proof -> proof
+val focus : 'a focus_condition -> 'a -> int -> t -> t
 
 exception FullyUnfocused
 exception CannotUnfocusThisWay
@@ -148,58 +149,59 @@ exception NoSuchGoals of int * int
    Raises [FullyUnfocused] if the proof is not focused.
    Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
      is not met. *)
-val unfocus : 'a focus_kind -> proof -> unit -> proof
+val unfocus : 'a focus_kind -> t -> unit -> t
 
 (* [unfocused p] returns [true] when [p] is fully unfocused. *)
-val unfocused : proof -> bool
+val unfocused : t -> bool
 
 (* [get_at_focus k] gets the information stored at the closest focus point
     of kind [k].
     Raises [NoSuchFocus] if there is no focus point of kind [k]. *)
 exception NoSuchFocus
-val get_at_focus : 'a focus_kind -> proof -> 'a
+val get_at_focus : 'a focus_kind -> t -> 'a
 
 (* [is_last_focus k] check if the most recent focus is of kind [k] *)
-val is_last_focus : 'a focus_kind -> proof -> bool
+val is_last_focus : 'a focus_kind -> t -> bool
 
 (* returns [true] if there is no goal under focus. *)
-val no_focused_goal : proof -> bool
+val no_focused_goal : t -> bool
 
 (*** Tactics ***)
 
 (* the returned boolean signal whether an unsafe tactic has been
    used. In which case it is [false]. *)
 val run_tactic : Environ.env ->
-  unit Proofview.tactic -> proof -> proof*(bool*Proofview_monad.Info.tree)
+  unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
 
-val maximal_unfocus : 'a focus_kind -> proof -> proof
+val maximal_unfocus : 'a focus_kind -> t -> t
 
 (*** Commands ***)
 
-val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
+val in_proof : t -> (Evd.evar_map -> 'a) -> 'a
 
 (* Remove all the goals from the shelf and adds them at the end of the
    focused goals. *)
-val unshelve : proof -> proof
+val unshelve : t -> t
 
-val pr_proof : proof -> Pp.t
+val pr_proof : t -> Pp.t
 
 (*** Compatibility layer with <=v8.2 ***)
 module V82 : sig
-  val subgoals : proof -> Goal.goal list Evd.sigma
+  val subgoals : t -> Goal.goal list Evd.sigma
+  [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
 
   (* All the subgoals of the proof, including those which are not focused. *)
-  val background_subgoals : proof -> Goal.goal list Evd.sigma
+  val background_subgoals : t -> Goal.goal list Evd.sigma
 
-  val top_goal : proof -> Goal.goal Evd.sigma
+  val top_goal : t -> Goal.goal Evd.sigma
 
   (* returns the existential variable used to start the proof *)
-  val top_evars : proof -> Evd.evar list
+  val top_evars : t -> Evar.t list
 
   (* Turns the unresolved evars into goals.
      Raises [UnfinishedProof] if there are still unsolved goals. *)
-  val grab_evars : proof -> proof
+  val grab_evars : t -> t
 
   (* Implements the Existential command *)
-  val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> proof
+  val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t
 end
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 4f575ab4b..214916331 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -25,8 +25,8 @@ let pr_bullet b =
 
 type behavior = {
   name : string;
-  put : proof -> t -> proof;
-  suggest: proof -> Pp.t
+  put : Proof.t -> t -> Proof.t;
+  suggest: Proof.t -> Pp.t
 }
 
 let behaviors = Hashtbl.create 4
@@ -110,7 +110,7 @@ module Strict = struct
   let push (b:t) pr =
     focus bullet_cond (b::get_bullets pr) 1 pr
 
-  let suggest_bullet (prf : proof): suggestion =
+  let suggest_bullet (prf : Proof.t): suggestion =
     if is_done prf then ProofFinished
     else if not (no_focused_goal prf)
     then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
@@ -137,7 +137,7 @@ module Strict = struct
       in
       loop prf
 
-  let rec pop_until (prf : proof) bul : proof =
+  let rec pop_until (prf : Proof.t) bul : Proof.t =
     let prf', b = pop prf in
     if bullet_eq bul b then prf'
     else pop_until prf' bul
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 9e924fec9..09fcabf50 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -12,8 +12,6 @@
 (*                                                        *)
 (**********************************************************)
 
-open Proof
-
 type t = Vernacexpr.bullet
 
 (** A [behavior] is the data of a put function which
@@ -22,8 +20,8 @@ type t = Vernacexpr.bullet
     with a name to identify the behavior. *)
 type behavior = {
   name : string;
-  put : proof -> t -> proof;
-  suggest: proof -> Pp.t
+  put : Proof.t -> t -> Proof.t;
+  suggest: Proof.t -> Pp.t
 }
 
 (** A registered behavior can then be accessed in Coq
@@ -39,8 +37,8 @@ val register_behavior : behavior -> unit
 
 (** Handles focusing/defocusing with bullets:
      *)
-val put : proof -> t -> proof
-val suggest : proof -> Pp.t
+val put : Proof.t -> t -> Proof.t
+val suggest : Proof.t -> Pp.t
 
 (**********************************************************)
 (*                                                        *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 621178982..167d6bda0 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,17 +68,16 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  universes: proof_universes;
+  universes: UState.t;
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
@@ -90,12 +89,15 @@ type pstate = {
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Context.Named.t option;
-  proof : Proof.proof;
+  proof : Proof.t;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
   universe_decl: Univdecls.universe_decl;
 }
 
+type t = pstate list
+type state = t
+
 let make_terminator f = f
 let apply_terminator f = f
 
@@ -185,7 +187,7 @@ let msg_proofs () =
   match get_all_proof_names () with
     | [] -> (spc () ++ str"(No proof-editing in progress).")
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (pr_sequence Nameops.pr_id l) ++ str".")
+               (pr_sequence Id.print l) ++ str".")
 
 let there_is_a_proof () = not (List.is_empty !pstates)
 let there_are_pending_proofs () = there_is_a_proof ()
@@ -316,11 +318,7 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
-let constrain_variables init uctx =
-  let levels = Univ.Instance.levels (Univ.UContext.instance init) in
-  UState.constrain_variables levels uctx
-
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) =
@@ -329,10 +327,11 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
+  let constrain_variables ctx =
+    UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
+  in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
-  let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in
-  let binders = if poly then Some binders else None in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
@@ -348,20 +347,21 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
 	  if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
 	    nf t
 	  else t
-	in
-        let used_univs_body = Univops.universes_of_constr body in
-        let used_univs_typ = Univops.universes_of_constr typ in
+        in
+        let env = Global.env () in
+        let used_univs_body = Univops.universes_of_constr env body in
+        let used_univs_typ = Univops.universes_of_constr env typ in
         if keep_body_ucst_separate ||
            not (Safe_typing.empty_private_constants = eff) then
-          let initunivs = Evd.evar_context_universe_context initial_euctx in
-          let ctx = constrain_variables initunivs universes in
+          let initunivs = UState.const_univ_entry ~poly initial_euctx in
+          let ctx = constrain_variables universes in
           (* For vi2vo compilation proofs are computed now but we need to
              complement the univ constraints of the typ with the ones of
              the body.  So we keep the two sets distinct. *)
-	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx_body = UState.restrict ctx used_univs in
-          let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in
-          (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
+          let univs = UState.check_mono_univ_decl ctx_body universe_decl in
+          (initunivs, typ), ((body, univs), eff)
         else
           (* Since the proof is computed now, we can simply have 1 set of
              constraints in which we merge the ones for the body and the ones
@@ -370,30 +370,28 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
              TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx = UState.restrict universes used_univs in
-          let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
+          let univs = UState.check_univ_decl ~poly ctx universe_decl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
        fun t p -> Future.split2 (Future.chain p (make_body t))
     else
       fun t p ->
+        (* Already checked the univ_decl for the type universes when starting the proof. *)
+        let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in
         Future.from_val (univctx, nf t),
         Future.chain p (fun (pt,eff) ->
           (* Deferred proof, we already checked the universe declaration with
              the initial universes, ensure that the final universes respect
              the declaration as well. If the declaration is non-extensible,
              this will prevent the body from adding universes and constraints. *)
-          let bodyunivs = constrain_variables univctx (Future.force univs) in
-          let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in
-          (pt,Univ.ContextSet.of_context univs),eff)
+          let bodyunivs = constrain_variables (Future.force univs) in
+          let univs = UState.check_mono_univ_decl bodyunivs universe_decl in
+          (pt,univs),eff)
   in
   let entry_fn 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
-    let univs =
-      if poly then Entries.Polymorphic_const_entry univs
-      else Entries.Monomorphic_const_entry univs
-    in
     {Entries.
       const_entry_body = body;
       const_entry_secctx = section_vars;
@@ -405,7 +403,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   in
   let entries = Future.map2 entry_fn fpl initial_goals in
   { id = pid; entries = entries; persistence = strength;
-    universes = (universes, binders) },
+    universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
 let return_proof ?(allow_partial=false) () =
@@ -466,8 +464,6 @@ module V82 = struct
     pid, (goals, strength)
 end
 
-type state = pstate list
-        
 let freeze ~marshallable =
   match marshallable with
   | `Yes ->
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 8c0f6ad85..27e99f218 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -10,6 +10,10 @@
      toplevel. In particular it defines the global proof
      environment. *)
 
+type t
+type state = t
+[@@ocaml.deprecated "please use [Proof_global.t]"]
+
 val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
 
@@ -21,7 +25,7 @@ val discard_current : unit -> unit
 val discard_all : unit -> unit
 
 exception NoCurrentProof
-val give_me_the_proof : unit -> Proof.proof
+val give_me_the_proof : unit -> Proof.t
 (** @raise NoCurrentProof when outside proof mode. *)
 
 val compact_the_proof : unit -> unit
@@ -33,18 +37,17 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  universes: proof_universes;
+  universes: UState.t;
 }
 
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
-		  proof_universes
+                UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
@@ -86,7 +89,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
@@ -107,9 +110,9 @@ val get_open_goals : unit -> int
     no current proof.
     The return boolean is set to [false] if an unsafe tactic has been used. *)
 val with_current_proof :
-  (unit Proofview.tactic -> Proof.proof -> Proof.proof*'a) -> 'a
+  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 val simple_with_current_proof :
-  (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
+  (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
 val set_endline_tactic : Genarg.glob_generic_argument -> unit
@@ -129,11 +132,10 @@ module V82 : sig
   Decl_kinds.goal_kind)
 end
 
-type state
-val freeze : marshallable:[`Yes | `No | `Shallow] -> state
-val unfreeze : state -> unit
-val proof_of_state : state -> Proof.proof
-val copy_terminators : src:state -> tgt:state -> state
+val freeze : marshallable:[`Yes | `No | `Shallow] -> t
+val unfreeze : t -> unit
+val proof_of_state : t -> Proof.t
+val copy_terminators : src:t -> tgt:t -> t
 
 
 (**********************************************************)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 2ad5f607f..20293cb9b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -9,7 +9,7 @@
 (** Legacy proof engine. Do not use in newly written code. *)
 
 open Evd
-open Term
+open Constr
 
 (** This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 6052ba367..9a5d4e154 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -25,8 +25,11 @@ 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
-  Vnorm.cbv_vm env sigma c ctyp
+  if Coq_config.bytecode_compiler then
+    let ctyp = Retyping.get_type_of env sigma c in
+    Vnorm.cbv_vm env sigma c ctyp
+  else
+    compute env sigma c
 
 let warn_native_compute_disabled =
   CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
@@ -34,12 +37,12 @@ let warn_native_compute_disabled =
    strbrk "native_compute disabled at configure time; falling back to vm_compute.")
 
 let cbv_native env sigma c =
-  if Coq_config.no_native_compiler then
-    (warn_native_compute_disabled ();
-     cbv_vm env sigma c)
-  else
+  if Coq_config.native_compiler then
     let ctyp = Retyping.get_type_of env sigma c in
     Nativenorm.native_norm env sigma c ctyp
+  else
+    (warn_native_compute_disabled ();
+     cbv_vm env sigma c)
 
 let whd_cbn flags env sigma t =
   let (state,_) =
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index ccc2440a2..43e598773 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -9,7 +9,7 @@
 (** Interpretation layer of redexprs such as hnf, cbv, etc. *)
 
 open Names
-open Term
+open Constr
 open EConstr
 open Pattern
 open Genredexpr
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 3b0a9e5b6..cfdcde36e 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -17,7 +17,7 @@ open Proofview
 
 (** Printer used to print the constr which refine refines. *)
 val pr_constr :
-  (Environ.env -> Evd.evar_map -> Term.constr -> Pp.t) Hook.t
+  (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t
 
 (** {7 Refinement primitives} *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3e3313eb5..cd2b10906 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -30,8 +30,8 @@ let refiner pr goal_sigma =
 (* Profiling refiner *)
 let refiner = 
   if Flags.profile then
-    let refiner_key = Profile.declare_profile "refiner" in
-      Profile.profile2 refiner_key refiner
+    let refiner_key = CProfile.declare_profile "refiner" in
+      CProfile.profile2 refiner_key refiner
   else refiner
 
 (*********************)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 3ff010fe3..52dc8bfd8 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -35,12 +35,12 @@ val tclIDTAC_MESSAGE  : Pp.t -> tactic
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
-val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+val tclEVARUNIVCONTEXT : UState.t -> tactic
 
-val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic
-val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic
+val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
 
-val tclPUSHCONSTRAINTS : Univ.constraints -> tactic
+val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic
 
 (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a8ec4d8ca..d41541251 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -55,10 +55,11 @@ let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
 let pf_get_hyp gls id =
+  let env, sigma = pf_env gls, project gls in
   try
     Context.Named.lookup id (pf_hyps gls)
   with Not_found ->
-    raise (RefinerError (NoSuchHyp id))
+    raise (RefinerError (env, sigma, NoSuchHyp id))
 
 let pf_get_hyp_typ gls id =
   id |> pf_get_hyp gls |> NamedDecl.get_type
@@ -102,9 +103,6 @@ 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 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 *)
 (********************************************)
@@ -185,9 +183,10 @@ module New = struct
 
   let pf_get_hyp id gl =
     let hyps = Proofview.Goal.env gl in
+    let sigma = project gl in
     let sign =
       try EConstr.lookup_named id hyps
-      with Not_found -> raise (RefinerError (NoSuchHyp id))
+      with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id))
     in
     sign
 
@@ -223,8 +222,6 @@ module New = struct
   let pf_hnf_type_of gl t =
     pf_whd_all gl (pf_get_type_of gl t)
 
-  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
-
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index de9f8e700..e0fb8fbc5 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -7,19 +7,19 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open EConstr
-open Evd
 open Proof_type
 open Redexpr
-open Pattern
 open Locus
-open Ltac_pretype
 
 (** Operations for handling terms under a local typing context. *)
 
-type 'a sigma   = 'a Evd.sigma;;
+type 'a sigma   = 'a Evd.sigma
+[@@ocaml.deprecated "alias of Evd.sigma"]
+
+open Evd
 type tactic     = Proof_type.tactic;;
 
 val sig_it  : 'a sigma   -> 'a
@@ -77,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
-val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
-
-
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
@@ -136,8 +132,6 @@ module New : sig
   val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr
   val pf_compute : 'a Proofview.Goal.t -> constr -> constr
 
-  val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
-
   val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
 
 end