diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/nativenorm.ml | 2 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 10 |
2 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index f65ccc5ba9..a4f00bc457 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -170,7 +170,7 @@ let rec nf_val env v typ = let lvl = nb_rel env in let name,dom,codom = try decompose_prod env typ - with Invalid_argument _ -> + with DestKO -> Errors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b18719cc27..1ccc103755 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -176,7 +176,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 = try decompose_prod env typ with _ -> exit 120 in + let _,_,codom = try decompose_prod env typ with DestKO -> 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 +206,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 = try decompose_prod env pT with _ -> exit 121 in + let name,dom,codom = try decompose_prod env pT with DestKO -> 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 +228,7 @@ 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 DestKO -> exit 123 in let c = nf_val env (arg vargs i) dom in t := subst1 c codom; c) in !t,args @@ -239,7 +239,7 @@ 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 DestKO -> exit 124 in let c = nf_val env (bfield b i) dom in t := subst1 c codom; c) in args @@ -249,7 +249,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 Invalid_argument _ -> + with DestKO -> (* 27/2/13: Turned this into an anomaly *) Errors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") |