diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-12 10:41:06 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-12 10:41:06 +0000 |
| commit | 2c80742b0f1d8f51a7afcf533194a092c6007fad (patch) | |
| tree | a390ea4607cd8c07d6fe3c21ee9bd574e2d5b0d3 /contrib | |
| parent | 78a10cc3d8c46db0fd135c7ed0ee1040da1d2e03 (diff) | |
Comment fixed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1246 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/ring/ring.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 1a7722aee..b9cce1e29 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -558,7 +558,7 @@ let raw_polynom th op lc gl = List.fold_right2 (fun ci (c'i, c''i, c'i_eq_c''i) tac -> let c'''i = pf_nf gl c''i in - if pf_conv_x gl c'''i ci then tac (* Ring == Reflexivity *) + if pf_conv_x gl c'''i ci then tac (* convertible terms *) else (tclORELSE (tclORELSE |