From 82fb5aa169bff5d3aaa29c8eadce995379a5f7b5 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Mon, 13 Feb 2006 13:27:11 +0000
Subject: firstorder fails gracefullly when encountering untypable higher-order
 terms

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8040 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/first-order/instances.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index eac842b86a..04852da664 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   *)
-- 
cgit v1.2.3