aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\
* \ Merge PR #6934: Warn when using “Require” in a sectionGravatar Maxime Dénès2018-03-08
|\ \
* \ \ Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Maxime Dénès2018-03-08
|\ \ \
| | * | [stdlib] Do not use “Require” inside sectionsGravatar Vincent Laporte2018-03-07
| |/ / |/| |
* | | Merge PR #6932: [stdlib] Do not use deprecated notationsGravatar Maxime Dénès2018-03-07
|\ \ \
* \ \ \ Merge PR #6905: Fix make ml-docGravatar Maxime Dénès2018-03-07
|\ \ \ \
* \ \ \ \ Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \
| | | * | | [stdlib] Do not use deprecated notationsGravatar Vincent Laporte2018-03-06
| |_|/ / / |/| | | |
* | | | | Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \
| | | | * | ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Enrico Tassi2018-03-06
* | | | | | 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
|\ \ \ \ \ \ \ | |_|_|_|_|/ / |/| | | | | |
| | | | | * | Escape curly braces in ocamldoc commentGravatar mrmr19932018-03-05
| | | | | * | Separate vim/emacs fold markers from ocamldoc commentsGravatar mrmr19932018-03-05
| |_|_|_|/ / |/| | | | |
| | | * | | [ssreflect] Export parsing witnesses in mli file.Gravatar Emilio Jesus Gallego Arias2018-03-05
| |_|/ / / |/| | | |
* | | | | 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: add Prenex Implicits for Some_inj to use it as a viewGravatar Anton Trunov2018-03-04
| | | | * | ssr: fix typo in doc commentGravatar Anton Trunov2018-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
|\ \ \ \ \ \ \
| | | | | | | * Remove all uses of Focus in standard library.Gravatar Théo Zimmermann2018-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
| |_|_|/ |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 08:42:10 +0000