diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:08 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:08 +0000 |
| commit | 6d5eee245a85f410ec184353ab9f38ce3aa4e331 (patch) | |
| tree | 9260a0fb3662dbeb6837468e30f69f5f862e7893 /pretyping/nativenorm.ml | |
| 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/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index f65ccc5ba..a4f00bc45 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 |