diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-25 12:19:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-25 12:19:39 +0000 |
| commit | e76a0434a8d88fb49543cedc9b342d8a1f7019b5 (patch) | |
| tree | 74165145f4f45ce38152bc622cec6f0853887227 /interp | |
| parent | ca0c3c0fe1b032113dbbe4b69b683c5669d79f4b (diff) | |
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèques de grands entiers relatifs munis des 4 opérations de base
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6505 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/symbols.ml | 2 | ||||
| -rw-r--r-- | interp/symbols.mli | 2 | ||||
| -rw-r--r-- | interp/topconstr.ml | 4 | ||||
| -rw-r--r-- | interp/topconstr.mli | 4 |
4 files changed, 6 insertions, 6 deletions
diff --git a/interp/symbols.ml b/interp/symbols.ml index b54c3323b..60e16e709 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 5760f7c27..e803d65e7 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 c483327b6..56e2171e9 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 a3224128a..152a54dc0 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 |