diff options
| -rw-r--r-- | Makefile | 13 | ||||
| -rwxr-xr-x | dev/ocamldebug-v7 | 2 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 2 | ||||
| -rwxr-xr-x | theories/Arith/Arith.v | 1 | ||||
| -rw-r--r-- | theories/Zarith/Zsyntax.v | 3 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 22 |
6 files changed, 21 insertions, 22 deletions
@@ -44,7 +44,7 @@ OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS) CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE) -COQINCLUDES=-I parsing -I contrib/omega -I contrib/ring -I contrib/xml \ +COQINCLUDES=-I contrib/omega -I contrib/ring -I contrib/xml \ -I theories/Init -I theories/Logic -I theories/Arith \ -I theories/Bool -I theories/Zarith -I theories/Lists \ -I theories/Sets -I theories/Relations -I theories/Reals @@ -93,9 +93,10 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_vernac.cmo parsing/g_tactic.cmo \ parsing/g_constr.cmo parsing/g_cases.cmo \ parsing/extend.cmo parsing/esyntax.cmo \ - parsing/printer.cmo parsing/pretty.cmo parsing/egrammar.cmo + parsing/printer.cmo parsing/pretty.cmo parsing/egrammar.cmo \ + parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo -ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo +# ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo PROOFS=proofs/proof_type.cmo proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ @@ -120,15 +121,15 @@ HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \ CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ contrib/ring/quote.cmo contrib/ring/ring.cmo \ - contrib/xml/xml.cmo contrib/xml/cooking.cmo contrib/xml/xmlcommand.cmo \ - contrib/xml/xmlentries.cmo + contrib/xml/xml.cmo contrib/xml/cooking.cmo \ + contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ $(PROOFS) $(TACTICS) $(TOPLEVEL) $(HIGHTACTICS) $(CONTRIB) -CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx) +CMX=$(CMO:.cmo=.cmx) ########################################################################### # Main targets (coqmktop, coqtop.opt, coqtop.byte) diff --git a/dev/ocamldebug-v7 b/dev/ocamldebug-v7 index 4d8e3092a..7d609badb 100755 --- a/dev/ocamldebug-v7 +++ b/dev/ocamldebug-v7 @@ -3,7 +3,7 @@ # wrap around ocamldebug for Coq # export COQTOP=`coqtop -where` -export COQTOP=$HOME/coq/V7 +export COQTOP=$HOME/local/coq/V7 export COQLIB=$COQTOP export COQTH=$COQLIB/theories export CAMLP4LIB=`camlp4 -where` diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index ffa62cdf4..0723aec67 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -44,7 +44,7 @@ let camlp4objs = "q_coqast.cmo" ] let topobjs = camlp4objs -let gramobjs = ["g_zsyntax.cmo"; "g_natsyntax.cmo"] +let gramobjs = [] let notopobjs = gramobjs (* 5. High-level tactics objects *) diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index ab3a00ce7..1912f82d0 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -11,7 +11,6 @@ Require Export Between. Require Export Minus. Axiom My_special_variable : nat -> nat. -Declare ML Module "g_natsyntax". Grammar nat number :=. diff --git a/theories/Zarith/Zsyntax.v b/theories/Zarith/Zsyntax.v index df7551e6a..bdb5ca7a8 100644 --- a/theories/Zarith/Zsyntax.v +++ b/theories/Zarith/Zsyntax.v @@ -4,9 +4,6 @@ Require Export fast_integer. Require Export zarith_aux. -Declare ML Module "g_zsyntax". - - Axiom My_special_variable0 : positive->positive. Axiom My_special_variable1 : positive->positive. diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 3135d53fc..c5d628769 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -149,8 +149,8 @@ let init_with_state () = List.iter (fun f -> f()) (List.rev !init_list); init_list := [] -(* known_loaded_module contains the names of the loaded ML modules - * (linked or loaded with load_object). It is used not to loaded a +(* [known_loaded_module] contains the names of the loaded ML modules + * (linked or loaded with load_object). It is used not to load a * module twice. It is NOT the list of ML modules Coq knows. *) type ml_module_object = { mnames : string list } @@ -203,13 +203,15 @@ let cache_ml_module_object (_,{mnames=mnames}) = (fun name -> let mname = mod_of_name name in if not (module_is_known mname) then - let fname= file_of_name mname in - begin try - mSG [< 'sTR"[Loading ML file " ; 'sTR fname ; 'sTR" ..." >]; - load_object mname fname; - mSGNL [< 'sTR"done]" >] - with e -> - begin pPNL [< 'sTR"failed]" >]; raise e end + let fname = file_of_name mname in + begin + try + mSG [< 'sTR"[Loading ML file " ; 'sTR fname ; 'sTR" ..." >]; + load_object mname fname; + mSGNL [< 'sTR"done]" >] + with e -> + pPNL [< 'sTR"failed]" >]; + raise e end; add_loaded_module mname) mnames @@ -219,7 +221,7 @@ let specification_ml_module_object x = x let (inMLModule,outMLModule) = declare_object ("ML-MODULE", { load_function = cache_ml_module_object; - cache_function = (fun _ -> ()); + cache_function = cache_ml_module_object; open_function = (fun _ -> ()); specification_function = specification_ml_module_object }) |