Modification pour faire compiler pretyping.ml qui maintenant compile

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@156 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 8 insertions, 6 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 60139def2e..0e8dc75d2a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -150,4 +150,3 @@ let mind_check_lc params mie =
       raise (InductiveError BadEntry)
   in
   List.iter check_lc mie.mind_entry_inds
-
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index bc4021fbf9..5f011c06d8 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1265,16 +1265,16 @@ let poly_args env sigma t =
 
 (* Expanding existential variables (trad.ml, progmach.ml) *)
 (* 1- whd_ise fails if an existential is undefined *)
+
+exception Uninstantiated_evar of int
+
 let rec whd_ise env sigma = function
   | DOPN(Evar sp,_) as k ->
       if Evd.in_dom sigma sp then
         if Evd.is_defined sigma sp then
           whd_ise env sigma (existential_value sigma k)
-        else
-          errorlabstrm "whd_ise"
-            [< 'sTR"There is an unknown subterm I cannot solve" >]
-      else 
-	k
+        else raise (Uninstantiated_evar sp)
+      else k
   | DOP2(Cast,c,_) -> whd_ise env sigma c
   | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
   | c -> c
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 67ad99f55a..3e2fc9ffd1 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -180,6 +180,9 @@ val whd_meta : (int * constr) list -> constr -> constr
 val plain_instance : (int * constr) list -> constr -> constr
 val instance : (int * constr) list -> 'a reduction_function
 
+(* whd_ise raise Uninstantiated_evar if an evar remains uninstantiated *)
+(* the '*_ise1*' leave uninstantiated evar as it *)
+exception Uninstantiated_evar of int
 val whd_ise : 'a reduction_function
 val whd_ise1 : 'a reduction_function
 val nf_ise1 : 'a reduction_function