aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/instances.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a3513692c..44bdb585a 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -155,7 +155,7 @@ let left_instance_tac (inst,id) continue seq=
it_mkLambda_or_LetIn
(mkApp(idc,[|ot|])) rc in
let evmap, _ =
- try Typing.type_of (pf_env gl) evmap gt
+ try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt)
with e when CErrors.noncritical e ->
error "Untypable instance, maybe higher-order non-prenex quantification" in
tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)