aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
2018-06-05Make direct invocations of `simple apply` obey `Opaque` directive.Maxime Dénès
2018-06-04Merge PR #7229: Deprecate implicit tactic solving.Hugo Herbelin
2018-06-04Merge PR #7486: Update old parts of CHANGES to use current bug numbers.Hugo Herbelin
2018-06-04Documenting the deprecation.Pierre-Marie Pédrot
2018-05-28Add CHANGES entryMaxime Dénès
2018-05-24[tactics] Remove anonymous fix/cofix form.Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-17Document nested proofs and associated option.Théo Zimmermann
2018-05-11Update old parts of CHANGES to use current bug numbers.Théo Zimmermann
2018-05-11Notations: advertize that distinct "only parsing"/"only printing" rules work.Hugo Herbelin
2018-05-02Make "intro"/"intros" progress on existential variables.Hugo Herbelin
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-23Merge PR #7244: Making tactic-in-term aware of "Set Ltac Debug"Pierre-Marie Pédrot
2018-04-16Fix typo in CHANGES.Maxime Dénès
2018-04-16Mention other deprecations and fixes in CHANGESMaxime Dénès
2018-04-16CHANGES: document COQFLAGS changeRalf Jung
2018-04-16Merge PR #7200: [ltac] Deprecate nameless fix/cofix.Maxime Dénès
2018-04-14Add missing CHANGES entry for #6169.Théo Zimmermann
2018-04-13Making tactic-in-term aware of "Set Ltac Debug".Hugo Herbelin
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
2018-04-09Merge PR #7103: Fix #7101: STM delegation policy brokenEnrico Tassi
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-30Add CHANGES for removing Implicit Arguments and Arguments ScopeJasper Hugunin
2018-03-28Supporting fix/cofix in Ltac pattern-matching (wish #7092).Hugo Herbelin
2018-03-28Fix #7101: STM delegation policy brokenMaxime Dénès
2018-03-23Merge PR #7018: Fix typo in CHANGES.Maxime Dénès
2018-03-23update CHANGESEnrico Tassi
2018-03-19Fix typo in CHANGES.Théo Zimmermann
2018-03-15Add some missing entries in CHANGESMaxime Dénès
2018-03-09[doc] Document removal of deprecated options.Emilio Jesus Gallego Arias
2018-03-09Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...Maxime Dénès
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-09Merge PR #6923: Export optionsMaxime Dénès
2018-03-09Documentation for Cumulativity Weak Constraints.Gaëtan Gilbert
2018-03-09Merge PR #6480: Allow Prop as source for coercionsMaxime Dénès
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-09Documenting the Export modifier for options in CHANGES.Pierre-Marie Pédrot
2018-03-09doc and changes for coercion from prop/typecharguer
2018-03-09Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for fiat-cry...Maxime Dénès
2018-03-08Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Maxime Dénès
2018-03-08Merge PR #6743: Add notation {x & P} for sigTMaxime Dénès
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-07[vernac] Warn when using “Require” in a sectionVincent Laporte
2018-03-07Merge PR #6744: Add String.concatMaxime Dénès
2018-03-06Add CHANGES and man entry for coqdep learning _CoqProject.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 15:45:42 +0000