aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacmach.mli
Commit message (Expand)AuthorAge
* Remove up-to-conversion matching functions.Gravatar Pierre-Marie Pédrot2017-12-09
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\
* | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Moving "assert" (internally "Cut") to the new proof engine.Gravatar Hugo Herbelin2017-06-25
|/
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | Quote API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Eqdecide API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Use pf_get_type_of to avoid blowup in pose proof of large proof termsGravatar Matthieu Sozeau2016-11-08
| * Fix #3441 Use pf_get_type_of to avoid blowupGravatar Matthieu Sozeau2016-11-04
|/
* Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
* | Indexing Proofview.goals with a stage.Gravatar Pierre-Marie Pédrot2015-10-20
|/
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Removing useless flag of the historical move tactic.Gravatar Pierre-Marie Pédrot2014-11-22
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Removing the old rename tactic.Gravatar Pierre-Marie Pédrot2014-11-04
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Removing Convert_concl and Convert_hyp from Logic.Gravatar Hugo Herbelin2014-10-09
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 10:35:51 +0000