diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-20 22:30:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-12 10:39:33 +0200 |
| commit | b006f10e7d591417844ffa1f04eeb926d6092d7b (patch) | |
| tree | 9253b32cb1adabafce28f123ef9eb11d4fa122f4 /plugins/firstorder | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/instances.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 6fd934654..2987ce60a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -127,7 +127,7 @@ let mk_open_instance id idc gl m t= GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,None),t1) | _-> anomaly (Pp.str "can't happen") in let ntt=try - fst (Pretyping.understand evmap env (raux m rawt))(*FIXME*) + fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*) with e when Errors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in decompose_lam_n_assum m ntt |