aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2016-08-23Fix bug #4904: [Import] does not load intermediately unqualified names of ↵Pierre-Marie Pédrot
aliases.
2016-08-21Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-21Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-20Fixing an anomaly in printing a unification error message.Hugo Herbelin
2016-08-19Test file for bug #4187.Pierre-Marie Pédrot
2016-08-19Merge remote-tracking branch 'origin/pr/246' into v8.6Matthieu Sozeau
2016-08-18Adding a test for bug #4653.Pierre-Marie Pédrot
2016-08-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-17Fixing #3070 ("subst" taking properly into account chains of dependencies).Hugo Herbelin
2016-08-16Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-29Fix bug #4673: regression in setoid_rewrite.Matthieu Sozeau
Modulo delta for types should be fully transparent.
2016-07-29Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-29Fix bug #3886, generation of obligations of fixesMatthieu Sozeau
This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
2016-07-29Fix #4769, univ poly and elim schemes in sectionsMatthieu Sozeau
2016-07-26Merge branch 'v8.6' into trunkPierre Letouzey
2016-07-26Fix bug #4754, allow conversion problems to remainMatthieu Sozeau
when checking that the rewrite relation is homogeneous in setoid_rewrite.
2016-07-21Fix bug #4679, weakened setoid_rewrite unificationMatthieu Sozeau
It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4.
2016-07-20Merge branch 'v8.6'Pierre-Marie Pédrot
2016-07-20Fix bug #4780: universe leak in letin_tacMatthieu Sozeau
2016-07-20Fix bug #4780: universe leak in letin_tacMatthieu Sozeau
2016-07-19Fix Errors.out missing a dot...Matthieu Sozeau
2016-07-19Some extra fixes in printing patterns in binders.Hugo Herbelin
- typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me.
2016-07-19Taking into account binding patterns when agglutinating sequences of binders.Hugo Herbelin
Supporting accordingly printing of sequences of binders including binding patterns.
2016-07-19Fixing missing parentheses in printing of patterns in binders.Hugo Herbelin
(In agreement with Daniel.)
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-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-18Marking bug #3383 as solved.Pierre-Marie Pédrot
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.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-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-12A short test on printing evars in Show Proof (this was wrong at some time).Hugo Herbelin
2016-07-08Fix test file for #4858.Maxime Dénès
2016-07-08Add test for pi_eq_proofs.Matthieu 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-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-07Merge remote-tracking branch 'github/bug4653' into v8.6Matthieu Sozeau
2016-07-07Program: fix #4873: transparency option not usedMatthieu Sozeau
2016-07-06Update csdp.cache.Maxime Dénès
2016-07-06Fixed bug #4622.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 08:33:51 +0000