aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/intros.v
Commit message (Collapse)AuthorAge
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
| | | | | | | | | | (the action is "clear"). Added subst_intropattern which was missing since the introduction of ApplyOn intro patterns. Still to do: make "intros _ ?id" working without interferences when "id" is precisely the internal name used for hypotheses to discard.
* Fixing introduction patterns * and ** when used in a branch so that they do ↵Gravatar Hugo Herbelin2014-05-31
| | | | not introduce beyond what is under control of the branch. See test-suite intros.v for an example.
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
| | | | | | | | Added full betaiota in hnf. This seems more natural, even if it changes the strict meaning of hnf. This is source of incompatibilities as "intro" might succeed more often. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 17:57:29 +0000