aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.ml')
-rw-r--r--stm/stm.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 6012e3d2d..d60412c0c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1792,7 +1792,7 @@ end = struct (* {{{ *)
str"uc=" ++ Evd.pr_evar_universe_context uc)));
(if abstract then Tactics.tclABSTRACT None else (fun x -> x))
(V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
- Tactics.exact_no_check pt)
+ Tactics.exact_no_check (EConstr.of_constr pt))
with TacTask.NoProgress ->
if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
})