diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-01 20:17:09 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-02 20:00:03 +0100 |
| commit | 761316ea73ad23be898470caa1a7bf839fa4a12e (patch) | |
| tree | 1062dbbc4eb1a37cddd4d42b0a68c6ce8b6d4622 | |
| parent | 4b68dbe3428740a61cda825d3a45047571d9f299 (diff) | |
Migrate back g_obligations in toplevel
This almost reverts commit 845d6f (r15248).
It isn't ideal to put syntactic stuff in the toplevel directory.
Maybe this kind of files should have someday their own directory
along with g_rewrite.ml4 and some other (maybe a extraparsing dir?).
Meanwhile, this commit leads to a cleaner situation concerning *.ml4:
- everything needed to build grammar.cma (and q_constr.cmo) is in:
lib/ kernel/ library/ pretyping/ interp/ proofs/ parsing/ grammar/
- all *.ml4 using grammar.cma (or q_constr.cmo) are in:
tactics/ toplevel/ plugins/*/
| -rw-r--r-- | toplevel/g_obligations.ml4 (renamed from parsing/g_obligations.ml4) | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/parsing/g_obligations.ml4 b/toplevel/g_obligations.ml4 index 2354aa332..2354aa332 100644 --- a/parsing/g_obligations.ml4 +++ b/toplevel/g_obligations.ml4 |