aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-08Merge PR #6934: Warn when using “Require” in a sectionMaxime Dénès
2018-03-08Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Maxime Dénès
2018-03-07[stdlib] Do not use “Require” inside sectionsVincent Laporte
2018-03-07Merge PR #6932: [stdlib] Do not use deprecated notationsMaxime Dénès
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
2018-03-06Extraction: switch to EConstr.t as the central type to extract from.Pierre Letouzey
2018-03-06romega: get rid of EConstr.UnsafePierre Letouzey
2018-03-06[stdlib] Do not use deprecated notationsVincent Laporte
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-06Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Maxime Dénès
2018-03-06ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Enrico Tassi
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Maxime Dénès
2018-03-05Escape curly braces in ocamldoc commentmrmr1993
2018-03-05Separate vim/emacs fold markers from ocamldoc commentsmrmr1993
2018-03-05[ssreflect] Export parsing witnesses in mli file.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-05Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadMaxime Dénès
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
2018-03-04ssr: add Prenex Implicits for Some_inj to use it as a viewAnton Trunov
2018-03-04ssr: fix typo in doc commentAnton Trunov
2018-03-04ssr: ipats: V82.tactic ~nf_evars:false everywhereEnrico Tassi
2018-03-04ssr: rewrite Ssripats and Ssrview in the tactic monadEnrico Tassi
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Maxime Dénès
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
2018-03-04Pass the constant cache as a separate argument in kernel reduction.Pierre-Marie Pédrot
2018-03-04Remove all uses of Focus in standard library.Théo Zimmermann
2018-03-03[compat] Remove "Intuition Iff Unfolding"Emilio Jesus Gallego Arias
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-03-01Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Hugo Herbelin
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-28Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ...Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-21Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Maxime Dénès
2018-02-21Merge PR #6767: [ci] add elpiMaxime Dénès
2018-02-20proofview: goals come with a stateEnrico Tassi
2018-02-20Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).Hugo Herbelin
2018-02-20Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Hugo Herbelin
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-20Adding patterns in the category of binders for notations.Hugo Herbelin
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2018-02-19pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)Enrico Tassi
2018-02-19Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 15:48:09 +0000