Quelques modifications autour du filtrage Ltac:

- Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas
  où c'est le n-ième sous-termes qui finalement réussit (passage à une
  complexité en n plutôt que n^2, via l'utilisation de continuations).
- Sémantique du filtrage: suppression dans sub_match de la recherche
  dans le type des let (puisque ce n'est pas cencé être une
  information utilisateur) mais rajout de la recherche dans le champ
  cast qui lui est utilisateur.
- Nouvelle fonctionnalité: récupération des noms des variables liantes
  filtrées (dans matches/sub_match) et utilisation de ces noms dans
  ltac (utile pour récupérer x dans "exists x, P x");



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

0 files changed, 0 insertions, 0 deletions