diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 19 |
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) |