kill an ugly warning about a non-exhaustive pattern

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9911 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 5 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9143db37d..e69f63d24 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -402,14 +402,15 @@ let unregister env field =
 	(*there is only one matching kind due to the fact that Environ.env
           is abstract, and that the only function which add elements to the
           retroknowledge is Environ.register which enforces this shape *)
-        let Ind i31t = retroknowledge find env field in 
-	let i31c = Construct (i31t, 1) in
-	  {env with retroknowledge = 
-	      remove (retroknowledge clear_info env i31c) field}
+	(match retroknowledge find env field with 
+	   | Ind i31t -> let i31c = Construct (i31t, 1) in
+	     {env with retroknowledge = 
+		 remove (retroknowledge clear_info env i31c) field}
+	   | _ -> assert false)
     |_ -> {env with retroknowledge =
 	   try 
 	     remove (retroknowledge clear_info env 
-                                         (retroknowledge find env field)) field
+                       (retroknowledge find env field)) field
 	   with Not_found ->
 	     retroknowledge remove env field}