diff options
| author | letouzey | 2012-05-29 11:09:25 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:09:25 +0000 |
| commit | 463e46425b56360a158b44c61208060c64eb2ff5 (patch) | |
| tree | 7e55457a3aaa07032f8afb8528d027cac26245f4 /tactics | |
| parent | 51efb80ac1699a27e0003349bb766a430fbaf86a (diff) | |
place all files specific to camlp4 syntax extensions in grammar/
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 2 | ||||
| -rw-r--r-- | tactics/eqdecide.ml4 | 2 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/hipattern.ml4 | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 2 |
8 files changed, 8 insertions, 8 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index a749ba8ab5..d62320e769 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index fb692873e1..1cde368a11 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 1a65f62780..6a88843555 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -12,7 +12,7 @@ (* by Eduardo Gimenez *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Errors open Util diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 4677d87ef1..bff4f47601 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Pcoq diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index db55f6434a..82b08289da 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Pcoq diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 5abbe7ae98..bc91219112 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*) +(*i camlp4deps: "grammar/grammar.cma grammar/q_constr.cmo" i*) open Pp open Errors diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 004599f455..16eb595eaf 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 79c1797e41..0ab78fcd6c 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Term open Hipattern |