aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
Commit message (Expand)AuthorAge
...
| * | Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
| * | Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
| |\ \
| * | | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat...Gravatar Hugo Herbelin2017-05-04
| | | * Generalizing the tactic-in-term embedding to any generic argument.Gravatar Pierre-Marie Pédrot2017-05-03
| | | * Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
| | |/ | |/|
| * | Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
| * | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| * | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| * | Add [_] prefix to unused values which maybe should be keptGravatar Gaetan Gilbert2017-04-27
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| * | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| * | Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
| | * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
* | | [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] Remove `Loc.internal_ghost`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
| |/ |/|
| * Removing various tactic compatibility layers in core tactics.Gravatar Pierre-Marie Pédrot2017-04-24
|/
* Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
* \ Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \
| * | [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | | Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \ | |/ / |/| |
| * | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| |\ \
* | | | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / |/| |
* | | Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \ \
| | * | Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
| | * | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| | |\ \ | |_|/ / |/| | |
* | | | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\ \ \ \
| | | * | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | | | | Declaring ltac plugin, so that static linking works.Gravatar Hugo Herbelin2017-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
| |_|/ / |/| | |
| * | | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
|/ / /
| * | Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| * | Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
|/ /
* | [pp] Move terminal-specific tagging to the toplevel.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] ltac/profile_ltacGravatar Emilio Jesus Gallego Arias2017-03-14
| |_|/ / |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 11:16:50 +0000