diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-24 11:25:18 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-24 11:25:18 +0000 |
| commit | 355671c60fa075b64f64e175bada909a4ce759ac (patch) | |
| tree | e2ade8e51a0e377dac068c43d469951274513f89 /parsing/g_prim.ml4 | |
| parent | 13517a671562062b32fbe90106098854faa46525 (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@6499 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_prim.ml4')
| -rw-r--r-- | parsing/g_prim.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 6973a551d..10ffbecaf 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -33,7 +33,7 @@ let local_make_binding loc a b = let local_append l id = l@[id] GEXTEND Gram - GLOBAL: ident natural integer bigint string preident ast + GLOBAL: bigint ident natural integer string preident ast astlist qualid reference dirpath identref name base_ident var hyp; (* Compatibility: Prim.var is a synonym of Prim.ident *) @@ -66,8 +66,8 @@ GEXTEND Gram [ [ i = INT -> local_make_posint i ] ] ; bigint: - [ [ i = INT -> Bignat.POS (Bignat.of_string i) - | "-"; i = INT -> Bignat.NEG (Bignat.of_string i) ] ] + [ [ i = INT -> Bigint.of_string i + | "-"; i = INT -> Bigint.neg (Bigint.of_string i) ] ] ; integer: [ [ i = INT -> local_make_posint i |