diff options
| author |  clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-10 12:03:08 +0000 |
|---|---|---|
| committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-10 12:03:08 +0000 |
| commit | 9c007d7d9744bababdb8b57da0a7ee7835bac434 (patch) | |
| tree | 2902f1610752a83a809cbf88a02bd1356b82bd65 /contrib/ring/Ring_normalize.v | |
| parent | d751d60b0511ff3daeb0bcd1384e3e982c410fa9 (diff) | |
Ajout d'un Ring pour setoides
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1839 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring/Ring_normalize.v')
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 94b5093c7..f44f554e0 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -457,6 +457,7 @@ Trivial. Elim (varlist_lt v v0); Simpl. Repeat Rewrite ics_aux_ok. Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto. + Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto. (* monom and varlist *) |