From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 17:21:44 +0100 Subject: Typing API using EConstr. --- plugins/firstorder/instances.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder') 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) -- cgit v1.2.3