From 5a932e8c77207188c73629da8ab80f4c401c4e76 Mon Sep 17 00:00:00 2001 From: pboutill Date: Fri, 18 Jan 2013 15:21:02 +0000 Subject: Unset Asymmetric Patterns git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/Tauto.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'plugins/micromega/Tauto.v') diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index 440070a15..046c1b7cf 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -31,10 +31,10 @@ Set Implicit Arguments. Fixpoint eval_f (A:Type) (ev:A -> Prop ) (f:BFormula A) {struct f}: Prop := match f with - | TT => True - | FF => False + | TT _ => True + | FF _ => False | A a => ev a - | X p => p + | X _ p => p | Cj e1 e2 => (eval_f ev e1) /\ (eval_f ev e2) | D e1 e2 => (eval_f ev e1) \/ (eval_f ev e2) | N e => ~ (eval_f ev e) @@ -54,9 +54,9 @@ Set Implicit Arguments. Fixpoint map_bformula (T U : Type) (fct : T -> U) (f : BFormula T) : BFormula U := match f with - | TT => TT _ - | FF => FF _ - | X p => X _ p + | TT _ => TT _ + | FF _ => FF _ + | X _ p => X _ p | A a => A (fct a) | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2) | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2) @@ -172,9 +172,9 @@ Set Implicit Arguments. Fixpoint xcnf (pol : bool) (f : BFormula Term) {struct f}: cnf := match f with - | TT => if pol then tt else ff - | FF => if pol then ff else tt - | X p => if pol then ff else ff (* This is not complete - cannot negate any proposition *) + | TT _ => if pol then tt else ff + | FF _ => if pol then ff else tt + | X _ p => if pol then ff else ff (* This is not complete - cannot negate any proposition *) | A x => if pol then normalise x else negate x | N e => xcnf (negb pol) e | Cj e1 e2 => -- cgit v1.2.3