aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
|\ \
| * | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionGravatar Jasper Hugunin2018-01-17
* | | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
|/ /
| * Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
* | Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
|/
* Merge PR #6493: [API] remove large file containing duplicate interfacesGravatar Maxime Dénès2017-12-29
|\
| * [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
* | Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
|/
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 12:16:23 +0000