diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 16:40:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 16:40:48 +0200 |
| commit | 0db1d850b940a5f2351c1ec6e26d1f8087064d40 (patch) | |
| tree | 992670fc650c387f927de2f218dae94fa5e032e6 | |
| parent | 5ca744aef261972e3f0c6bbed1ef5bfe1c8cff2e (diff) | |
Moving Dnet-related code to tactics/.
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 1 | ||||
| -rw-r--r-- | tactics/dnet.ml (renamed from lib/dnet.ml) | 0 | ||||
| -rw-r--r-- | tactics/dnet.mli (renamed from lib/dnet.mli) | 0 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 2 | ||||
| -rw-r--r-- | tactics/term_dnet.ml (renamed from pretyping/term_dnet.ml) | 0 | ||||
| -rw-r--r-- | tactics/term_dnet.mli (renamed from pretyping/term_dnet.mli) | 0 |
8 files changed, 2 insertions, 4 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index fb8d4c73e..5a9acb6dd 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -39,7 +39,6 @@ Explore Predicate Rtree Heap -Dnet Genarg Stateid Ephemeron @@ -121,7 +120,6 @@ Cbv Pretype_errors Evarutil Evarsolve -Term_dnet Recordops Evarconv Arguments_renaming diff --git a/lib/lib.mllib b/lib/lib.mllib index edef3da03..b5421a8c8 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -16,7 +16,6 @@ Explore Predicate Rtree Heap -Dnet Unionfind Genarg Ephemeron diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 469be6d9e..a4c72f482 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -11,7 +11,6 @@ Cbv Pretype_errors Evarutil Evarsolve -Term_dnet Recordops Evarconv Arguments_renaming diff --git a/lib/dnet.ml b/tactics/dnet.ml index 22ca7e78d..22ca7e78d 100644 --- a/lib/dnet.ml +++ b/tactics/dnet.ml diff --git a/lib/dnet.mli b/tactics/dnet.mli index d2373a0d6..d2373a0d6 100644 --- a/lib/dnet.mli +++ b/tactics/dnet.mli diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 27ded2357..4eb4318ee 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,5 @@ Geninterp +Dnet Dn Btermdn Tacticals @@ -20,5 +21,6 @@ Tacenv TacticMatching Tacinterp Evar_tactics +Term_dnet Autorewrite Tactic_option diff --git a/pretyping/term_dnet.ml b/tactics/term_dnet.ml index e05f4bcfe..e05f4bcfe 100644 --- a/pretyping/term_dnet.ml +++ b/tactics/term_dnet.ml diff --git a/pretyping/term_dnet.mli b/tactics/term_dnet.mli index 7825ebdf1..7825ebdf1 100644 --- a/pretyping/term_dnet.mli +++ b/tactics/term_dnet.mli |