aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-07-19Notations: fixing multiple binders used as terms in reverse order.Hugo Herbelin
2016-07-19Removing a source of clash with multiple recursive patterns in notations.Hugo Herbelin
The same variable name was used to collect the binders and the successive steps of matching one binder, resulting in unexpected attempts for merging in the presence of multiple occurrence of the same recursive pattern. An amusing side-effect: when eta-expanding for a notation with recursive binders, it is the second variable of the "x .. y" which is used to invent a name rather than the first one.
2016-07-19Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp).Hugo Herbelin
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns).
2016-07-18Replacing deprecated Implicit Arguments in prelude.Maxime Dénès
Was triggering a deprecation warning.
2016-07-18Remove the swap tactic from the prelude.Maxime Dénès
It was anyway unusable due to a parsing conflict with the swap operator on goals. Was triggering a warning when compiling the prelude.
2016-07-18Marking bug #3383 as solved.Pierre-Marie Pédrot
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
2016-07-18Removing useless grammar entries. Fixes bug #4919.Pierre-Marie Pédrot
2016-07-17Partial fix to #4592 (notation requiring alpha-conversion for printing).Hugo Herbelin
2016-07-17More examples of recursive notations, with emphasis in reference manual.Hugo Herbelin
Further work would include: - Identify binders up to alpha-conversion (see #4932 with a list of binders of length at least 2, or #4592 on printing notations such as ex2). A cool example that one could also consider supporting: - Notation "[[ a , .. , b | .. | a , .. , b ]]" := (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
2016-07-17Fixing a bug in recognizing a recursive pattern of notationsHugo Herbelin
immediately in the scope of another recursive pattern.
2016-07-17Fixing interpretation of notations w/ opposite instances of a recursive pattern.Hugo Herbelin
2016-07-17Fixing printing of notations with several instances of a recursive pattern.Hugo Herbelin
2016-07-17First step in adding printing for notations such as given in #4932.Hugo Herbelin
In particular, it becomes possible to have recursive patterns used shared by binders and terms. Currently limited by alpha-conversion issues (e.g. test2 from 4932.v is not reprinted).
2016-07-17Fixing #4932 (anomaly when using binders as terms in recursive notations).Hugo Herbelin
This application was actually not anticipated. It is nice and was not too difficult to support. Design for pattern binders maybe to clarify. When seing pat(x1,..,xn) as a term, I just reused pat(x1,..,xn), but maybe it is worth using the variable aliasing the pattern, for more a concise notation. But at the same time, this means exposing the internal name of the alias which is not so elegant.
2016-07-16Fixing a collision about the meta-variable ".." in recursive notations.Hugo Herbelin
This happens when recursive notations are used to define recursive notations.
2016-07-13Merge branch 'v8.6'Pierre-Marie Pédrot
2016-07-13Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-13Fixing printing of evar name in an error message of instantiate.Hugo Herbelin
2016-07-13Typo.Hugo Herbelin
2016-07-13Makefile.dev: fix a typo in the 'logic' rulePierre Letouzey
2016-07-13Makefile.dev: fix a typo in the 'logic' rulePierre Letouzey
2016-07-12Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4Pierre Letouzey
- With the ?= construction, we avoid warnings about undefined variables, while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make' - Some extra documentation and cleanup
2016-07-12.gitignore: no more generated grammar/*.ml filesPierre Letouzey
2016-07-12Makefile: no more .ml4.d hence no more rule to clean themPierre Letouzey
2016-07-12A short test on printing evars in Show Proof (this was wrong at some time).Hugo Herbelin
2016-07-12Renouncing for uniformity to the few instances of pf_interp_* in Tacinterp.Hugo Herbelin
2016-07-12".gitignore" updateMatej Kosik
2016-07-12removing ocamldoc-related syntax errorsMatej Kosik
2016-07-12expanding "make help" a little bitMatej Kosik
2016-07-12Removing "READABLE_ML4=" from "Makefile.build"Matej Kosik
2016-07-11Removing "VERBOSE=" from "Makefile.build"Matej Kosik
2016-07-08Fixing the printing of unknown locations by adding a newline.Pierre-Marie Pédrot
2016-07-08Adding a breaking space in warning names.Pierre-Marie Pédrot
2016-07-08Remove spurious warnings about projections when requiring modules.Pierre-Marie Pédrot
2016-07-08Add a few fixes in CHANGES that were forgotten.Maxime Dénès
We should really automate the generation of the log of fixes for CHANGES.
2016-07-08Fix test file for #4858.Maxime Dénès
2016-07-08Fixing #4906 (regression in printing an error message).Hugo Herbelin
2016-07-08Typo in a comment of stdlib.Hugo Herbelin
2016-07-08Add test for pi_eq_proofs.Matthieu Sozeau
2016-07-08Program: Move ProofIrrelevance to Subset.vMatthieu Sozeau
2016-07-08Update csdp.cache.Maxime Dénès
2016-07-08Test file for #4858.Maxime Dénès
2016-07-08Add test file for #4880.Maxime Dénès
2016-07-08Update COPYRIGHT.Maxime Dénès
2016-07-08Merge remote-tracking branch 'github/pr/243' into v8.5Maxime Dénès
Was PR#243: fixing nsatz
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-07Merge remote-tracking branch 'github/bug4653' into v8.6Matthieu Sozeau
2016-07-07Prevent "Load" from displaying all the intermediate subgoals.Guillaume Melquiond
Note that even "Load Verbose" is not supposed to display them.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 15:09:25 +0000