Various little fixes:

- allow a new line after a (** printing *) directive in coqdoc so as not
to output spurious new lines.
- never directly unify the lemma with an evar in setoid_rewrite (they
act as opaque constants).
- Fix a useless dependency introduced by tauto which splits a record in
SetoidList.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11799 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 1 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e38b9a6e69..6d01ea00c9 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -808,7 +808,8 @@ let refresh_hypinfo env sigma hypinfo =
   else ()
 
 let unify_eqn env sigma hypinfo t = 
-  try 
+  if isEvar t then None
+  else try 
     let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
     let env', prf, c1, c2, car, rel =
       let left = if l2r then c1 else c2 in