From 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 14 Sep 2015 18:35:48 +0200 Subject: Univs: Add universe binding lists to definitions ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. --- tactics/elimschemes.ml | 4 ++-- tactics/leminv.ml | 2 +- tactics/rewrite.ml | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) (limited to 'tactics') diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 749e0d2b5b..e1c9c2de59 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -51,7 +51,7 @@ let optimize_non_type_induction_scheme kind dep sort ind = let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx 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 + let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in (c, Evd.evar_universe_context sigma), Declareops.no_seff let build_induction_scheme_in_type dep sort ind = @@ -63,7 +63,7 @@ let build_induction_scheme_in_type dep sort ind = let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx 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 + let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in c, Evd.evar_universe_context sigma let rect_scheme_kind_from_type = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 9a64b03fd1..efd6ded44c 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.from_env ~ctx:(evar_universe_context sigma) invEnv) [invEnv,invGoal] in + let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [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 719cc7c98d..aa057a3e86 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1824,8 +1824,8 @@ let declare_projection n instance_id r = let build_morphism_signature m = let env = Global.env () in - let m,ctx = Constrintern.interp_constr env Evd.empty m in - let sigma = Evd.from_env ~ctx env in + let m,ctx = Constrintern.interp_constr env (Evd.from_env env) m in + let sigma = Evd.from_ctx ctx in let t = Typing.unsafe_type_of env sigma m in let cstrs = let rec aux t = -- cgit v1.2.3 From e91327a01f725f6c709adba9ddf3b41212b488ca Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 16 Sep 2015 08:42:14 +0200 Subject: Continuing investigation on how to preserve the locality of the action of "apply ... in ... as ..." in the context. Fixing a regression done by 7e00e8d60 and f2130a88e1: when an evar is created, the statement of the refined hypothesis virtually depends on the whole context and has to be left at the top. --- tactics/tactics.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0235126cc0..d0724804b4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2283,7 +2283,9 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id lemma tac in Proofview.Goal.enter begin fun gl -> - let destopt = get_previous_hyp_position id gl in + let destopt = + if with_evars then MoveLast (* evars would depend on the whole context *) + else get_previous_hyp_position id gl in let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = let last,first = List.sep_last lemmas in -- cgit v1.2.3 From 16db94e6c142217a81cc78be8788137617c24de7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 16 Sep 2015 21:44:47 +0200 Subject: In pat/constr introduction patterns, fixing in a better way clearing problems of temporary hypotheses than 76f27140e6e34 did. --- tactics/tactics.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d0724804b4..ad7ff14e6b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2209,6 +2209,11 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with | IntroApplyOn (f,(loc,pat)) -> let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) destopt pat in + let doclear = + if naming = NamingMustBe (loc,id) then + Proofview.tclUNIT () (* apply_in_once do a replacement *) + else + Proofview.V82.tactic (clear [id]) in Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -2217,7 +2222,9 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with (Tacticals.New.tclTHENFIRST (* Skip the side conditions of the apply *) (apply_in_once false true true true naming id - (None,(sigma,(c,NoBindings))) tac_ipat) (tac ((dloc,id)::thin) None [])) + (None,(sigma,(c,NoBindings))) + (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id))) + (tac thin None [])) sigma end -- cgit v1.2.3