- Extracted from the tactic "now" an experimental tactic "easy" for small

  automation.
- Permitted to use evars in the intermediate steps of "apply in" (as expected 
  in the test file apply.v).
- Back on the systematic use of eq_rect (r11697) for implementing
  rewriting (some proofs, especially lemma DistOoVv in
  Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in
  Sophia-Antipolis/Semantics/example2.v are explicitly refering
  to the name of the lemmas used for rewriting).
- Fixed at the same time a bug in get_sort_of (predicativity of Set was not
  taken into account).



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

0 files changed, 0 insertions, 0 deletions