aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2016-08-18Adding a test for bug #4653.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-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-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.5' into v8.6Pierre-Marie Pédrot
2016-07-13Fixing printing of evar name in an error message of instantiate.Hugo Herbelin
2016-07-08Fix test file for #4858.Maxime Dénès
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
2016-07-06Disallow dependent case on prim records w/o etaMatthieu Sozeau
2016-07-06Merge remote-tracking branch 'github/pr/199' into v8.5Maxime Dénès
Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
2016-07-06Fix test-suite file 3690Matthieu Sozeau
2016-07-05congruence fix: test-suite code and update CHANGESMatthieu Sozeau
This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards.
2016-07-04congruence/univs: properly refresh (fix #4609)Matthieu Sozeau
In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609.
2016-07-04test-suite: test checking of libraries checksum.Maxime Dénès
2016-07-02Adding test for #4811.Hugo Herbelin
2016-07-01Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).Hugo Herbelin
But there are still bugs with Declare Implicit Tactic, which should probably rather be reimplemented with ltac:(tac). Indeed, it does support evars in the type of the term, and solve_by_implicit_tactic should transfer universe constraints to the main goal. E.g., the following still fails, at Qed time. Definition Foo {T}{a : T} : T := a. Declare Implicit Tactic eassumption. Goal forall A (x : A), A. intros. apply Foo. Qed.
2016-06-29Fixing #4865 (deciding on which arguments to recompute scopes was not robust).Hugo Herbelin
See 4865.v for details.
2016-06-29Univs: Fix bug #4726Matthieu Sozeau
When using Record and an explicit sort constraint, the universe was wrongly made flexible and minimized.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 08:43:26 +0000