aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
Commit message (Expand)AuthorAge
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\
* \ Merge PR #6497: Add optimize_heap tactic for #6488Gravatar Maxime Dénès2018-01-08
|\ \
| | * Brackets support single numbered goal selectors.Gravatar Théo Zimmermann2018-01-05
| |/ |/|
| * add optimize_heap tactic for #6488Gravatar Paul Steckler2018-01-03
* | Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
* | Remove legacy Value.normalize function.Gravatar Maxime Dénès2017-12-22
|/
* Merge PR #6381: A version of [time] that works on constr evaluationGravatar Maxime Dénès2017-12-18
|\
* \ Merge PR #6406: Make [abstract] nodes show up in the Ltac profileGravatar Maxime Dénès2017-12-18
|\ \
* \ \ Merge PR #6380: Add tactics to reset and display the Ltac profileGravatar Maxime Dénès2017-12-18
|\ \ \
* \ \ \ Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingGravatar Maxime Dénès2017-12-18
|\ \ \ \
* \ \ \ \ Merge PR #6419: [vernac] Split `command.ml` into separate files.Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \
| * | | | | [flags] Make program_mode a parameter for commands in vernac.Gravatar Emilio Jesus Gallego Arias2017-12-17
| | | | * | Pass a ghost location for abstractGravatar Jason Gross2017-12-14
| | | | * | Make [abstract] nodes show up in the Ltac profileGravatar Jason Gross2017-12-14
| |_|_|/ / |/| | | |
| | | | * Add named timers to LtacProfGravatar Jason Gross2017-12-14
| | | |/
| | | * Add tactics to reset and display the Ltac profileGravatar Jason Gross2017-12-14
| |_|/ |/| |
* | | Merge PR #6386: Catch errors while coercing 'and' intro patternsGravatar Maxime Dénès2017-12-14
|\ \ \
* \ \ \ Merge PR #6379: Fix profiling pluginGravatar Maxime Dénès2017-12-14
|\ \ \ \
* \ \ \ \ Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \
| | | | | | * Fix #5081 by more fine-grained LtacProf recordingGravatar Jason Gross2017-12-12
| | | | | |/
| | | * | | Use msg_info for LtacProfGravatar Jason Gross2017-12-11
| | | * | | Allow LtacProf tactics to be calledGravatar Jason Gross2017-12-11
| | | | |/ | | | |/|
| | | | * Catch errors while coercing 'and' intro patternsGravatar Tej Chajed2017-12-11
| | | |/
* | | / [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |_|/ |/| |
| | * Remove deprecated appcontext and corresponding documentation.Gravatar Théo Zimmermann2017-12-11
| | * Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
| |/ |/|
| * [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* | [stm] Remove all but one use of VtUnknown.Gravatar Emilio Jesus Gallego Arias2017-12-09
|/
* Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\
* \ Merge PR #6210: More complete not-fully-applied error messages, #6145Gravatar Maxime Dénès2017-12-05
|\ \
| * | more complete not-fully-applied error messages, #6145Gravatar Paul Steckler2017-11-28
* | | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \
* | | | Use Evarutil.has_undefined_evars for tactic has_evar.Gravatar Gaëtan Gilbert2017-11-24
| * | | Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
| * | | When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| * | | Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
| * | | Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
|/ / /
| | * 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
| |/ |/|
* | Merge PR #6197: [plugin] Remove LocalityFixme über hack.Gravatar Maxime Dénès2017-11-24
|\ \
* \ \ Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Maxime Dénès2017-11-23
|\ \ \
| | * | [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
| |/ / |/| |
* | | [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* | | Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesGravatar Maxime Dénès2017-11-21
|\ \ \
| * | | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
| | * | Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Gaëtan Gilbert2017-11-19
| |/ / |/| |
| * | 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
| |/