From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 8 May 2013 17:47:10 +0200
Subject: Imported Upstream version 8.4pl2dfsg

---
 pretyping/vnorm.ml | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

(limited to 'pretyping/vnorm.ml')

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 00efa981..3966146d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -44,7 +44,7 @@ let invert_tag cst tag reloc_tbl =
 let find_rectype_a env c =
   let (t, l) =
     let t = whd_betadeltaiota env c in
-    try destApp t with _ -> (t,[||]) in
+    try destApp t with e when Errors.noncritical e -> (t,[||]) in
   match kind_of_term t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
@@ -176,7 +176,10 @@ and nf_stk env c t stk  =
       nf_stk env (mkApp(c,args)) t stk
   | Zfix (f,vargs) :: stk ->
       let fa, typ = nf_fix_app env f vargs in
-      let _,_,codom = try decompose_prod env typ with _ -> exit 120 in
+      let _,_,codom =
+        try decompose_prod env typ
+        with e when Errors.noncritical e -> exit 120
+      in
       nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
       let (mind,_ as ind),allargs = find_rectype_a env t in
@@ -206,7 +209,10 @@ and nf_predicate env ind mip params v pT =
   | Vfun f, Prod _ ->
       let k = nb_rel env in
       let vb = body_of_vfun k f in
-      let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in
+      let name,dom,codom =
+        try decompose_prod env pT
+        with e when Errors.noncritical e -> exit 121
+      in
       let dep,body =
 	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
       dep, mkLambda(name,dom,body)
@@ -228,7 +234,10 @@ and nf_args env vargs t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in
+	let _,dom,codom =
+          try decompose_prod env !t
+          with e when Errors.noncritical e -> exit 123
+        in
 	let c = nf_val env (arg vargs i) dom in
 	t := subst1 c codom; c) in
   !t,args
@@ -239,7 +248,10 @@ and nf_bargs env b t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
+	let _,dom,codom =
+          try decompose_prod env !t
+          with e when Errors.noncritical e -> exit 124
+        in
 	let c = nf_val env (bfield b i) dom in
 	t := subst1 c codom; c) in
   args
@@ -249,7 +261,7 @@ and nf_fun env f typ =
   let vb = body_of_vfun k f in
   let name,dom,codom =
     try decompose_prod env typ
-    with _ ->
+    with e when Errors.noncritical e ->
       raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
   in
   let body = nf_val (push_rel (name,None,dom) env) vb codom in
-- 
cgit v1.2.3