aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:03:39 +0000