aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations2.out
Commit message (Collapse)AuthorAge
* Updating some output tests in test-suite:Gravatar herbelin2013-05-09
| | | | | | | | | | | | | | InitSyntax, PrintInfos: consequence of r16467 which improved printing of sigT Notations2: consequence of r16470 on using notations while asked to print the body of an abbreviation Notations: fix from r16417 was incomplete (and by the way associated to a wrong commit message) names: related to commit r16205 which aligned "In environment" with the variables of the environment (maybe should it be better to still have "In environment" printed after "Error: " but I don't know how to do it with a forced newline). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16503 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
| | | | | | | | | notations: - hopefully never 2 spaces when the user did not ask for - more systematic default insertion of spaces around symbols - e.g. have space before "[" if after a non-terminal - have spaces between consecutive terminals git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
| | | | | | | | | | | | | | | | | | | | | | | | - fixing missing spaces in the format of the exists' notations (Logic.v); - fixing wrong variable name in check_is_hole error message (topconstr.ml); - interpret expressions with open binders such as "forall x y, t" as "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid the "implicit type" of a variable being propagated to the type of another variable of different base name. An open question remains: when writing explicitly "forall (x y:_),t", should the types of x and y be the same or not. To avoid the "bug" that x and y have implicit types but the one of x takes precedences, I enforced the interpretation (in constrintern, not in parsing) that "forall (x y:_),t" means the same as "forall (x:_) (y:_),t". However, another choice could have been made. Then one would have to check that if x and y have implicit types, they are the same; also, glob_constr should ideally be changed to support a GProd and GLam with multiple names in the same type, especially if this type is an evar. On the contrary, one might also want e.g. "forall x y : list _, t" to mean "forall (x:list _) (y:list _), t" with distinct instanciations of "_" ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations with binders: Accepting using notations for functional termsGravatar herbelin2012-01-20
| | | | | | | which do not necessarily depend on their parameter (e.g. a notation for "fun x => t" might match also "fun _ => t"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14926 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite : an additional message displayed by Notation2.vGravatar letouzey2011-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.Gravatar letouzey2011-09-22
| | | | | | Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partly revert commit r14389 about relaxing the condition for being a keywordGravatar herbelin2011-08-10
| | | | | | | | | | | | | | (it does not work) Indeed, if a rule in operconstr at some level starts with an ident, it has to be declared as a keyword because other rules whose leftmost call is a call to operconstr will eventually the top level "200" even thought this leftmost operconstr might be declared at a lower level. This is for instance the reason why "True /\ forall x, x=0" is parsed even though /\ expects arguments at level less than 80 and forall is at level 200. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Be a bit less aggressive in declaring idents as keywords in notationsGravatar herbelin2011-08-08
| | | | | | | | | | | (an articulating ident needs to be a keyword if the constr entry that preceeds it is higher than the level of applications). Also fixed is_ident_not_keyword which only looked at the first letter and at the keyword status to decide if a token is an ident. This allowed to simplified define_keywords in Metasyntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing output of Notations2.v test messed up in r14060Gravatar herbelin2011-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing and completing interpretation of let's in notations for iterated binders.Gravatar herbelin2011-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14018 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing multiple printing bugs with "Notation f x := ..."Gravatar herbelin2011-04-08
| | | | | | | - Missing space and bad constr level in "About f" - Display of arguments missing when used as a pattern notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Did that adding a rule for printing applications as "f(x)" works.Gravatar herbelin2011-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13946 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
| | | | | | | | | | | | | - Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
| | | | | | | Note that the code is no longer in constrextern.ml but in topconstr.ml where the code for reversing notations of term already was. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13132 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some printing bugs.Gravatar herbelin2010-04-18
| | | | | | | | | | - Notations with coercions to funclass inserted were not working any longer since r11886. Made a fix but maybe should we eventually type the notations so that they have a canonical form (and in particular with coercions pre-inserted?). - Improved spacing management in printing extra tactic arguments "by" and "in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12951 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
| | | | | | | | | | - Adding test file related to commit 12080 (bug #2091). - Cleaning old parsing stuff from 8.0. - Support for camlp5 in base_include. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #2044 (bad printing of primitive notation at the head ofGravatar herbelin2009-02-06
coercion to funclass) [added a new notation output test as the initial one is quite saturated in miscellaneous notations]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11886 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 19:20:17 +0000