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.

1 files 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