diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-03-06 16:12:28 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-03-07 17:31:46 +0000 |
| commit | 66c523bcac8b64e202baa084bf24f5b57c61fcd6 (patch) | |
| tree | b3772186b0829ff27c76c05ae1bec44173758c01 /plugins/micromega | |
| parent | 144517d764f11b8b79e8f7adfeca0d075dd4ac19 (diff) | |
[stdlib] Do not use “Require” inside sections
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/RingMicromega.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 543a37ff8..f066ea462 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -21,6 +21,7 @@ Require Import List. Require Import Bool. Require Import OrderedRing. Require Import Refl. +Require Coq.micromega.Tauto. Set Implicit Arguments. @@ -796,7 +797,7 @@ Definition xnormalise (t:Formula C) : list (NFormula) := | OpLe => (psub lhs rhs ,Strict) :: nil end. -Require Import Coq.micromega.Tauto. +Import Coq.micromega.Tauto. Definition cnf_normalise (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnormalise t). |