aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2018-04-23Merge PR #7244: Making tactic-in-term aware of "Set Ltac Debug"Pierre-Marie Pédrot
2018-04-16Merge PR #7125: Adding ML headers in setoid_ringMaxime Dénès
2018-04-16Merge PR #7237: [ssr] fix delayed clears (fix #7045)Maxime Dénès
2018-04-13Making tactic-in-term aware of "Set Ltac Debug".Hugo Herbelin
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-13Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...Pierre-Marie Pédrot
2018-04-13[ssr] fix delayed clears (fix #7045)Enrico Tassi
2018-04-12Merge PR #7202: Correction of ugly message described in #4667Pierre Courtieu
2018-04-12Merge PR #7087: Congruence tactic engine updatePierre-Marie Pédrot
2018-04-12Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac failu...Pierre-Marie Pédrot
2018-04-11Correction of ugly message described in #4667Julien Forest
2018-04-09change error message in #5147Julien Forest
2018-04-09removing uggly error message of #5147Julien Forest
2018-04-09Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Maxime Dénès
2018-04-06Merge PR #6960: [api] Move some types to their proper module.Pierre-Marie Pédrot
2018-04-05Merge PR #7016: Make parsing independent of the cumulativity flag.Enrico Tassi
2018-04-04Fixing #7100 (lost of main file location in case of Ltac failure in other file).Hugo Herbelin
2018-04-04ssr: check cleared hyps do exist (fix #7050)Enrico Tassi
2018-04-02Fix #6404 - Print tactics called by ML tacticsJason Gross
2018-04-02[api] Move some types to their proper module.Emilio Jesus Gallego Arias
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-30Adding some headers, by consistency of style.Hugo Herbelin
2018-03-27Congruence: Fixing a bug with native projections.Hugo Herbelin
2018-03-27Congruence: typography in a comment.Hugo Herbelin
2018-03-27Congruence: getting rid of a detour by the compatibility layer of proof engine.Hugo Herbelin
2018-03-23Deprecate undocumented "intros until 0" in favor of "intros *".Hugo Herbelin
2018-03-23Merge PR #7028: Fix #7026: ssr: applying an overloaded lemma as a view takes ...Enrico Tassi
2018-03-21Make parsing independent of the cumulativity flag.Gaëtan Gilbert
2018-03-21Fix #7026: ssr: applying an overloaded lemma as a view takes too long.Pierre-Marie Pédrot
2018-03-20[ssreflect] Respect Opaque in FO unificationMaxime Dénès
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Merge PR #6769: Split closure cache and remove whd_bothMaxime Dénès
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-09Merge PR #6496: Generate typed generic code from ltac macrosMaxime Dénès
2018-03-08Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Maxime Dénès
2018-03-08Merge PR #6893: Cleanup UState API usageMaxime Dénès
2018-03-08Make most of TACTIC EXTEND macros runtime calls.Maxime Dénès
2018-03-08Merge PR #6918: romega: get rid of EConstr.UnsafeMaxime Dénès
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-08Merge PR #6934: Warn when using “Require” in a sectionMaxime Dénès
2018-03-08Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Maxime Dénès
2018-03-07[stdlib] Do not use “Require” inside sectionsVincent Laporte
2018-03-07Merge PR #6932: [stdlib] Do not use deprecated notationsMaxime Dénès
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:01:03 +0000