aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
Commit message (Expand)AuthorAge
* [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
|\ \
| | * Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
* | | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| |/ |/|
* | Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\ \
* | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| * | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|/ /
| * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/
* Put "ssreflect" behind "API".Gravatar Matej Košík2017-06-07
* Merge the ssr plugin.Gravatar Maxime Dénès2017-06-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 19:42:06 +0000