diff options
| author | letouzey | 2013-03-12 23:59:08 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-12 23:59:08 +0000 |
| commit | 6d5eee245a85f410ec184353ab9f38ce3aa4e331 (patch) | |
| tree | 9260a0fb3662dbeb6837468e30f69f5f862e7893 /pretyping | |
| parent | 3b7ecfa6d4da684a635b2469c2d9a2e1e0ed0807 (diff) | |
Term.dest* functions now raise specific DestKO exn instead of Invalid_argument
**Warning** the ml code of plugins may have to be adapted after this.
Concerning coq itself, I've done the adaptations, let's hope I've
forgotten none. In practice, the number of changes are relatively low,
and the code is quite cleaner this way.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16271 85f007b7-540e-0410-9357-904b9bb8a0f7
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.") |