aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
AgeCommit message (Expand)Author
2018-10-31[ssr] use tclDISPATCH for IPatDispatch (fix #8544)Enrico Tassi
2018-10-30Avoid passing dummy env to error printerMaxime Dénès
2018-10-30Remove one use of empty_env in ssrMaxime Dénès
2018-10-29Merge PR #8667: [RFC] Vendoring of Camlp5Pierre-Marie Pédrot
2018-10-29Merge PR #8812: [ssreflect] Better use of CoqlibEnrico Tassi
2018-10-29[gramlib] Wrap `Gramlib`.Emilio Jesus Gallego Arias
2018-10-26Cleanup evar_extra: remove evar_info's store and add maps to evar_mapMatthieu Sozeau
2018-10-24[ssreflect] Better use of CoqlibVincent Laporte
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-18[universes] deprecate constr_of_globalMatthieu Sozeau
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-27[ssr] [camlp5] Remove warning from camlp5Emilio Jesus Gallego Arias
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-09-19Merge PR #8246: Implementing an internal basic version of the "pose" tactic i...Enrico Tassi
2018-09-11Merge PR #8284: [ssr] anomaly -> errorMaxime Dénès
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-09-04[ssr] guard all `try pf_unify_HO` with CErrors.noncriticalEnrico Tassi
2018-09-03Merge PR #8147: [ssr] assertion -> error message (Fix #8134)Maxime Dénès
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-13Less crazy implementation of the "pose" family of tactics.Pierre-Marie Pédrot
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-25[ssr] assertion -> error message (Fix #8134)Enrico Tassi
2018-07-25Replace all the CoInductives with Variants in the SSR pluginKazuhiko Sakaguchi
2018-07-19Remove declare_object for SsrHave NoTCResolution.Maxime Dénès
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-06-30Split the Ssrmatching module between code and grammar rules.Pierre-Marie Pédrot
2018-06-25Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorMaxime Dénès
2018-06-23Merge PR #7236: [ssr] simpler semantics for delayed clearsMaxime Dénès
2018-06-22[ssr] implement {}/v as a short hand for {v}/v when v is an idEnrico Tassi
2018-06-22[ssr] simplify delayed clearsEnrico Tassi
2018-06-22[ssr] set: merge universe constraints before type checking the termEnrico Tassi
2018-06-20[ssr] rewrite: turn anomaly into regular errorEnrico Tassi
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-30Merge PR #7558: [api] Make `vernac/` self-contained.Maxime Dénès
2018-05-28Merge PR #7419: Remove 100 occurrences of Evd.emptyPierre-Marie Pédrot
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-25Merge PR #7524: [ssr] fix after to_constr ~abort_on_undefined_evars was addedMaxime Dénès
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-16[ssr] fix after to_constr ~abort_on_undefined_evars was addedEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 02:44:20 +0000