diff options
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | stm/lemmas.ml | 3 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 5 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 7 | ||||
| -rw-r--r-- | tactics/hints.ml | 3 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 24 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 10 | ||||
| -rw-r--r-- | toplevel/classes.ml | 15 | ||||
| -rw-r--r-- | toplevel/command.ml | 13 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 19 | ||||
| -rw-r--r-- | toplevel/record.ml | 79 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 5 |
13 files changed, 112 insertions, 77 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 18e83056b..2ef289650 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -370,7 +370,7 @@ let add_instance check inst = List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path (is_local inst) pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) - (Global.env ()) Evd.empty inst.is_impl inst.is_pri) + (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri) let rebuild_instance (action, inst) = let () = match action with diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 7679b1a66..2bd1c5451 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -503,4 +503,5 @@ let save_proof ?proof = function let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> - (Evd.empty, Global.env()) + let env = Global.env () in + (Evd.from_env env, env) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 2b3fadf7f..3a9d40de0 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -292,10 +292,13 @@ let find_applied_relation metas loc env sigma c left2right = (* To add rewriting rules to a base *) let add_rew_rules base lrul = let counter = ref 0 in + let env = Global.env () in + let sigma = Evd.from_env env in let lrul = List.fold_left (fun dn (loc,(c,ctx),b,t) -> - let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in + let info = find_applied_relation false loc env sigma c b in let pat = if b then info.hyp_left else info.hyp_right in let rul = { rew_lemma = c; rew_type = info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; diff --git a/tactics/equality.ml b/tactics/equality.ml index d012427a0..53678aa84 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -335,7 +335,9 @@ let find_elim hdcncl lft2rgt dep cls ot gl = | Ind (ind,u) -> let c, eff = find_scheme scheme_name ind in (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *) - let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in + let sigma, elim = + Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) + in sigma, elim, eff | _ -> assert false diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index af0870bc9..ead26e964 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -262,7 +262,8 @@ TACTIC EXTEND rewrite_star (* Hint Rewrite *) let add_rewrite_hint bases ort t lcsr = - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in let poly = Flags.is_universe_polymorphism () in let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in @@ -490,7 +491,9 @@ let inTransitivity : bool * constr -> obj = (* Main entry points *) let add_transitivity_lemma left lem = - let lem',ctx (*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty lem in + let env = Global.env () in + let sigma = Evd.from_env env in + let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in add_anonymous_leaf (inTransitivity (left,lem')) (* Vernacular syntax *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 0df1a35c6..48b450532 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1135,7 +1135,8 @@ let add_hints local dbnames0 h = if String.List.mem "nocore" dbnames0 then error "The hint database \"nocore\" is meant to stay empty."; let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in match h with | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index c64a1226a..937ad2b9d 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1797,11 +1797,13 @@ let proper_projection r ty = it_mkLambda_or_LetIn app ctx let declare_projection n instance_id r = - let c,uctx = Universes.fresh_global_instance (Global.env()) r in let poly = Global.is_polymorphic r in - let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in + let env = Global.env () in + let sigma = Evd.from_env env in + let evd,c = Evd.fresh_global env sigma r in + let ty = Retyping.get_type_of env sigma c in let term = proper_projection c ty in - let typ = Typing.unsafe_type_of (Global.env ()) Evd.empty term in + let typ = Typing.unsafe_type_of env sigma term in let ctx, typ = decompose_prod_assum typ in let typ = let n = @@ -1824,15 +1826,16 @@ let declare_projection n instance_id r = in let typ = it_mkProd_or_LetIn typ ctx in let cst = - Declare.definition_entry ~types:typ ~poly ~univs:(Univ.ContextSet.to_context uctx) - term + Declare.definition_entry ~types:typ ~poly + ~univs:(Evd.universe_context sigma) term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) let build_morphism_signature m = let env = Global.env () in - let m,ctx = Constrintern.interp_constr env (Evd.from_env env) m in + let sigma = Evd.from_env env in + let m,ctx = Constrintern.interp_constr env sigma m in let sigma = Evd.from_ctx ctx in let t = Typing.unsafe_type_of env sigma m in let cstrs = @@ -1844,7 +1847,7 @@ let build_morphism_signature m = in aux t in let evars, t', sig_, cstrs = - PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t cstrs None in + PropGlobal.build_signature (sigma, Evar.Set.empty) env t cstrs None in let evd = ref evars in let _ = List.iter (fun (ty, rel) -> @@ -1861,9 +1864,10 @@ let build_morphism_signature m = let default_morphism sign m = let env = Global.env () in - let t = Typing.unsafe_type_of env Evd.empty m in + let sigma = Evd.from_env env in + let t = Typing.unsafe_type_of env sigma m in let evars, _, sign, cstrs = - PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign) + PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in let evars, mor = resolve_one_typeclass env (goalevars evars) morph in @@ -1894,7 +1898,7 @@ let add_morphism_infer glob m n = let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = build_morphism_signature m in - let evd = Evd.empty (*FIXME *) in + let evd = Evd.from_env (Global.env ()) in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 7d1cc3341..bc82e9ef4 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -593,10 +593,12 @@ module New = struct (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - Proofview.Goal.nf_enter begin fun gl -> - let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in - (** FIXME: evar leak. *) + Proofview.Goal.nf_enter + begin fun gl -> let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Proofview.Goal.nf_enter begin fun gl -> + let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in (* applying elimination_scheme just a little modified *) let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in let indmv = @@ -647,7 +649,7 @@ module New = struct Proofview.tclTHEN (Clenvtac.clenv_refine false clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end + end) end let elimination_then tac c = Proofview.Goal.nf_enter begin fun gl -> diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 7fe79d948..805a29e39 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -347,7 +347,7 @@ let named_of_rel_context l = let context poly l = let env = Global.env() in - let evars = ref Evd.empty in + let evars = ref (Evd.from_env env) in let _, ((env', fullctx), impls) = interp_context_evars env evars l in let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in let fullctx = Context.map_rel_context subst fullctx in @@ -358,11 +358,13 @@ let context poly l = with e when Errors.noncritical e -> error "Anonymous variables not allowed in contexts." in - let uctx = Evd.universe_context_set !evars in + let uctx = ref (Evd.universe_context_set !evars) in let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let uctx = Univ.ContextSet.to_context uctx in - let decl = (ParameterEntry (None,poly,(t,uctx),None), IsAssumption Logical) in + let ctx = Univ.ContextSet.to_context !uctx in + (* Declare the universe context once *) + let () = uctx := Univ.ContextSet.empty in + let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr t with | Some (rels, ((tc,_), args) as _cl) -> @@ -379,8 +381,9 @@ let context poly l = let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in let nstatus = - pi3 (Command.declare_assumption false decl (t, uctx) [] impl + pi3 (Command.declare_assumption false decl (t, !uctx) [] impl Vernacexpr.NoInline (Loc.ghost, id)) in - status && nstatus + let () = uctx := Univ.ContextSet.empty in + status && nstatus in List.fold_left fn true (List.rev ctx) diff --git a/toplevel/command.ml b/toplevel/command.ml index d397eed61..b65ff73fe 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -241,11 +241,14 @@ let interp_assumption evdref env impls bl c = let ctx = Evd.universe_context_set evd in ((nf ty, ctx), impls) -let declare_assumptions idl is_coe k c imps impl_is_on nl = - let refs, status = - List.fold_left (fun (refs,status) id -> - let ref',u',status' = declare_assumption is_coe k c imps impl_is_on nl id in - (ref',u')::refs, status' && status) ([],true) idl in +let declare_assumptions idl is_coe k (c,ctx) imps impl_is_on nl = + let refs, status, _ = + List.fold_left (fun (refs,status,ctx) id -> + let ref',u',status' = + declare_assumption is_coe k (c,ctx) imps impl_is_on nl id in + (ref',u')::refs, status' && status, Univ.ContextSet.empty) + ([],true,ctx) idl + in List.rev refs, status let do_assumptions (_, poly, _ as kind) nl l = diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 3c0977784..e8682c1b5 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -623,7 +623,7 @@ let declare_obligation prg obl body ty uctx = let body = prg.prg_reduce body in let ty = Option.map prg.prg_reduce ty in match obl.obl_status with - | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) } + | Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } | Evar_kinds.Define opaque -> let opaque = if get_proofs_transparency () then false else opaque in let poly = pi2 prg.prg_kind in @@ -647,7 +647,7 @@ let declare_obligation prg obl body ty uctx = in if not opaque then add_hint false prg constant; definition_message obl.obl_name; - { obl with obl_body = + true, { obl with obl_body = if poly then Some (DefinedObl constant) else @@ -815,9 +815,9 @@ let obligation_hook prg obl num auto ctx' _ gr = let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in let ctx' = if not (pi2 prg.prg_kind) (* Not polymorphic *) then - (* This context is already declared globally, we cannot - instantiate the rigid variables anymore *) - Evd.abstract_undefined_variables ctx' + (* The universe context was declared globally, we continue + from the new global environment. *) + Evd.evar_universe_context (Evd.from_env (Global.env ())) else ctx' in let prg = { prg with prg_ctx = ctx' } in @@ -889,8 +889,13 @@ and solve_obligation_by_tac prg obls i tac = (pi2 !prg.prg_kind) !prg.prg_ctx in let uctx = Evd.evar_context_universe_context ctx in - prg := {!prg with prg_ctx = ctx}; - obls.(i) <- declare_obligation !prg obl t ty uctx; + let () = prg := {!prg with prg_ctx = ctx} in + let def, obl' = declare_obligation !prg obl t ty uctx in + obls.(i) <- obl'; + if def && not (pi2 !prg.prg_kind) then ( + (* Declare the term constraints with the first obligation only *) + let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in + prg := {!prg with prg_ctx = ctx'}); true else false with e when Errors.noncritical e -> diff --git a/toplevel/record.ml b/toplevel/record.ml index e214f9ca7..ee80101f3 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -233,7 +233,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let (mib,mip) = Global.lookup_inductive indsp in let u = Declareops.inductive_instance mib in let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in + let poly = mib.mind_polymorphic in + let ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in @@ -293,7 +294,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; - const_entry_universes = ctx; + const_entry_universes = + if poly then ctx else Univ.UContext.empty; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in @@ -397,44 +399,49 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity let impl, projs = match fields with | [(Name proj_name, _, field)] when def -> - let class_body = it_mkLambda_or_LetIn field params in - let _class_type = it_mkProd_or_LetIn arity params in - let class_entry = - Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in - let cst = Declare.declare_constant (snd id) - (DefinitionEntry class_entry, IsDefinition Definition) - in - let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in - let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in - let proj_type = - it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in - let proj_body = - it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in - let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in - let proj_cst = Declare.declare_constant proj_name - (DefinitionEntry proj_entry, IsDefinition Definition) - in - let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref [paramimpls]; - Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; - Classes.set_typeclass_transparency (EvalConstRef cst) false false; - let sub = match List.hd coers with - | Some b -> Some ((if b then Backward else Forward), List.hd priorities) - | None -> None - in - cref, [Name proj_name, sub, Some proj_cst] + let class_body = it_mkLambda_or_LetIn field params in + let _class_type = it_mkProd_or_LetIn arity params in + let class_entry = + Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in + let inst_type = appvectc (mkConstU cstu) + (Termops.rel_vect 0 (List.length params)) in + let proj_type = + it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in + let proj_body = + it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in + let proj_entry = + Declare.definition_entry ~types:proj_type ~poly + ~univs:(if poly then ctx else Univ.UContext.empty) proj_body + in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + let cref = ConstRef cst in + Impargs.declare_manual_implicits false cref [paramimpls]; + Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; + Classes.set_typeclass_transparency (EvalConstRef cst) false false; + let sub = match List.hd coers with + | Some b -> Some ((if b then Backward else Forward), List.hd priorities) + | None -> None + in + cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign - in - let coers = List.map2 (fun coe pri -> - Option.map (fun b -> - if b then Backward, pri else Forward, pri) coe) + in + let coers = List.map2 (fun coe pri -> + Option.map (fun b -> + if b then Backward, pri else Forward, pri) coe) coers priorities - in - IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y)) - (List.rev fields) coers (Recordops.lookup_projections ind)) + in + let l = List.map3 (fun (id, _, _) b y -> (id, b, y)) + (List.rev fields) coers (Recordops.lookup_projections ind) + in IndRef ind, l in let ctx_context = List.map (fun (na, b, t) -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8ae6ac2bc..2946766cb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1185,8 +1185,9 @@ let default_env () = { let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let env = Global.env() in - let t,ctx = Constrintern.interp_type env Evd.empty c in - let t = Detyping.detype false [] env Evd.empty t in + let sigma = Evd.from_env env in + let t,ctx = Constrintern.interp_type env sigma c in + let t = Detyping.detype false [] env (Evd.from_env ~ctx env) t in let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |