aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/pptactic.ml
Commit message (Expand)AuthorAge
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
* Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
* Extending further PR#6047 (system to register printers for Ltac values).Gravatar Hugo Herbelin2017-11-24
* Printing again "intros **" as "intros" by default.Gravatar Hugo Herbelin2017-11-24
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
* Fixing printing of tactics encapsulated as tacarg with Tacexp.Gravatar Hugo Herbelin2017-11-15
* Using "l" printer for glob_constr, like for constr.Gravatar Hugo Herbelin2017-11-15
* Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\
| * [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* | Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Hugo Herbelin2017-11-04
|/
* Binding ltac printing functions to the system of generic printing.Gravatar Hugo Herbelin2017-11-02
* Setting a system to register printers for Ltac values.Gravatar Hugo Herbelin2017-11-02
* Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
* Exporting a few more printing functions.Gravatar Hugo Herbelin2017-11-02
* Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
* Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Gravatar Maxime Dénès2017-10-03
|\
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| * Properly display the "only" prefix for selectors (bug #5760).Gravatar Guillaume Melquiond2017-09-26
|/
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\
* \ Merge PR#722: [printing] Remove duplicated printing function.Gravatar Maxime Dénès2017-06-05
|\ \
| | * Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| |/ |/|
* | Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \
| | * [printing] Remove duplicated printing function.Gravatar Emilio Jesus Gallego Arias2017-06-01
| |/ |/|
| * Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
* | Adding "epose", "eset", "eremember" which allow to set terms withGravatar Hugo Herbelin2017-05-30
* | Adding "eassert", "eenough", "epose proof", which allow to stateGravatar Hugo Herbelin2017-05-30
|/
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
| * Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
* | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Use located in tactics.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
* [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 14:31:05 +0000