diff options
| -rw-r--r-- | _tags | 6 | ||||
| -rw-r--r-- | myocamlbuild.ml | 12 | ||||
| -rw-r--r-- | plugins/_tags | 4 | ||||
| -rw-r--r-- | plugins/pluginsbyte.itarget | 2 | ||||
| -rw-r--r-- | plugins/pluginsopt.itarget | 2 | ||||
| -rw-r--r-- | plugins/pluginsvo.itarget | 2 | ||||
| -rw-r--r-- | theories/theories.itarget | 2 |
7 files changed, 14 insertions, 16 deletions
@@ -9,12 +9,16 @@ <tools/coq_makefile.{native,byte}> : use_str <tools/coqdoc/main.{native,byte}> : use_str <checker/main.{native,byte}> : use_str, use_unix, use_gramlib -<plugins/micromega/csdpcert.{native,byte}> : use_nums +<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix ## tags for ide <ide/**/*.{ml,mli}>: thread, ide +## tags for grammar.cm* + +<parsing/grammar.{cma,cmxa}> : use_unix + ## tags for camlp4 files <**/*.ml4>: is_ml4 diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 963adcc7c..f7c014aba 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -124,18 +124,18 @@ let theoriesv = let vo = string_list_of_file "theories/theories.itarget" in List.map (fun s -> "theories/"^(Filename.chop_suffix s "o")) vo -let contribv = +let pluginsv = let vo = string_list_of_file "plugins/pluginsvo.itarget" in List.map (fun s -> "plugins/"^(Filename.chop_suffix s "o")) vo -let contribmllib = +let pluginsmllib = let cma = string_list_of_file "plugins/pluginsbyte.itarget" in List.map (fun s -> "plugins/"^(Filename.chop_suffix s ".cma")^".mllib") cma (** for correct execution of coqdep_boot, source files should have been imported in _build (and NMake.v should have been created). *) -let coqdepdeps = theoriesv @ contribv @ contribmllib +let coqdepdeps = theoriesv @ pluginsv @ pluginsmllib let coqtop = "toplevel/coqtop" let coqide = "ide/coqide" @@ -209,9 +209,11 @@ let incl f = Ocaml_utils.ocaml_include_flags f let cmd cl = (fun _ _ -> (Cmd (S cl))) let initial_actions () = begin - make_bin_links all_binaries; - (** We "pre-create" a few subdirs in _build to please coqtop *) + (** We "pre-create" a few subdirs in _build *) Shell.mkdir_p (!_build^"/dev"); + Shell.mkdir_p (!_build^"/bin"); + Shell.mkdir_p (!_build^"/plugins/micromega"); + make_bin_links all_binaries; end let extra_rules () = begin diff --git a/plugins/_tags b/plugins/_tags index 6d28450fd..f95e0c5b8 100644 --- a/plugins/_tags +++ b/plugins/_tags @@ -3,8 +3,6 @@ "cc/g_congruence.ml4": use_grammar "setoid_ring/newring.ml4": use_grammar "dp/g_dp.ml4": use_grammar -"interface/centaur.ml4": use_grammar -"interface/debug_tac.ml4": use_grammar "quote/g_quote.ml4": use_grammar "subtac/equations.ml4": use_grammar, use_extend "subtac/g_eterm.ml4": use_grammar @@ -23,12 +21,10 @@ "groebner/ideal.ml4": use_refutpat "groebner/groebner.ml4": use_grammar - "cc": include "extraction": include "firstorder": include "funind": include -"interface": include "micromega": include "quote": include "romega": include diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget index 7e0a77787..7ca8020dc 100644 --- a/plugins/pluginsbyte.itarget +++ b/plugins/pluginsbyte.itarget @@ -3,8 +3,6 @@ setoid_ring/newring_plugin.cma extraction/extraction_plugin.cma firstorder/ground_plugin.cma rtauto/rtauto_plugin.cma -interface/coqinterface_plugin.cma -interface/coqparser_plugin.cma fourier/fourier_plugin.cma romega/romega_plugin.cma omega/omega_plugin.cma diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget index e8e7868b7..520627115 100644 --- a/plugins/pluginsopt.itarget +++ b/plugins/pluginsopt.itarget @@ -3,8 +3,6 @@ setoid_ring/newring_plugin.cmxa extraction/extraction_plugin.cmxa firstorder/ground_plugin.cmxa rtauto/rtauto_plugin.cmxa -interface/coqinterface_plugin.cmxa -interface/coqparser_plugin.cmxa fourier/fourier_plugin.cmxa romega/romega_plugin.cmxa omega/omega_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget index af4d23310..14c288005 100644 --- a/plugins/pluginsvo.itarget +++ b/plugins/pluginsvo.itarget @@ -8,8 +8,6 @@ fourier/Fourier.vo funind/Recdef.vo groebner/GroebnerR.vo groebner/GroebnerZ.vo -interface/CoqInterface.vo -#interface/CoqParser.vo (should not be compiled) micromega/CheckerMaker.vo micromega/EnvRing.vo micromega/Env.vo diff --git a/theories/theories.itarget b/theories/theories.itarget index 019047ef5..99b059f51 100644 --- a/theories/theories.itarget +++ b/theories/theories.itarget @@ -42,6 +42,7 @@ Classes/SetoidAxioms.vo Classes/SetoidClass.vo Classes/SetoidDec.vo Classes/SetoidTactics.vo +Classes/RelationPairs.vo FSets/FMapAVL.vo FSets/FMapFacts.vo @@ -89,6 +90,7 @@ Structures/DecidableType2.vo Structures/DecidableType2Ex.vo Structures/DecidableType2Facts.vo Structures/OrderTac.vo +Structures/GenericMinMax.vo Init/Datatypes.vo Init/Logic_Type.vo |