diff options
| -rw-r--r-- | contrib/first-order/instances.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index eac842b86..04852da66 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -129,7 +129,10 @@ let mk_open_instance id gl m t= let t1=raux (n-1) t0 in RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1) | _-> anomaly "can't happen" in - let ntt=Pretyping.understand evmap env (raux m rawt) in + let ntt=try + Pretyping.understand evmap env (raux m rawt) + with _ -> + error "Untypable instance, maybe higher-order non-prenex quantification" in Sign.decompose_lam_n_assum m ntt (* tactics *) |