aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-04-02Update coq_makefile timing testJason 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-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-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
2018-03-09Cumulativity: improve treatment of irrelevant universes.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09Merge PR #6480: Allow Prop as source for coercionsMaxime Dénès
2018-03-09Merge PR #6895: [compat] Remove "Refolding Reduction" option.Maxime Dénès
2018-03-09added test for coercion from typecharguer
2018-03-09allow Prop as source for coercionscharguer
2018-03-09Merge PR #6945: Fix error with univ binders on monomorphic records.Maxime Dénès
2018-03-09Merge PR #6155: Get rid of ' notation for Zpos in QArithMaxime Dénès
2018-03-09Merge PR #6747: Relax conversion of constructors according to the pCuIC modelMaxime Dénès
2018-03-09Merge PR #6328: Fix #6313: lost goals in nested ltac in refineMaxime Dénès
2018-03-09Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesMaxime Dénès
2018-03-08More examples about shelve/given_up in tactic-in-terms.Hugo Herbelin
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
2018-03-08Merge PR #6522: Fix core hint database issue #6521Maxime Dénès
2018-03-08Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsMaxime Dénès
2018-03-08Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Maxime Dénès
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
2018-03-08Fix error with univ binders on monomorphic records.Gaëtan Gilbert
2018-03-08Fix SR breakage due to allowing fixpoints on non-rec valuesMatthieu Sozeau
2018-03-08Add test-suite file for cumulative constructorsMatthieu Sozeau
2018-03-08Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Maxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-08Merge PR #6903: [compat] Remove "Shrink Abstract"Maxime Dénès
2018-03-08Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Maxime Dénès
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-07Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Maxime Dénès
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Maxime Dénès
2018-03-06ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Enrico Tassi
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-05CHANGES and tests for with Definition @{univs}Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 12:21:29 +0000