diff options
| author | Pierre-Marie Pédrot | 2016-03-21 00:26:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-21 00:36:57 +0100 |
| commit | a581331f26d96d1a037128ae83bebd5e6c27f665 (patch) | |
| tree | a45c2df2962dffd9ccdab2806f23c717d87d9fdc /dev | |
| parent | df6132c06f9c8480b01f0a269cd1b95bbaa7f912 (diff) | |
Creating a dedicated ltac/ folder for Hightactics.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 7 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 2 |
3 files changed, 2 insertions, 8 deletions
diff --git a/dev/base_include b/dev/base_include index 767e023ea2..86f34b2ac9 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,6 +17,7 @@ #directory "grammar";; #directory "intf";; #directory "stm";; +#directory "ltac";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index fe896d3160..00e7f5c53c 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -19,13 +19,6 @@ highparsing : Files in parsing/ that cannot be linked too early. Contains the grammar rules g_*.ml4 -hightactics : - - Files in tactics/ that cannot be linked too early. - These are the .ml4 files that uses the EXTEND possibilities - provided by grammar.cma, for instance eauto.ml4. - - Special components ------------------ diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index b00d084edb..f9310e076a 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -20,7 +20,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ - -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ + -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ |