diff options
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 48 |
1 files changed, 16 insertions, 32 deletions
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 = |