From 837cde99a5b3995bddd5ecfbaa48ee19dcd615a1 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Thu, 13 Feb 2003 17:24:40 +0000
Subject: Chargement dynamique de .cma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3676 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES              |  5 ++++
 tactics/tacinterp.ml |  6 -----
 toplevel/mltop.ml4   | 64 ++++++++++++++++++++++------------------------------
 3 files changed, 32 insertions(+), 43 deletions(-)

diff --git a/CHANGES b/CHANGES
index 481509b7f6..73df7cb096 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,11 @@
 Changes from V7.4
 =================
 
+Vernacular commands
+
+- "Declare ML Module" now allows us to import .cma files. This avoids to use a
+   bunch of "Declare ML Module" statements when using several ML files.
+
 Bugs
 
 - Rename bug fixed (#244)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3f9ad2fd79..eb29d67edb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -772,12 +772,6 @@ let apply_one_mhyp_context ist env gl lmatch mhyp lhyps noccopt =
   and get_info_pattern = function
     | Hyp((_,idpat),pat) -> (Some idpat,pat)
     | NoHypId pat -> (None,pat) in
-
-(*=======
-    | Hyp((_,idpat),_) -> [idpat,VConstr (mkVar id)]
-    | NoHypId _ -> [] in
->>>>>>> 1.28*)
-
   let rec apply_one_mhyp_context_rec ist env mhyp lhyps_acc nocc = function
     | (id,hyp)::tl ->
       (match (get_pattern mhyp) with
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 20d87306a1..553da3493f 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -87,47 +87,29 @@ let ocaml_toploop () =
   match !load with
     | WithTop t -> Printexc.catch t.ml_loop ()
     | _ -> ()
-(*
-        errorlabstrm "Mltop.ocaml_toploop"
-          [< str"Cannot access the ML toplevel" >]
-*)
 
-(* Dynamic loading of .cmo *)
+(* Dynamic loading of .cmo/.cma *)
 let dir_ml_load s = 
   match !load with
-    | WithTop t -> 
-	if is_in_path !coq_mlpath_copy s then
-          try 
-            t.load_obj s
-          with
-            | (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 >]
+    | WithTop t ->
+      (try t.load_obj s
+       with
+       | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u
+       | _ -> errorlabstrm "Mltop.load_object" [< str"Cannot link ml-object ";
+                str s; str" to Coq code." >])
+(* TO DO: .cma loading without toplevel *)
     | WithoutTop ->
       ifdef Byte then
-	(if is_in_path !coq_mlpath_copy s then
-          let _,gname = where_in_path !coq_mlpath_copy s in
-          try
-            Dynlink.loadfile gname;
-	    Dynlink.add_interfaces 
-	      [(String.capitalize (Filename.chop_suffix
-				     (Filename.basename gname) ".cmo"))] 
-	      [Filename.dirname gname]
-	  with
-	    | Dynlink.Error(a) ->
-		errorlabstrm "Mltop.load_object"
-                  [< str (Dynlink.error_message a) >]
-	else errorlabstrm "Mltop.load_object"
-          [< str"File not found on loadpath : "; str s >])
-      else
-	()
+        let _,gname = where_in_path !coq_mlpath_copy s in
+        try
+          Dynlink.loadfile gname;
+	  Dynlink.add_interfaces 
+	    [(String.capitalize (Filename.chop_suffix
+				(Filename.basename gname) ".cmo"))] 
+	    [Filename.dirname gname]
+	with | Dynlink.Error a ->
+          errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >]
+      else ()
     | Native ->
 	errorlabstrm "Mltop.no_load_object"
           [< str"Loading of ML object file forbidden in a native Coq" >]
@@ -193,7 +175,15 @@ let mod_of_name name =
   in 
   String.capitalize base
 
-let file_of_name name = make_suffix (String.uncapitalize name) ".cmo"
+let file_of_name name =
+  let bname = String.uncapitalize name in
+  let fname = make_suffix bname ".cmo" in
+  if (is_in_path !coq_mlpath_copy fname) then fname
+  else let fname=make_suffix bname ".cma" in
+  if (is_in_path !coq_mlpath_copy fname) then fname
+  else
+    errorlabstrm "Mltop.load_object"
+      [< str"File not found on loadpath : "; str (bname^".cm[oa]") >]
 
 (* TODO: supprimer ce hack, si possible *)
 (* Initialisation of ML modules that need the state (ex: tactics like
-- 
cgit v1.2.3