- Relâchement de la contrainte de bonne longueur des intropatterns

  lorsqu'en position terminale (en fait, l'idéal serait de pouvoir
  mettre des tactiques dans les branches, style "intros [H ; tac | ]")
  (cf un exemple QvMake.v)
- Pas de delta du tout quand on fait de la recherche de sous-terme
  (même lorsqu'on vient de apply avec une conclusion ?P t) (cf un
  exemple dans Rocq/DEMOS/Sorting.v)



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

0 files changed, 0 insertions, 0 deletions