| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
variable is used both as term and as binder, resulting in
ununderstandable error message about scopes).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15642 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Reset and the other backtracking commands (Back, BackTo, Backtrack)
are now allowed only during interactive session, not in compiled
or loaded scripts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15087 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
was provoking an anomaly instead of a regular error).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15070 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
interpretation order of scoped notations).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14819 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
(the number of entries to reset was not correct).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14778 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Probably something related with the unicode lambda syntax...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13911 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Thanks to Marc Lasson for the analysis of the problem and for the
initial patch.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
(currently only one expansion but could be virtually made user-parametrizable).
Also fixed a bug in recursive notations happening with multiple-tokens
separators (see Notations.v in test-suite).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12881 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Deactivation of short names registration and printing for
abbreviations to identical names, what avoids printing uselessly
qualified names binding where the short name is in fact equivalent.
- New treatment of abbreviations to names: don't insert any maximally
inserted implicit arguments at all at the time of the abbreviation
and use the regular internalization strategy to have them inserted
at use time.
- The previous modifications altogether make redirections of
qualified names easier and avoid the semantic change of r12349 and
hence allows to keep "Notation b := @a" as it was before, i.e. as a
notation for the deactivation of the implicit arguments of a.
- Took benefit of these changes and updated nil/cons/list/app
redefinition in "List.v".
- Fixed parsing/printing notation bugs (loop on partially applied
abreviations for constructors in constrintern.ml + bad reverting of
notations with holes that captured non anonymous variables in
match_cases_pattern).
- Add support for parsing/printing abbreviations to @-like constructors
and for reverting printing for abbreviations to constructors applied
to parameters only (function extern_symbol_pattern).
- Minor error messages fixes and minor APIs cleaning.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
implicit arguments and scope (use Implicit Arguments or Arguments
Scope commands instead if not the desired behaviour).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Implicit Arguments, Arguments Scope and Coercion fixed, noneffective
Global in sections for Hints and Notation detected).
Misc. improvements (comments + interpretation of Hint Constructors +
dev printer for hint_db).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
(see Notations.v).
Improved the "already occurs in a different scope" test and message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12399 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
Not_found bug in Theorem with) from V8.2 to trunk.
- Improving indentation in presence of tabulation and utf-8 when
reporting error messages with "^^^^^^".
- Updating a few svn:ignore properties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
late 2008 Coq WG.
- Updated Copyright file wrt JProver.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11781 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Application to the test of notation import from within a section.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11652 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
camlp4 (faire l'initialisation dans l'ordre: les sous-niveaux vides,
eux-mêmes dans l'ordre, avant de créer le niveau de la notation elle-même).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11220 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
camlp4. Petit nettoyage en passant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10987 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8720 85f007b7-540e-0410-9357-904b9bb8a0f7
|
herbelin
letouzey
glondu