Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 12 insertions, 7 deletions

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 465c062b..5d09570e 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vnorm.ml 11017 2008-05-29 13:00:24Z barras $ i*)
+(*i $Id: vnorm.ml 11424 2008-09-30 12:10:28Z jforest $ i*)
 
 open Names
 open Declarations
@@ -20,7 +20,7 @@ open Vm
 (* Calcul de la forme normal d'un terme    *)
 (*******************************************)
 
-let crazy_type = mkSet 
+let crazy_type =  mkSet 
 
 let decompose_prod env t =
   let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
@@ -178,7 +178,7 @@ 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 = decompose_prod env typ in
+      let _,_,codom = try decompose_prod env typ with _ -> 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
@@ -187,6 +187,7 @@ and nf_stk env c t stk  =
       let params,realargs = Util.array_chop nparams allargs in
       let pT = 
 	hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in
+      let pT = whd_betadeltaiota env pT in
       let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in
       (* Calcul du type des branches *)
       let btypes = build_branches_type env ind mib mip params dep p in
@@ -210,7 +211,7 @@ 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 = decompose_prod env pT in
+      let name,dom,codom = try decompose_prod env pT with _ -> 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)
@@ -232,7 +233,7 @@ and nf_args env vargs t =
   let args = 
     Array.init len 
       (fun i ->
-	let _,dom,codom = decompose_prod env !t in
+	let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in
 	let c = nf_val env (arg vargs i) dom in
 	t := subst1 c codom; c) in
   !t,args
@@ -243,7 +244,7 @@ and nf_bargs env b t =
   let args =
     Array.init len 
       (fun i -> 
-	let _,dom,codom = decompose_prod env !t in
+	let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
 	let c = nf_val env (bfield b i) dom in
 	t := subst1 c codom; c) in
   args
@@ -251,7 +252,11 @@ and nf_bargs env b t =
 and nf_fun env f typ =
   let k = nb_rel env in
   let vb = body_of_vfun k f in
-  let name,dom,codom = decompose_prod env typ in
+  let name,dom,codom = 
+    try decompose_prod env typ
+    with _ ->
+      raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
+  in
   let body = nf_val (push_rel (name,None,dom) env) vb codom in
   mkLambda(name,dom,body)