Removed unused module Encode.Hints

ahelwer · Jan 25, 2024 · 7c13511 · 7c13511
1 parent e0ce4e6
commit 7c13511
Show file tree

Hide file tree

Showing 7 changed files with 2 additions and 154 deletions.
diff --git a/src/.depend b/src/.depend
@@ -918,20 +918,6 @@ encode/n_subst.cmx: encode/n_subst.mlt \
     util/deque.cmx \
     ctx.cmx \
     encode/n_subst.cmi
-encode/n_hints.cmo: encode/n_hints.mlt \
-    util/property.cmi \
-    util/ext.cmi \
-    expr.cmi \
-    util/deque.cmi \
-    builtin.cmi \
-    encode/n_hints.cmi
-encode/n_hints.cmx: encode/n_hints.mlt \
-    util/property.cmx \
-    util/ext.cmx \
-    expr.cmx \
-    util/deque.cmx \
-    builtin.cmx \
-    encode/n_hints.cmi
 encode/n_rewrite.cmo: encode/n_rewrite.mlt \
     type.cmi \
     util/property.cmi \
@@ -1011,6 +997,7 @@ encode/n_axioms.cmx: encode/n_axioms.mlt \
 encode/n_standardize.cmo: encode/n_standardize.mlt \
     type.cmi \
     util/property.cmi \
+    params.cmi \
     encode/n_table.cmi \
     encode/n_smb.cmi \
     util/ext.cmi \
@@ -1021,6 +1008,7 @@ encode/n_standardize.cmo: encode/n_standardize.mlt \
 encode/n_standardize.cmx: encode/n_standardize.mlt \
     type.cmx \
     util/property.cmx \
+    params.cmx \
     encode/n_table.cmx \
     encode/n_smb.cmx \
     util/ext.cmx \
@@ -1079,7 +1067,6 @@ encode.cmo: encode.mlt \
     encode/n_standardize.cmi \
     encode/n_smb.cmi \
     encode/n_rewrite.cmi \
-    encode/n_hints.cmi \
     encode/n_flatten.cmi \
     encode/n_axiomatize.cmi \
     encode.cmi
@@ -1088,7 +1075,6 @@ encode.cmx: encode.mlt \
     encode/n_standardize.cmx \
     encode/n_smb.cmx \
     encode/n_rewrite.cmx \
-    encode/n_hints.cmx \
     encode/n_flatten.cmx \
     encode/n_axiomatize.cmx \
     encode.cmi
@@ -2454,8 +2440,6 @@ encode/n_subst.cmi : \
     util/property.cmi \
     expr.cmi \
     util/deque.cmi
-encode/n_hints.cmi : \
-    expr.cmi
 encode/n_rewrite.cmi : \
     expr.cmi
 encode/n_table.cmi : \

diff --git a/src/Makefile b/src/Makefile
@@ -92,7 +92,6 @@ TYPE_PACK = \
 
 ENCODE_PACK = \
   encode/n_subst \
-  encode/n_hints \
   encode/n_rewrite \
   encode/n_table \
   encode/n_data \

diff --git a/src/encode.ml b/src/encode.ml
@@ -4,7 +4,6 @@
 
 (* Packaging module for the modules that implement PO transformations *)
 
-module Hints = N_hints
 module Rewrite = N_rewrite
 module Table = N_table
 module Smb = N_smb

diff --git a/src/encode.mli b/src/encode.mli
@@ -4,12 +4,6 @@
 
 (* Packaging module for the modules that implement PO transformations *)
 
-module Hints : sig
-  open Expr.T
-  val with_id : string
-  val main : sequent -> sequent
-end
-
 module Rewrite : sig
   open Expr.T
   val elim_bounds : sequent -> sequent

diff --git a/src/encode/n_hints.ml b/src/encode/n_hints.ml
diff --git a/src/encode/n_hints.mli b/src/encode/n_hints.mli
diff --git a/src/encode/n_hints.mlt b/src/encode/n_hints.mlt