aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-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
* [api] Misctypes removal: multi to tactics/rewriteGravatar Emilio Jesus Gallego Arias2018-06-12
* Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Gravatar Matthieu Sozeau2018-06-04
|\
* | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* | Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
* | Deprecate most evarutil evdref functionsGravatar Gaëtan Gilbert2018-05-11
* | Merge PR #7215: Deprecate the "simple subst" tactic.Gravatar Hugo Herbelin2018-04-16
|\ \
* | | Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
| * | Deprecate the "simple subst" tactic.Gravatar Pierre-Marie Pédrot2018-04-10
|/ /
| * Replace uses of Termops.dependent by more specific functions.Gravatar Pierre-Marie Pédrot2018-04-10
|/
* [compat] Remove "Discriminate Introduction"Gravatar Emilio Jesus Gallego Arias2018-03-06
* Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Gravatar Maxime Dénès2018-03-06
|\
* \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \
* \ \ Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \
| | | * [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
|/ /
| * 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
* [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
* [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
* In injection/inversion, consider all template-polymorphic types as injectable.Gravatar Hugo Herbelin2017-11-28
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
* Delay use of flag "Discriminate Introduction" from interp to execution time.Gravatar Hugo Herbelin2017-10-26
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Fix BZ#5697: Congruence does not work with primitive projections.Gravatar Pierre-Marie Pédrot2017-08-29
* better `try with` scope in `discr_positions`Gravatar amblaf2017-07-31
* Correcting [build_discriminator] to make the test-suite passGravatar amblaf2017-07-31
* Remove references to Global.env in tactics/*.mlGravatar amblaf2017-07-31
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Deprecate options that were introduced for compatibility with 8.4.Gravatar Guillaume Melquiond2017-06-14
* Deprecate options that were introduced for compatibility with 8.2.Gravatar Guillaume Melquiond2017-06-14
* Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
* Remove support for Coq 8.3.Gravatar Guillaume Melquiond2017-06-14
* Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* tactics cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
* Equality cleanup: remove constr_of_globalGravatar Matthieu Sozeau2017-05-29
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
| * [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 21:06:13 +0000