aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/pptactic.ml
Commit message (Expand)AuthorAge
* Pptactic: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Remove Misctypes.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
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
* Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
* [ssreflect] Fix module scoping problems due to packing and mli files.Gravatar Emilio Jesus Gallego Arias2018-03-10
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* 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
* 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
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 14:02:46 +0000