diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elimschemes.ml | 6 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 14 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 |
6 files changed, 23 insertions, 18 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 9b600409a..f497b99d6 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -50,7 +50,8 @@ let optimize_non_type_induction_scheme kind dep sort ind = let ctx = if mib.mind_polymorphic then mib.mind_universes else Univ.UContext.empty in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in - let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ctxset env) (ind,u) dep sort in + let ectx = Evd.evar_universe_context_of ctxset in + let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in (c, Evd.evar_universe_context sigma), Declareops.no_seff let build_induction_scheme_in_type dep sort ind = @@ -61,7 +62,8 @@ let build_induction_scheme_in_type dep sort ind = in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in - let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ctxset env) (ind,u) dep sort in + let ectx = Evd.evar_universe_context_of ctxset in + let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in c, Evd.evar_universe_context sigma let rect_scheme_kind_from_type = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index da1475d7b..9cb22e5ea 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -304,10 +304,11 @@ open Coqlib let project_hint pri l2r r = let gr = Smartlocate.global_with_alias r in let env = Global.env() in - let c,ctx = Universes.fresh_global_instance env gr in - let t = Retyping.get_type_of env (Evd.from_env ~ctx env) c in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + let t = Retyping.get_type_of env sigma c in let t = - Tacred.reduce_to_quantified_ref env Evd.empty (Lazy.force coq_iff_ref) t in + Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in let sign,ccl = decompose_prod_assum t in let (a,b) = match snd (decompose_app ccl) with | [a;b] -> (a,b) @@ -320,6 +321,7 @@ let project_hint pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in + let ctx = Evd.universe_context_set sigma in let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in (pri,false,true,Auto.PathAny, Auto.IsGlobRef (Globnames.ConstRef c)) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index a10ad1e2b..d4f521054 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start Evd.empty [invEnv,(invGoal,universe_context_set sigma)] in + let pf = Proof.start (Evd.from_env ~ctx:(evar_universe_context sigma) invEnv) [invEnv,invGoal] in let pf = fst (Proof.run_tactic env ( tclTHEN intro (onLastHypId inv_op)) pf) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index b4b8d468c..477e5bcda 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -589,8 +589,9 @@ let solve_remaining_by by env prf = let evd' = List.fold_right (fun mv evd -> let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in - let c,_,_ = Pfedit.build_by_tactic env.env (ty,Univ.ContextSet.empty) (Tacticals.New.tclCOMPLETE tac) in - meta_assign mv (fst c (*FIXME*), (Conv,TypeNotProcessed)) evd) + let c,_,ctx' = Pfedit.build_by_tactic env.env (Evd.evar_universe_context evd) ty (Tacticals.New.tclCOMPLETE tac) in + let evd = Evd.set_universe_context evd ctx' in + meta_assign mv (c, (Conv,TypeNotProcessed)) evd) indep env.evd in { env with evd = evd' }, prf @@ -1236,7 +1237,8 @@ module Strategies = fail cs let inj_open hint = - (Evd.from_env ~ctx:hint.Autorewrite.rew_ctx (Global.env()), + let ctx = Evd.evar_universe_context_of hint.Autorewrite.rew_ctx in + (Evd.from_env ~ctx (Global.env()), (hint.Autorewrite.rew_lemma, NoBindings)) let old_hints (db : string) : strategy = @@ -1727,7 +1729,7 @@ let declare_projection n instance_id r = let build_morphism_signature m = let env = Global.env () in let m,ctx = Constrintern.interp_constr Evd.empty env m in - let sigma = Evd.from_env ~ctx:(Evd.evar_universe_context_set ctx) env in + let sigma = Evd.from_env ~ctx env in let t = Typing.type_of env sigma m in let cstrs = let rec aux t = @@ -1788,7 +1790,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 ctx = Univ.ContextSet.empty (*FIXME *) in + let ctx = Evd.empty_evar_universe_context (*FIXME *) in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id (Entries.ParameterEntry @@ -1815,7 +1817,7 @@ let add_morphism_infer glob m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind (instance, ctx) hook; + Lemmas.start_proof instance_id kind ctx instance hook; ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism glob binders m s n = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1d76f4afd..aafe6f2f7 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2060,8 +2060,7 @@ let _ = if has_type arg (glbwit wit_tactic) then let tac = out_gen (glbwit wit_tactic) arg in let tac = interp_tactic ist tac in - let ctx = Evd.universe_context_set sigma in - let prf = Proof.start sigma [env, (ty, ctx)] in + let prf = Proof.start sigma [env, ty] in let (prf, _) = try Proof.run_tactic env tac prf with Proof_errors.TacticFailure e as src -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 984e165d1..c7fc4197e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3823,8 +3823,9 @@ let abstract_subproof id gk tac = evd, ctx, nf concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in - let (const, safe, (subst, ctx)) = - try Pfedit.build_constant_by_tactic ~goal_kind:gk id secsign (concl, ctx) solve_tac + let ectx = Evd.evar_universe_context evd in + let (const, safe, ectx) = + try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac with Proof_errors.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it @@ -3840,8 +3841,7 @@ let abstract_subproof id gk tac = let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in - let evd = Evd.merge_context_set Evd.univ_rigid evd (Univ.ContextSet.of_context ctx) in - let evd = Evd.merge_universe_subst evd subst in + let evd = Evd.set_universe_context evd ectx in let open Declareops in let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in let effs = cons_side_effects eff |