aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/symbols.ml2
-rw-r--r--interp/symbols.mli2
-rw-r--r--interp/topconstr.ml4
-rw-r--r--interp/topconstr.mli4
4 files changed, 6 insertions, 6 deletions
diff --git a/interp/symbols.ml b/interp/symbols.ml
index b54c3323b7..60e16e7094 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -11,7 +11,7 @@
(*i*)
open Util
open Pp
-open Bignat
+open Bigint
open Names
open Nametab
open Libnames
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 5760f7c27a..e803d65e7c 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -11,7 +11,7 @@
(*i*)
open Util
open Pp
-open Bignat
+open Bigint
open Names
open Nametab
open Libnames
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c483327b64..56e2171e95 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -483,7 +483,7 @@ type cases_pattern_expr =
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_expr list
- | CPatNumeral of loc * Bignat.bigint
+ | CPatNumeral of loc * Bigint.bigint
| CPatDelimiters of loc * string * cases_pattern_expr
type constr_expr =
@@ -512,7 +512,7 @@ type constr_expr =
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr
| CNotation of loc * notation * constr_expr list
- | CNumeral of loc * Bignat.bigint
+ | CNumeral of loc * Bigint.bigint
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index a3224128a8..152a54dc01 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -77,7 +77,7 @@ type cases_pattern_expr =
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_expr list
- | CPatNumeral of loc * Bignat.bigint
+ | CPatNumeral of loc * Bigint.bigint
| CPatDelimiters of loc * string * cases_pattern_expr
type constr_expr =
@@ -106,7 +106,7 @@ type constr_expr =
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr
| CNotation of loc * notation * constr_expr list
- | CNumeral of loc * Bignat.bigint
+ | CNumeral of loc * Bigint.bigint
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t