From 462c44e6139282eaea7a91e03287ad9a132df28b Mon Sep 17 00:00:00 2001 From: vsiles Date: Tue, 24 Jun 2008 14:34:41 +0000 Subject: Catch a Not_found exception in the Combined Scheme mechanism to hide an ugly Anomaly with a better error message git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11168 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/command.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/toplevel/command.ml b/toplevel/command.ml index 518ae25cf..df133e769 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -999,11 +999,14 @@ let build_combined_scheme name schemes = | App (ind, args) -> ctx, destInd ind, Array.length args | _ -> ctx, destInd last, 0 in - let defs = + let defs = List.map (fun x -> let refe = Ident x in let qualid = qualid_of_reference refe in - let cst = Nametab.locate_constant (snd qualid) in + let cst = try + Nametab.locate_constant (snd qualid) + with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared") + in let ty = Typeops.type_of_constant env cst in qualid, cst, ty) schemes @@ -1035,7 +1038,6 @@ let build_combined_scheme name schemes = const_entry_boxed = Flags.boxed_definitions() } in let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in if_verbose ppnl (recursive_message Fixpoint None [snd name]) - (* 4| Goal declaration *) (* 4.1| Support for mutually proved theorems *) -- cgit v1.2.3