aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
Commit message (Expand)AuthorAge
* Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Gravatar Maxime Dénès2018-03-06
|\
* \ Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \
| | * [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: 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
|\ \ \ | |/ / |/| |
| * | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
* | | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-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
* 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
* Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\
* | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
|/
* Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\
| * Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* | [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
|/
* [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
* Merge PR #6219: Document undocumented optionsGravatar Maxime Dénès2017-12-15
|\
| * Deprecate dead option Match Strict (ssr).Gravatar Gaëtan Gilbert2017-12-14
* | Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...Gravatar Maxime Dénès2017-12-14
|\ \
* | | Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
* | | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| |/ |/|
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
* | Merge PR #6197: [plugin] Remove LocalityFixme über hack.Gravatar Maxime Dénès2017-11-24
|\ \
| * | [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
* | | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
|/ /
* | [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
| * ssr: fill_occ_pattern: return valid ustate even if no match (fix #6106)Gravatar Enrico Tassi2017-11-09
* | [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
|/
* Merge PR #6015: [general] Remove Econstr dependency from `intf`Gravatar Maxime Dénès2017-10-27
|\
* | Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| * [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
|/
* Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
* Removing Proof_type from the API.Gravatar Pierre-Marie Pédrot2017-06-16
* Remove the last use of the low-level Proof_type API in ssr.Gravatar Pierre-Marie Pédrot2017-06-16
* Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\
* \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \