diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-02 10:46:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-02 10:46:25 +0000 |
| commit | d4c5a863d35bb131b7236fd5df48cfc882c0b0f1 (patch) | |
| tree | 97d965fdb63c10f634588aee32a53e093e21997f /contrib7 | |
| parent | b8145043da6f504d60abf4f4aa4be24bf774b215 (diff) | |
Utilisation Z_scope
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6982 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib7')
| -rw-r--r-- | contrib7/omega/OmegaLemmas.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/contrib7/omega/OmegaLemmas.v b/contrib7/omega/OmegaLemmas.v index f9027d348..b27afd0dd 100644 --- a/contrib7/omega/OmegaLemmas.v +++ b/contrib7/omega/OmegaLemmas.v @@ -10,6 +10,8 @@ Require ZArith_base. +Open Scope Z_scope. + (** These are specific variants of theorems dedicated for the Omega tactic *) Lemma new_var: (x:Z) (EX y:Z |(x=y)). |