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/comDefinition.ml | 48 ++++++++++++++++--------------------------------
 1 file changed, 16 insertions(+), 32 deletions(-)

(limited to 'vernac/comDefinition.ml')

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b18a60a1..60f9d674 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -10,39 +10,19 @@
 
 open Pp
 open Util
-open Constr
-open Environ
 open Entries
 open Redexpr
 open Declare
 open Constrintern
 open Pretyping
 
-open Context.Rel.Declaration
-
 (* Commands of the interface: Constant definitions *)
 
-let rec under_binders env sigma f n c =
-  if Int.equal n 0 then f env sigma (EConstr.of_constr c) else
-    match Constr.kind c with
-      | Lambda (x,t,c) ->
-          mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c)
-      | LetIn (x,b,t,c) ->
-          mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c)
-      | _ -> assert false
-
-let red_constant_entry n ce sigma = function
-  | None -> ce
+let red_constant_body red_opt env sigma body = match red_opt with
+  | None -> sigma, body
   | Some red ->
-      let proof_out = ce.const_entry_body in
-      let env = Global.env () in
-      let (redfun, _) = reduction_of_red_expr env red in
-      let redfun env sigma c =
-        let (_, c) = redfun env sigma c in
-        EConstr.Unsafe.to_constr c
-      in
-      { ce with const_entry_body = Future.chain proof_out
-        (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
+    let red, _ = reduction_of_red_expr env red in
+    red env sigma body
 
 let warn_implicits_in_term =
   CWarnings.create ~name:"implicits-in-term" ~category:"implicits"
@@ -65,7 +45,7 @@ let interp_definition pl bl poly red_option c ctypopt =
   let open EConstr in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
-  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  let evd, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   (* Build the parameters *)
   let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
   (* Build the type *)
@@ -84,16 +64,18 @@ let interp_definition pl bl poly red_option c ctypopt =
       check_imps ~impsty ~impsbody;
       evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
   in
+  (* Do the reduction *)
+  let evd, c = red_constant_body red_option env_bl evd c in
   (* universe minimization *)
   let evd = Evd.minimize_universes evd in
   (* Substitute evars and universes, and add parameters.
      Note: in program mode some evars may remain. *)
-  let ctx = List.map (EConstr.to_rel_decl evd) ctx in
-  let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in
-  let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in
+  let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in
+  let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in
+  let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in
   (* Keep only useful universes. *)
   let uvars_fold uvars c =
-    Univ.LSet.union uvars (universes_of_constr env evd (of_constr c))
+    Univ.LSet.union uvars (universes_of_constr evd (of_constr c))
   in
   let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
   let evd = Evd.restrict_universe_context evd uvars in
@@ -101,10 +83,12 @@ let interp_definition pl bl poly red_option c ctypopt =
   let uctx = Evd.check_univ_decl ~poly evd decl in
   (* We're done! *)
   let ce = definition_entry ?types:tyopt ~univs:uctx c in
-  (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
+  (ce, evd, decl, imps)
 
 let check_definition (ce, evd, _, imps) =
-  check_evars_are_solved (Global.env ()) evd Evd.empty;
+  let env = Global.env () in
+  let empty_sigma = Evd.from_env env in
+  check_evars_are_solved env evd empty_sigma;
   ce
 
 let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
@@ -118,7 +102,7 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
       assert(Univ.ContextSet.is_empty ctx);
       let typ = match ce.const_entry_type with
         | Some t -> t
-        | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+        | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
       in
       Obligations.check_evars env evd;
       let obls, _, c, cty =
-- 
cgit v1.2.3