aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-04-02
* Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of tclTHEN...Gravatar Pierre-Marie Pédrot2018-04-01
|\
* | Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Gravatar Pierre-Marie Pédrot2018-03-29
| * Adding tacticals tclBINDFIRST/tclBINDLAST.Gravatar Hugo Herbelin2018-03-27
|/
* Deprecate undocumented "intros until 0" in favor of "intros *".Gravatar Hugo Herbelin2018-03-23
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* Add an invariant on given up goals in class_tactics.Gravatar Hugo Herbelin2018-03-08
* Proof engine: support for nesting tactic-in-term within other tactics.Gravatar Hugo Herbelin2018-03-08
* Proof engine: consider the pair principal and future goals as an entity.Gravatar Hugo Herbelin2018-03-08
* Merge PR #6893: Cleanup UState API usageGravatar Maxime Dénès2018-03-08
|\
* \ Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Gravatar Maxime Dénès2018-03-08
|\ \
* \ \ Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \
* \ \ \ Merge PR #6924: Clean-up remove always false useeager argument.Gravatar Maxime Dénès2018-03-08
|\ \ \ \
* \ \ \ \ Merge PR #6902: [compat] Remove "Discriminate Introduction"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6903: [compat] Remove "Shrink Abstract"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6905: Fix make ml-docGravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \
| | | | * | | | Clean-up remove always false useeager argument.Gravatar Théo Zimmermann2018-03-06
| |_|_|/ / / / |/| | | | | |
| | | | | | * Rename some universe minimizing "normalize" functions to "minimize"Gravatar Gaëtan Gilbert2018-03-06
| | | | | | * Deprecate UState aliases in Evd.Gravatar Gaëtan Gilbert2018-03-06
| |_|_|_|_|/ |/| | | | |
| | | * | | [compat] Remove "Discriminate Introduction"Gravatar Emilio Jesus Gallego Arias2018-03-06
| |_|/ / / |/| | | |
| | * | | [compat] Remove "Shrink Abstract"Gravatar Emilio Jesus Gallego Arias2018-03-06
| |/ / / |/| | |
* | | | Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \ \ \
* \ \ \ \ Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \
| | | * | | Tweak comments to fix ocamldoc errorsGravatar mrmr19932018-03-05
| |_|/ / / |/| | | |
* | | | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadGravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \
| | | | * | | Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| |_|_|/ / / |/| | | | |
| * | | | | tactics: export e_reduct_in_conclGravatar Enrico Tassi2018-03-04
* | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ | |/ / / / / |/| | | | |
* | | | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \
| | | | | | | | * [compat] Remove "Standard Proposition Elimination"Gravatar Emilio Jesus Gallego Arias2018-03-03
| | | | | | * | | [compat] Remove "Injection L2R Pattern Order"Gravatar Emilio Jesus Gallego Arias2018-03-03
| | | | | | | |/ | | | | | | |/|
| | | | * | / | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | | | | |/ / | | | | |/| |
* | | | / | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| |_|_|/ / / |/| | | | |
| | * | | | Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Gravatar Hugo Herbelin2018-03-01
| |/ / / / |/| | | |
| | * | | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / / |/| | |
| | * | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ / |/| |
* | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| * | proofview: goals come with a stateGravatar Enrico Tassi2018-02-20
|/ /
* | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\ \
| | * Implement name mangling optionGravatar Jasper Hugunin2018-02-17
* | | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| |/ |/|
| * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
|/
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\
* \ Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \