From 6288d74ca83dd5f93758da01f7028b8d9954c391 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 26 Jun 2007 14:19:41 +0000 Subject: 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 --- kernel/environ.ml | 11 ++++++----- 1 file 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} -- cgit v1.2.3