aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprGravatar Maxime Dénès2018-01-16
|\
* \ Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \
| | * [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
* | | 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
* | Merge PR #6493: [API] remove large file containing duplicate interfacesGravatar Maxime Dénès2017-12-29
|\ \
| * | [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
* | | Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
|/ /
* | Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Gravatar Maxime Dénès2017-12-27
|\ \
* \ \ Merge PR #6494: Remove legacy Value.normalize function.Gravatar Maxime Dénès2017-12-27
|\ \ \ | |_|/ |/| |
| | * [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| |/ |/|
| * Remove legacy Value.normalize function.Gravatar Maxime Dénès2017-12-22
* | Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
|/
* Merge PR #6234: Make the micromega extraction check a regular output test.Gravatar Maxime Dénès2017-12-20
|\
* \ 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 #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Gravatar 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
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \ \ \ \
| | * | | | | | | [flags] Make program_mode a parameter for commands in vernac.Gravatar Emilio Jesus Gallego Arias2017-12-17
| | * | | | | | | [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-12-17
| |/ / / / / / /
* | | | | | | | Merge PR #6219: Document undocumented optionsGravatar Maxime Dénès2017-12-15
|\ \ \ \ \ \ \ \
| | * | | | | | | [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
| | | | | | * | | Pass a ghost location for abstractGravatar Jason Gross2017-12-14
| | | | | | * | | Make [abstract] nodes show up in the Ltac profileGravatar Jason Gross2017-12-14
| |_|_|_|_|/ / / |/| | | | | | |
| * | | | | | | Deprecate dead option Match Strict (ssr).Gravatar Gaëtan Gilbert2017-12-14
| * | | | | | | Deprecate dead code option Congruence Depth.Gravatar Gaëtan Gilbert2017-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 #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6379: Fix profiling pluginGravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Gravatar 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
| | | | | | | | |/ / /
| | | * | | | | | | | In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
| | | * | | | | | | | Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-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
| |/ / / / / / |/| | | | | |
* | | | | | | Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1150: [stm] Remove all but one use of VtUnknown.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6338: Remove up-to-conversion term matchingGravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / |/| | | | | | | |