aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
AgeCommit message (Expand)Author
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-29A new step of restructuration of notations.Hugo Herbelin
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-13Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Pierre-Marie Pédrot
2017-06-16Removing Proof_type from the API.Pierre-Marie Pédrot
2017-06-16Remove the last use of the low-level Proof_type API in ssr.Pierre-Marie Pédrot
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
2017-06-13Dualize the unsafe flag of refine into typecheck and make it mandatory.Pierre-Marie Pédrot
2017-06-12Merge PR#718: API cleanup: aliasesMaxime Dénès
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-06Merge the ssr plugin.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:30:20 +0000