Revert "Make it apparent (with Poly/ML for now) that Arbint.int = Int…

…Inf.int" This reverts commit e38b007. This makes the repl's I/O behaviour differ depending on whether or not Poly has been compiled with IntInf by default because the custom HOL pretty-printer will/won't get installed for IntInf. This is causing Github regression errors.
HOL-Theorem-Prover · Oct 28, 2024 · d313757 · d313757
1 parent f7bb5bb
commit d313757
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/portableML/Arbint.sig b/src/portableML/Arbint.sig
@@ -1,7 +1,7 @@
 signature Arbint =
 sig
 
-  include Arbintcore
+  include Arbintcore where type int = Arbintcore.int
   val pp_int     : int -> HOLPP.pretty
 
 end
diff --git a/src/portableML/poly/Arbintcore.sig b/src/portableML/poly/Arbintcore.sig
@@ -1,7 +1,7 @@
 signature Arbintcore =
 sig
 
-  type int = IntInf.int
+  eqtype int
 
   type num = Arbnumcore.num