diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-25 11:17:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-25 11:17:06 +0000 |
| commit | 5ab19982880474727a9d0f0dcd36c7175afceb33 (patch) | |
| tree | 0c6155c64c770c97beec321a232e06cbfce5364f /pretyping | |
| parent | bd6de6aaae725104e41f1eb90afae4ee93711a41 (diff) | |
- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaient
disparus dès la version 1.11 de proofs/tacinterp.ml
- Prise en compte du contexte de filtrage sous-terme du but dans
'match goal with' quand des hypothèses aussi sont filtrées ce qui
avait disparu dans la version 1.56 de proofs/tacinterp.ml
- Restauration du filtrage sous-terme dans 'match c with' qui avait
disparu dans la version 1.27 de tactics/tacinterp.ml
- Nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6132 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions