aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\
* \ Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Gravatar Maxime Dénès2018-03-06
|\ \
* \ \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \
* \ \ \ Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadGravatar Maxime Dénès2018-03-05
|\ \ \ \
| | | | * [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| |_|_|/ |/| | |
| * | | ssr: ipats: V82.tactic ~nf_evars:false everywhereGravatar Enrico Tassi2018-03-04
| * | | ssr: rewrite Ssripats and Ssrview in the tactic monadGravatar Enrico Tassi2018-03-04
* | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ | |/ / / |/| | |
* | | | 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
|\ \ \ \ \ \
| | | | | | * [compat] Remove "Intuition Iff Unfolding"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|_|_|/ |/| | | | |
| | | | * | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
| |_|_|/ / |/| | | |
| | * | | 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
|\ \ \
| | | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |_|/ |/| |
* | | [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
| |_|/ |/| |