From 6d5eee245a85f410ec184353ab9f38ce3aa4e331 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 12 Mar 2013 23:59:08 +0000 Subject: 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 --- plugins/firstorder/ground.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/firstorder/ground.ml') 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 -- cgit v1.2.3