aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/evar_tactics.mli
Commit message (Collapse)AuthorAge
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
| | | | | | | | | | | | | | | - make the modifiers "value of" and "type of" for "set" working (it was not!), - clear unselected hypotheses in the "in" clause of "induction/destruct" when the destructed term is a variable (experimental), - support for generalization of hypotheses in the induction hypotheses using the "in" clause of "induction" (e.g. "induction n in m, H" will generalize over m -- would it be better to have an explicit "over"/"generalizing" clause ?). Added clause "as" to "apply in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11509 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-tĂȘteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* more evar stuffGravatar corbinea2004-06-28
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7