diff options
| author |  vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-24 14:34:41 +0000 |
|---|---|---|
| committer | vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-24 14:34:41 +0000 |
| commit | 462c44e6139282eaea7a91e03287ad9a132df28b (patch) | |
| tree | e970d21b5665e834c0e50a784d22b7c57ed079e6 | |
| parent | 4823449f7f3800835bfd5ebc4de5bdf407fdc2c2 (diff) | |
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
| -rw-r--r-- | toplevel/command.ml | 8 |
1 files 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 *) |