From b354b232c3356159f6866fab00816cd5412cd036 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 25 Jun 2014 13:08:17 +0200 Subject: In exact check, use e_type_of to ensure that universe constraints necessary to typecheck the term are not forgotten. (relieves tactic implementors from calling e_type_of themselves, e.g. in congruence). Fixes a bug found in Containers. --- tactics/tactics.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3c0016830..178087cff 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1227,8 +1227,11 @@ let exact_check c = Proofview.Goal.raw_enter begin fun gl -> (** We do not need to normalize the goal because we just check convertibility *) let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - let ct = Tacmach.New.pf_type_of gl c in - Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, ct = Typing.e_type_of env sigma c in + Proofview.V82.tclEVARS sigma <*> + Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) end let exact_no_check = refine_no_check -- cgit v1.2.3