aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Extend `zify_N` with knowledge about `N.pred`Gravatar Joachim Breitner2018-02-14
* Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\
* \ Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\ \
* \ \ Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...Gravatar Maxime Dénès2018-02-05
|\ \ \
| | * | Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
| |/ / |/| |
| * | [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
* | | Delete duplicate lineGravatar Paul Steckler2018-01-30
|/ /
| * Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
|/
* Remove dead code from funind.Gravatar Maxime Dénès2018-01-24
* Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\
| * Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
* | 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
| | | | | | | | |/ / /