| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
Compared to the original proposition (59a594b in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
| |
|
|
|
|
|
|
|
|
| |
The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.
Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Marking it as experimental.
|
| |
|
|
|
|
| |
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
|
| |
|
|
| |
of temporary hypotheses than 76f27140e6e34 did.
|
| |
|
|
|
| |
ago) which broke compilation of theories/Logic/WKL.v (collision
between a temporary name and a user name).
|
| |
|
|
|
|
|
|
| |
an initial hypothesis hyp at the same position in the context.
Ensuring the same for "apply c in hyp as pat".
Ensuring that "pose proof (H ...) as H" does not change the position of H.
|
| |
|
|
|
|
|
|
|
|
| |
(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.
|
| |
|
|
| |
not introduce beyond what is under control of the branch. See test-suite intros.v for an example.
|
| |
|
|
|
|
|
|
| |
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
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Hugo Herbelin
Théo Zimmermann
herbelin