aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2018-04-01Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of tclTHEN...Pierre-Marie Pédrot
2018-03-29Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Pierre-Marie Pédrot
2018-03-27Adding tacticals tclBINDFIRST/tclBINDLAST.Hugo Herbelin
2018-03-23Deprecate undocumented "intros until 0" in favor of "intros *".Hugo Herbelin
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-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-08Add an invariant on given up goals in class_tactics.Hugo Herbelin
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
2018-03-08Proof engine: consider the pair principal and future goals as an entity.Hugo Herbelin
2018-03-08Merge PR #6893: Cleanup UState API usageMaxime Dénès
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 #6924: Clean-up remove always false useeager argument.Maxime Dénès
2018-03-08Merge PR #6902: [compat] Remove "Discriminate Introduction"Maxime Dénès
2018-03-08Merge PR #6903: [compat] Remove "Shrink Abstract"Maxime Dénès
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-06Clean-up remove always false useeager argument.Théo Zimmermann
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-06[compat] Remove "Discriminate Introduction"Emilio Jesus Gallego Arias
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-06Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Maxime Dénès
2018-03-05Tweak comments to fix ocamldoc errorsmrmr1993
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-05Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadMaxime Dénès
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04tactics: export e_reduct_in_conclEnrico Tassi
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Maxime Dénès
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
2018-03-03[compat] Remove "Injection L2R Pattern Order"Emilio Jesus Gallego Arias
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
2018-03-01Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Hugo Herbelin
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20proofview: goals come with a stateEnrico Tassi
2018-02-19Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Maxime Dénès
2018-02-17Implement name mangling optionJasper Hugunin
2018-02-16apply_type: add option "typecheck" passed down to refineEnrico Tassi
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-17Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 14:43:59 +0000