From ce11f55e27c8e4f98384aacd61ee67c593340195 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 2 May 2014 11:33:34 +0200 Subject: Fix extraction taking a type in the wrong environment. Fix restriction of universe contexts to not forget about potentially useful constraints. --- plugins/setoid_ring/Field_theory.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/setoid_ring/Field_theory.v') diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 10d54d228..ad7fbd871 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -588,13 +588,13 @@ Qed. (** Smart constructors for polynomial expression, with reduction of constants *) -Time Definition NPEadd e1 e2 := +Definition NPEadd e1 e2 := match e1, e2 with | PEc c1, PEc c2 => PEc (c1 + c2) | PEc c, _ => if (c =? 0)%coef then e2 else e1 + e2 | _, PEc c => if (c =? 0)%coef then e1 else e1 + e2 (* Peut t'on factoriser ici ??? *) - | _, _ => (@PEadd C e1 e2) + | _, _ => (e1 + e2) end%poly. Infix "++" := NPEadd (at level 60, right associativity). -- cgit v1.2.3