diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 5 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 4 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 32 | ||||
| -rw-r--r-- | vernac/comFixpoint.ml | 4 | ||||
| -rw-r--r-- | vernac/obligations.ml | 4 |
5 files changed, 16 insertions, 33 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 09e2b8df45..3cf5e9bfdf 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -9,6 +9,7 @@ (************************************************************************) (*i*) +module CVars = Vars open Names open EConstr open Nametab @@ -116,8 +117,8 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = let kind = IsDefinition Instance in let sigma = - let levels = Univ.LSet.union (Univops.universes_of_constr termtype) - (Univops.universes_of_constr term) in + let levels = Univ.LSet.union (CVars.universes_of_constr termtype) + (CVars.universes_of_constr term) in Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 9497f2fb03..e990f0cd15 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -162,7 +162,7 @@ let do_assumptions kind nl l = let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in - let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in + let uvars = Univ.LSet.union uvars (Vars.universes_of_constr t) in uvars, (coe,t,imps)) Univ.LSet.empty l in @@ -173,7 +173,7 @@ let do_assumptions kind nl l = let t = replace_vars subst t in let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 - (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u))) + (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs in subst'@subst, status' && status, next_uctx uctx) 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 diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 5f340dc144..138696e3a7 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -266,7 +266,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in + let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -299,7 +299,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Univops.universes_of_constr (List.hd fixdecls) in + let vars = Vars.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 5352cf5f8c..0ac97a74e4 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -487,8 +487,8 @@ let declare_definition prg = let typ = nf typ in let body = nf body in let uvars = Univ.LSet.union - (Univops.universes_of_constr typ) - (Univops.universes_of_constr body) in + (Vars.universes_of_constr typ) + (Vars.universes_of_constr body) in let uctx = UState.restrict prg.prg_ctx uvars in let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in |