aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\
| * Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Gravatar Maxime Dénès2017-03-23
| * Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\
| | * Merge PR#495: funind: Ignore missing info for current functionGravatar Maxime Dénès2017-03-23
| | |\
| | * | Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
| * | | Mark ring morphisms as opaque.Gravatar Guillaume Melquiond2017-03-22
| * | | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
| * | | Fix broken evaluation strategies for ring and field.Gravatar Guillaume Melquiond2017-03-22
| * | | Remove duplicate lemmas.Gravatar Guillaume Melquiond2017-03-22
| | | * funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
| | |/
| * | [extraction] Flush formatters at end of output.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * | [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * | [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * | [pp] Force well-formed boxes by construction.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * | [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * | [pp] Remove `Pp.stras`.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * | [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
| * | [pp] Remove unused printing tagging infrastructure.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * | Merge PR#134: Enable `-safe-string`Gravatar Maxime Dénès2017-03-21
| |\ \
| * \ \ Merge PR#428: Report missing tactic arguments in error messageGravatar Maxime Dénès2017-03-17
| |\ \ \
| * \ \ \ Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-03-17
| |\ \ \ \
| * | | | | Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
| | | | * | [safe-string] plugins/extractionGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | * | [safe-string] ltac/profile_ltacGravatar Emilio Jesus Gallego Arias2017-03-14
| | |_|/ / | |/| | |
| | | * | Report missing tactic arguments in error messageGravatar Tej Chajed2017-03-14
| | |/ / | |/| |
| * | | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
| |\ \ \
| * | | | Micromega: removing a constant preventing micromega to be loaded before Logic.v.Gravatar Hugo Herbelin2017-03-09
| | | | * [ltac] Move dummy plugin to plugins folder.Gravatar Emilio Jesus Gallego Arias2017-03-03
| * | | | Merge PR#395: Allow hintdb to be parameters in a Ltac definition orGravatar Maxime Dénès2017-02-27
| |\ \ \ \
| | | | * | TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-02-24
| | |_|/ / | |/| | |
| * | | | Revert "Add empty ltac_plugin file for forward compatibility."Gravatar Maxime Dénès2017-02-24
| * | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
| |\ \ \ \ | | | |_|/ | | |/| |
| * | | | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| * | | | Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | * [cleanup] Change Id.t option to Name.t in TacFunGravatar Tej Chajed2017-02-16
| | |_|/ | |/| |
* | | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\| | |
* | | | Porting the ssrmatching plugin to the new EConstr API.Gravatar Enrico Tassi2017-02-14
* | | | Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Fix a mishandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
* | | | Omega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Micromega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 16:29:03 +0000