aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\
* \ Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Gravatar Maxime Dénès2018-03-04
|\ \
* \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \
| | * | Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Gravatar Hugo Herbelin2018-03-01
| |/ / |/| |
| | * [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ |/|
* | Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ...Gravatar Maxime Dénès2018-02-28
|\ \
* | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \ \
* \ \ \ Merge PR #6767: [ci] add elpiGravatar Maxime Dénès2018-02-21
|\ \ \ \
| | | | * proofview: goals come with a stateGravatar Enrico Tassi2018-02-20
| | | * | Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).Gravatar Hugo Herbelin2018-02-20
| | | |/
* | | | Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
* | | | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* | | | Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
* | | | Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
| |_|/ |/| |
| * | pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)Gravatar Enrico Tassi2018-02-19
|/ /
* | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\ \
* \ \ Merge PR #6648: [tactics] make apply_type safeGravatar Maxime Dénès2018-02-19
|\ \ \
* \ \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...Gravatar Maxime Dénès2018-02-19
|\ \ \ \
* \ \ \ \ Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \
| | * | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | * | | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| |_|/ / / |/| | | |
| | | | * Extend `zify_N` with knowledge about `N.pred`Gravatar Joachim Breitner2018-02-14
| |_|_|/ |/| | |
| | | * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
| |_|/ |/| |
* | | 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
|\ \ \ \ | |_|/ / |/| | |
| | | * Remove dir-locals and ship suggested helper hooks instead.Gravatar Gaëtan Gilbert2018-01-06
| |_|/ |/| |
| | * 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
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 13:04:41 +0000