aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-08 16:40:48 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-08 16:40:48 +0200
commit0db1d850b940a5f2351c1ec6e26d1f8087064d40 (patch)
tree992670fc650c387f927de2f218dae94fa5e032e6
parent5ca744aef261972e3f0c6bbed1ef5bfe1c8cff2e (diff)
Moving Dnet-related code to tactics/.
-rw-r--r--dev/printers.mllib2
-rw-r--r--lib/lib.mllib1
-rw-r--r--pretyping/pretyping.mllib1
-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.mllib2
-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