diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-02 11:33:34 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:01 +0200 |
| commit | ce11f55e27c8e4f98384aacd61ee67c593340195 (patch) | |
| tree | 9537fb3faf09eb0bb67eef5a25be7cca2516040a /plugins/setoid_ring/Field_theory.v | |
| parent | af533645b1033dc386d8ac99cc8c4b6491b0ca91 (diff) | |
Fix extraction taking a type in the wrong environment.
Fix restriction of universe contexts to not forget about potentially useful
constraints.
Diffstat (limited to 'plugins/setoid_ring/Field_theory.v')
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 4 |
1 files changed, 2 insertions, 2 deletions
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). |