aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-04-26[ci] Fix another issue with the timing testsJason Gross
2018-04-26Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Hugo Herbelin
2018-04-23Fix #7327: coqchk subtyping of polymorphic constantsGaëtan Gilbert
2018-04-22test suite: clean more things (glob, MExtraction.out, distclean aux)Gaëtan Gilbert
2018-04-22test suite: print message for failing tests as they comeGaëtan Gilbert
2018-04-22test suite Makefile: do not use %.stamp for subsystem targetsGaëtan Gilbert
2018-04-20Fix #6798: coqchk ignores ugraph when comparing constant instancesGaëtan Gilbert
2018-04-16Merge PR #7237: [ssr] fix delayed clears (fix #7045)Maxime Dénès
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
2018-04-13[ssr] fix delayed clears (fix #7045)Enrico Tassi
2018-04-12Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...Jason Gross
2018-04-12Merge PR #500: Move bugs that have been closed on BugzillaMaxime Dénès
2018-04-12Merge PR #7087: Congruence tactic engine updatePierre-Marie Pédrot
2018-04-11Fix the status of some resolved bugsTej Chajed
2018-04-09Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Emilio Jesus Gallego Arias
2018-04-09Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilationPierre-Marie Pédrot
2018-04-09Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Maxime Dénès
2018-04-08Fixes #7195 (missing freshness condition in Ltac pattern-matching names).Hugo Herbelin
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
2018-04-06Fix #5539: algebraic universe produced by cases.Gaëtan Gilbert
2018-04-06Fix #6956: Uncaught exception in bytecode compilationMaxime Dénès
2018-04-05Improve shell scriptszapashcanon
2018-04-05Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.Théo Zimmermann
2018-04-04Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Hugo Herbelin
2018-04-04Merge PR #6407: Fix #6404 - Print tactics called by ML tacticsPierre-Marie Pédrot
2018-04-04ssr: check cleared hyps do exist (fix #7050)Enrico Tassi
2018-04-02Update coq_makefile timing testJason Gross
2018-04-02Fix #6404 - Print tactics called by ML tacticsJason Gross
2018-04-01Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Pierre-Marie Pédrot
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-30Fix #6257: anomaly with Printing Projections and Context.Gaëtan Gilbert
2018-03-29Fixes #7110 ("as" untested while looking for notation for nested patterns).Hugo Herbelin
2018-03-29Fix #6770: fixpoint loses locality info in proof mode.Gaëtan Gilbert
2018-03-29Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Pierre-Marie Pédrot
2018-03-28Supporting fix/cofix in Ltac pattern-matching (wish #7092).Hugo Herbelin
2018-03-28Merge PR #7090: stm: don't propagate side effects when editing a proofEmilio Jesus Gallego Arias
2018-03-28Merge PR #6961: [test-suite] Add backtracking test for `Load`.Enrico Tassi
2018-03-27stm: don't propagate side effects when editing a proofEnrico Tassi
2018-03-27Congruence: Fixing a bug with native projections.Hugo Herbelin
2018-03-27Fixing #5547 (typability of return predicate in nested pattern-matching).Hugo Herbelin
2018-03-27Fixing #5500 (missing test in return clause of match leading to anomaly).Hugo Herbelin
2018-03-26Fixes #7011 (Fix/CoFix were not considered in tactic unification).Hugo Herbelin
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2018-03-10[test-suite] Add backtracking test for `Load`.Emilio Jesus Gallego Arias
2018-03-09Merge PR #6946: Fix expected number of arguments for cumulative constructors.Maxime Dénès
2018-03-09Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...Maxime Dénès
2018-03-09Fix expected number of arguments for cumulative constructors.Gaëtan Gilbert
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Maxime Dénès
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 22:03:13 +0000