From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 vernac/lemmas.ml | 30 +++++++++++++-----------------
 1 file changed, 13 insertions(+), 17 deletions(-)

(limited to 'vernac/lemmas.ml')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 30dd6ec7..880a11be 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,7 +34,7 @@ open Impargs
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
+type 'a declaration_hook = Decl_kinds.locality -> GlobRef.t -> 'a
 let mk_hook hook = hook
 let call_hook fix_exn hook l c =
   try hook l c
@@ -71,17 +71,13 @@ let adjust_guardness_conditions const = function
 	  List.interval 0 (List.length ((lam_assum c))))
 	  lemma_guard (Array.to_list fixdefs) in
 *)
-              let add c cb e =
-                let exists c e =
-                  try ignore(Environ.lookup_constant c e); true
-                  with Not_found -> false in 
-                if exists c e then e else Environ.add_constant c cb e in
-              let env = List.fold_left (fun env { eff } ->
-                match eff with
-                | SEsubproof (c, cb,_) -> add c cb env
-                | SEscheme (l,_) ->
-                    List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
-                env (Safe_typing.side_effects_of_private_constants eff) in
+              let fold env eff =
+                try
+                  let _ = Environ.lookup_constant eff.seff_constant env in
+                  env
+                with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+              in
+              let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
                 search_guard env
                   possible_indexes fixdecls in
@@ -334,8 +330,8 @@ let universe_proof_terminator compute_guard hook =
       Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff = match opaque with
-        | Vernacexpr.Transparent -> false, true
-        | Vernacexpr.Opaque      -> true, false
+        | Transparent -> false, true
+        | Opaque      -> true, false
       in
       let proof = get_proof proof compute_guard
         (hook (Some (proof.Proof_global.universes))) is_opaque in
@@ -436,7 +432,7 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook =
 let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
-  let evd, decl = Univdecls.interp_univ_decl_opt env0 (snd decl) in
+  let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
   let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
     let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in
     let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
@@ -451,12 +447,12 @@ let start_proof_com ?inference_hook kind thms hook =
            (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
       evd thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in
-  let evd, _nf = Evarutil.nf_evars_and_universes evd in
+  let evd = Evd.minimize_universes evd in
   (* XXX: This nf_evar is critical too!! We are normalizing twice if
      you look at the previous lines... *)
   let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in
   let () =
-    let open Misctypes in
+    let open UState in
     if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
        ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl)
   in
-- 
cgit v1.2.3