Merge PR #8059: Simplify code for [Definition := Eval ...]

5 files changed, 21 insertions, 40 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 20185363e6..022c383f60 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -132,15 +132,15 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   (mkApp(mkConstructU((ind,i),u), params), ctyp)
  
 
-let construct_of_constr const env tag typ =
+let construct_of_constr const env sigma tag typ =
   let t, l = app_type env typ in
-  match kind t with
+  match EConstr.kind_upto sigma t with
   | Ind (ind,u) -> 
       construct_of_constr_notnative const env tag ind u l
   | _ -> assert false
 
-let construct_of_constr_const env tag typ = 
-  fst (construct_of_constr true env tag typ)
+let construct_of_constr_const env sigma tag typ =
+  fst (construct_of_constr true env sigma tag typ)
 
 let construct_of_constr_block = construct_of_constr false
 
@@ -207,9 +207,9 @@ let rec nf_val env sigma v typ =
       let env = push_rel (LocalAssum (name,dom)) env in
       let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
       mkLambda(name,dom,body)
-  | Vconst n -> construct_of_constr_const env n typ
+  | Vconst n -> construct_of_constr_const env sigma n typ
   | Vblock b ->
-      let capp,ctyp = construct_of_constr_block env (block_tag b) typ in
+      let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in
       let args = nf_bargs env sigma b ctyp in
       mkApp(capp,args)
 
diff --git a/test-suite/bugs/closed/bug_3690.v b/test-suite/bugs/closed/bug_3690.v
index fa30132ab5..9273a20e19 100644
--- a/test-suite/bugs/closed/bug_3690.v
+++ b/test-suite/bugs/closed/bug_3690.v
@@ -41,8 +41,5 @@ Type@{Top.34} -> Type@{Top.37}
                                   Top.36 < Top.34
                                   Top.37 < Top.36
                                    *) *)
-Fail Check @qux@{Set Set}.
-Check @qux@{Type Type Type Type}.
-(* [qux] should only need two universes *)
-Check @qux@{i j k l}.  (* Error: The command has not failed!, but I think this is suboptimal *)
-Fail Check @qux@{i j}.
+Check @qux@{Type Type}.
+(* used to have 4 universes *)
diff --git a/test-suite/bugs/closed/bug_3956.v b/test-suite/bugs/closed/bug_3956.v
index 115284ec02..456fa11bd0 100644
--- a/test-suite/bugs/closed/bug_3956.v
+++ b/test-suite/bugs/closed/bug_3956.v
@@ -129,13 +129,13 @@ Module Comodality_Theory (F : Comodality).
       := IdmapM FPM.
     Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM.
     Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM.
-      Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x.
+      Definition m : forall x, cip_FPM.fhM.m x = cip_FPM.fkM.m x.
       Proof.
         intros x.
-        refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _).
+        refine (concat (cmpinvM.m_beta (cmpM.m x)) _).
         apply path_prod@{i i i}; simpl.
-        - exact (cmpM.FfstM.mM.m_beta@{i j} x).
-        - exact (cmpM.FsndM.mM.m_beta@{i j} x).
+        - exact (cmpM.FfstM.mM.m_beta x).
+        - exact (cmpM.FsndM.mM.m_beta x).
       Defined.
     End cip_FPHM.
   End isequiv_F_prod_cmp_M.
diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v
index 34eb8b8676..93aeb83e28 100644
--- a/test-suite/bugs/closed/bug_7631.v
+++ b/test-suite/bugs/closed/bug_7631.v
@@ -7,6 +7,7 @@ Section Foo.
 Let bar := foo.
 
 Eval native_compute in bar.
+Eval vm_compute in bar.
 
 End Foo.
 
@@ -17,5 +18,6 @@ Module RelContext.
 Definition foo := true.
 
 Definition bar (x := foo) := Eval native_compute in x.
+Definition barvm (x := foo) := Eval vm_compute in x.
 
 End RelContext.
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5d17662d1a..cc03473bc6 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"
@@ -84,6 +64,8 @@ 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.
@@ -101,7 +83,7 @@ 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) =
   let env = Global.env () in