aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 23:59:08 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 23:59:08 +0000
commit6d5eee245a85f410ec184353ab9f38ce3aa4e331 (patch)
tree9260a0fb3662dbeb6837468e30f69f5f862e7893 /plugins/firstorder
parent3b7ecfa6d4da684a635b2469c2d9a2e1e0ed0807 (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 'plugins/firstorder')
-rw-r--r--plugins/firstorder/ground.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 48e60d798..6c1709140 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -20,7 +20,8 @@ let update_flags ()=
try
let kn=destConst (Classops.get_coercion_value coe) in
predref:=Names.Cpred.add kn !predref
- with Invalid_argument "destConst"-> () in
+ with DestKO -> ()
+ in
List.iter f (Classops.coercions ());
red_flags:=
Closure.RedFlags.red_add_transparent