diff options
| author |  thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-12 07:52:00 +0000 |
|---|---|---|
| committer | thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-12 07:52:00 +0000 |
| commit | 813f6748aadc060b76e6c4c4484d8e0de48ff7a8 (patch) | |
| tree | 1f39922ed783e39d23e92852aaf5e574843e5c47 /contrib/setoid_ring | |
| parent | 4641ee76a7258409a0a16b7b3a4b4d5b3ac76d92 (diff) | |
Fix name clash on left
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9234 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/setoid_ring')
| -rw-r--r-- | contrib/setoid_ring/Field_theory.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index 206367ba2..28f35c1a1 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -647,10 +647,14 @@ intros l e1 e2; elim e2; simpl; auto. Qed. Record rsplit : Type := mk_rsplit { - left : PExpr C; - common : PExpr C; - right : PExpr C}. - + rsplit_left : PExpr C; + rsplit_common : PExpr C; + rsplit_right : PExpr C}. + +(* Stupid name clash *) +Let left := rsplit_left. +Let right := rsplit_right. +Let common := rsplit_common. Fixpoint split (e1 e2: PExpr C) {struct e1}: rsplit := match e1 with |