aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
* Merge PR #7789: Fixes #7779: destruct's "in" clause was forgetting the possib...Gravatar Pierre-Marie Pédrot2018-06-13
|\
| * Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Gravatar Hugo Herbelin2018-06-12
* | [api] Misctypes removal: tactic flags.Gravatar Emilio Jesus Gallego Arias2018-06-12
* | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
|/
* Merge PR #7004: Make `simple apply` obey `Opaque` directive.Gravatar Pierre-Marie Pédrot2018-06-05
|\
| * Make direct invocations of `simple apply` obey `Opaque` directive.Gravatar Maxime Dénès2018-06-05
* | Stronger invariants in unification signature.Gravatar Pierre-Marie Pédrot2018-06-04
|/
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* Tactics.introduction: remove dangerous option ~checkGravatar Enrico Tassi2018-05-28
* [tactics] Remove anonymous fix/cofix form.Gravatar Emilio Jesus Gallego Arias2018-05-24
* Deprecate Typing.e_* functionsGravatar Gaëtan Gilbert2018-05-14
* Deprecate Evarconv.e_conv,e_cumulGravatar Gaëtan Gilbert2018-05-11
* Convert clear_hyps_in_evi to state passing style.Gravatar Gaëtan Gilbert2018-05-11
* Deprecate most evarutil evdref functionsGravatar Gaëtan Gilbert2018-05-11
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Make "intro"/"intros" progress on existential variables.Gravatar Hugo Herbelin2018-05-02
* Merge PR #6935: Separate universe minimization and evar normalization functionsGravatar Pierre-Marie Pédrot2018-04-30
|\
* | Improving error message for clear tactic (and indirect uses of it).Gravatar Hugo Herbelin2018-04-24
| * Deprecate mixing univ minimization and evm normalization functions.Gravatar Gaëtan Gilbert2018-04-17
|/
* Merge PR #7200: [ltac] Deprecate nameless fix/cofix.Gravatar Maxime Dénès2018-04-16
|\
* | Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
| * [ltac] Deprecate nameless fix/cofix.Gravatar Emilio Jesus Gallego Arias2018-04-13
|/
* [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-04-02
* Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Gravatar Pierre-Marie Pédrot2018-03-29
* Deprecate undocumented "intros until 0" in favor of "intros *".Gravatar Hugo Herbelin2018-03-23
* [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
* 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
|\ \
* | | [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 #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
|\ \ \ \ \
| | | | | * [compat] Remove "Standard Proposition Elimination"Gravatar Emilio Jesus Gallego Arias2018-03-03
| | * | | | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | | |_|/ | | |/| |
* | / | | 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
* | 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
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23