diff options
| author | filliatr | 2000-10-27 08:46:13 +0000 |
|---|---|---|
| committer | filliatr | 2000-10-27 08:46:13 +0000 |
| commit | 751620c70bd3a77ed8fde7cca9e3893f339643b3 (patch) | |
| tree | 517f1e98436989ba549f36f4c895624482e1419e /theories | |
| parent | fc6300ffd9d98da50b6302e11742ac29eb572366 (diff) | |
g_natsyntax et g_zsyntax maintenant toujours linkes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Arith/Arith.v | 1 | ||||
| -rw-r--r-- | theories/Zarith/Zsyntax.v | 3 |
2 files changed, 0 insertions, 4 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index ab3a00ce7b..1912f82d05 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -11,7 +11,6 @@ Require Export Between. Require Export Minus. Axiom My_special_variable : nat -> nat. -Declare ML Module "g_natsyntax". Grammar nat number :=. diff --git a/theories/Zarith/Zsyntax.v b/theories/Zarith/Zsyntax.v index df7551e6ab..bdb5ca7a80 100644 --- a/theories/Zarith/Zsyntax.v +++ b/theories/Zarith/Zsyntax.v @@ -4,9 +4,6 @@ Require Export fast_integer. Require Export zarith_aux. -Declare ML Module "g_zsyntax". - - Axiom My_special_variable0 : positive->positive. Axiom My_special_variable1 : positive->positive. |