diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-17 04:57:32 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-17 04:57:32 +0000 |
| commit | 1a750105e7d9630acf44dd0833cdc34578a0aea5 (patch) | |
| tree | 5165a4abf83dec76bca5fc37fdc1403e23c0bb58 /toplevel | |
| parent | 6e616fea2b9e153b04232537b7ee2539409521ac (diff) | |
Meilleure gestion de la reduction dans Field
Field term (nouveau)
Injections dans l'interpreteur de tactiques
Exportation de quelques entrees de grammaires
Exportation de quelques fonctionnalites des definitions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.mli | 8 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 8 |
2 files changed, 14 insertions, 2 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 04ae5a454..baa983788 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -21,6 +21,14 @@ open Nametab functions of [Declare]; they return an absolute reference to the defined object *) +val constant_entry_of_com : + Coqast.t * Coqast.t option * bool -> Safe_typing.constant_entry + +val declare_global_definition : + Names.identifier -> + Safe_typing.constant_entry -> + Declare.strength -> bool -> Nametab.global_reference + val definition_body : identifier -> bool * strength -> Coqast.t -> Coqast.t option -> global_reference diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index d9325a2e7..0b86c7656 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -97,12 +97,16 @@ let dir_ml_load s = match !load with | WithTop t -> if is_in_path !coq_mlpath_copy s then - try t.load_obj s + try + t.load_obj s with - | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u + | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> + raise u | _ -> errorlabstrm "Mltop.load_object" [< str"Cannot link ml-object "; str s; str" to Coq code." >] + + else errorlabstrm "Mltop.load_object" [< str"File not found on loadpath : "; str s >] |