aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
AgeCommit message (Expand)Author
2018-05-14Deprecate Refiner [evar_map ref] exported functions.Gaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-16Merge PR #7237: [ssr] fix delayed clears (fix #7045)Maxime Dénès
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-13Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...Pierre-Marie Pédrot
2018-04-13[ssr] fix delayed clears (fix #7045)Enrico Tassi
2018-04-04ssr: check cleared hyps do exist (fix #7050)Enrico Tassi
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-21Fix #7026: ssr: applying an overloaded lemma as a view takes too long.Pierre-Marie Pédrot
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-08Merge PR #6893: Cleanup UState API usageMaxime Dénès
2018-03-08Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Maxime 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-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-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-02Turn warning for deprecated notations on.Théo Zimmermann
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
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-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-19Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Maxime Dénès
2018-02-16apply_type: add option "typecheck" passed down to refineEnrico Tassi
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2018-02-07Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingMaxime Dénès
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2018-01-08[vernac] vernac_expr no longer recursiveVincent Laporte
2017-12-15Merge PR #6219: Document undocumented optionsMaxime Dénès
2017-12-14Deprecate dead option Match Strict (ssr).Gaëtan Gilbert
2017-12-14Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...Maxime Dénès
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 04:14:05 +0000