aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
AgeCommit message (Expand)Author
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-05[cleanup] remove useless EConstr qualificationsEnrico Tassi
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-02-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
2019-12-27fix: Shorten ssrsetoid.vErik Martin-Dorel
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-24fix «W -- weakening» docAntonio Nikishaev
2019-11-22Merge PR #11136: Adding `inj_compr` lemma in ssrfun.Enrico Tassi
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-18Adding `inj_compr` lemma in ssrfun.Cyril Cohen
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01[ssr] chore: Remove ssrclasses.{ml,mli} (now unneeded)Erik Martin-Dorel
2019-11-01[ssr] Refactor/Extend of under to support more relationsErik Martin-Dorel
2019-10-31[ssr] Refactor/Simplify the implementation of underErik Martin-Dorel
2019-10-22Add a notation for the empty type.Arthur Azevedo de Amorim
2019-10-21chore: Enclose the […get_reflexive_proof_ssr…] call in a try/with->assert...Erik Martin-Dorel
2019-10-13fix rev_right_loop docAntonio Nikishaev
2019-09-10feat: Add a rewrite rule (UnderE) to unprotect evars in subgoalsErik Martin-Dorel
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-09-02Merge PR #10719: Make SSR congr tactic work on arrows in Type.Enrico Tassi
2019-08-30Make SSR congr tactic work on arrows in Type.Andreas Lynge
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
2019-08-06[ssr] under: extend ssreflect.v to generalize iff to any setoid eqErik Martin-Dorel
2019-08-06[ssr] export Ssrequality.ssr_is_setoidErik Martin-Dorel
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-07-26Remove unused grammar productionsJim Fehrle
2019-07-23Do not rely on dummy TACTIC EXTEND for ssreflect tactics.Pierre-Marie Pédrot
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-06Merge PR #10305: Fix SSR (un)fold of polymorphic terms - issue 9336Enrico Tassi
2019-06-06Merge PR #10302: Fix SSR 'case B:b' with universe polymorphic equalityEnrico Tassi
2019-06-05Merge PR #10307: allow empty tactic_rules in ARGUMENT EXTENDPierre-Marie Pédrot
2019-06-05allow empty tactic_rules in ARGUMENT EXTENDDabrowski
2019-06-04Fix SSR (un)fold of polymorphic terms - issue 9336Andreas Lynge
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 09:30:14 +0000