From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/micromega/RingMicromega.v | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'plugins/micromega/RingMicromega.v') diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index ed49c3df..f066ea46 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (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). -- cgit v1.2.3