aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* 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
|/
* [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
|/
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/
| * Stopping injection not to work on discriminable atoms (see #4890).Gravatar Hugo Herbelin2017-05-17
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| * Fix the API of the new pf_constr_of_global.Gravatar Pierre-Marie Pédrot2017-04-24
| * Removing the tclNOTSAMEGOAL primitive from the API.Gravatar Pierre-Marie Pédrot2017-04-24
|/
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 12:59:41 +0000