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/mltop.ml4 | |
| 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/mltop.ml4')
| -rw-r--r-- | toplevel/mltop.ml4 | 8 |
1 files changed, 6 insertions, 2 deletions
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 >] |