aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2017-09-27Moving setting of "cleared" evar flag directly in Evd.restrict.Hugo Herbelin
In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further.
2017-09-27Fixing an old bug in collecting evars with cleared context.Hugo Herbelin
The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
2017-09-27Fixing an old bug in collecting evars with cleared context.Hugo Herbelin
The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-25BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsPaul Steckler
2017-09-25Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ↵Maxime Dénès
inductive types)
2017-09-25Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵Maxime Dénès
let-ins and non-recursively uniform parameters
2017-09-25Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵Maxime Dénès
4e70791).
2017-09-25Merge PR #1060: An optimization of tactic constructorMaxime Dénès
2017-09-23Fixing #5755 (discharging of inductive types not correct with let-ins).Hugo Herbelin
The number of effective parameters was used where the number of declarations in the signature of parameters should have been used.
2017-09-23Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Hugo Herbelin
2017-09-23Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Hugo Herbelin
The bug was caused by an inconsistency in different part of the code for deciding where cutting the context in between recursively uniform parameters and non-recursively uniform ones when let-ins were in the middle. We fix it by using uniformly "context_chop".
2017-09-22Make a test for coq_makefile portable.Pierre-Marie Pédrot
The validity of this test depended on Makefile issueing warnings in English. We simply force the global language of the shell to be C.
2017-09-21Report missing arguments in error messageTej Chajed
Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753.
2017-09-21A possible fix to BZ#5750 (ability to print context of ltac subterm match).Hugo Herbelin
The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1".
2017-09-20ssr: fix canonical strucut key comparison with primproj onEnrico Tassi
2017-09-19An optimization of tactic constructor.Hugo Herbelin
As was questioned on Stack Overflow and discussed on Gitter, reduction of the conclusion of the goal was done up to n+1 times for a failing call to "constructor" on an inductive type of n constructors. We do it at most once. Reworking the layout of the code at the same time.
2017-09-19Fixing bug #5741 (anomaly in info_trivial).Hugo Herbelin
The bug was introduced in 1559f73.
2017-09-19Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Maxime Dénès
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
2017-09-19test-suite: polymorphismMatthieu Sozeau
2017-09-19Allow declaring universe binders with no constraints with @{|}Gaëtan Gilbert
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
2017-09-19Merge PR #920: kernel: bugfix in filter_stack_domain.Maxime Dénès
2017-09-18Add test-suite script by Cyprien ManginMatthieu Sozeau
2017-09-15Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵Maxime Dénès
Inductive-keyworded record failing even on non-dependent goal)
2017-09-15Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Maxime Dénès
work better on them
2017-09-15Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵Maxime Dénès
anonymous variables)
2017-09-14Avoid extra failure in the "constructor" tactic (bug #5666).Guillaume Melquiond
This changes the implementation of "constructor" from constructor 1 + ... + constructor n + fail to constructor 1 + ... + constructor n.
2017-09-13Adding a test for utf8 characters in directory names.Hugo Herbelin
2017-09-12Fixing bug #5693 (treating empty notation format as any format).Hugo Herbelin
A trick in counting spaces in a format was making the empty notation not behaving correctly.
2017-09-12Fixing a bug of recursive notations introduced in dfdaf4de.Hugo Herbelin
When a proper notation variable occurred only in a recursive pattern of the notation, the notation was wrongly considered non printable due (the side effect that function compare_glob_constr and that mk_glob_constr_eq does not do anymore was indeed done by aux' but thrown away). This fixes it.
2017-09-12Fixing little inaccuracy in coercions to ident or name.Hugo Herbelin
For instance, we don't want "id@{u}" to be coerced to id, or "?[n]" to "_".
2017-09-11Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right ↵Maxime Dénès
artificially restricted to a non-empty context).
2017-09-07Merge PR #997: coqdoc: Support comments in verbatim outputMaxime Dénès
2017-09-04fix test-suite/coq-makefile/findlib-package on windowsEnrico Tassi
2017-09-03Addressing BZ#5713 (classical_left/classical_right artificially restricted).Hugo Herbelin
As explained in BZ#5713 report, the requirement for a non-empty context is not needed, so we remove it.
2017-08-31Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projectionsMaxime Dénès
2017-08-31Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateMaxime Dénès
2017-08-31Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagMaxime Dénès
2017-08-31Merge PR #958: coq_makefile: build/use .cma for packed plugins tooMaxime Dénès
2017-08-30Merge PR #998: Avoid running interactive tests on Windows.Maxime Dénès
2017-08-30Fixing part of #5707 (allowing destruct to use non dependent case analysis).Hugo Herbelin
The fix covers the case of a non-dependent goal with unavailable dependent case analysis: destruct was not seeing that it could still use non-dependent case analysis.
2017-08-29coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxsEnrico Tassi
2017-08-29Avoid running interactive tests on Windows.Maxime Dénès
This is a temporary workaround, until we fix the underlying issue which makes coqtop hang on those tests.
2017-08-29Properly handling parameters of primitive projections in cctac.Pierre-Marie Pédrot
2017-08-29Fix BZ#5697: Congruence does not work with primitive projections.Pierre-Marie Pédrot
The code generating the projection was unconditionally generating pattern-matchings, although this is incorrect for primitive records.
2017-08-29Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵Maxime Dénès
restructuration
2017-08-29Merge PR #830: Moving assert (the "Cut" rule) to new proof engineMaxime Dénès
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 16:31:22 +0000