aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssreflect.v
AgeCommit message (Expand)Author
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
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-09-10feat: Add a rewrite rule (UnderE) to unprotect evars in subgoalsErik Martin-Dorel
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
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-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 2JPR
2019-04-30fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interfaceGeorges Gonthier
2019-04-23[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notationsErik Martin-Dorel
2019-04-23[ssr] under: Add iff support in side-conditionsErik Martin-Dorel
2019-04-23[ssr] under: Simplify the over tacticErik Martin-Dorel
2019-04-23[ssr] Remove the unify_helper tactic that appears unnecessaryErik Martin-Dorel
2019-04-23[ssr] under: Change the style of a few tests (over tactic vs. lemma)Erik Martin-Dorel
2019-04-23[ssr] under: Move {beta_expand, unify_helper} in the module type (qualify them)Erik Martin-Dorel
2019-04-23[ssr] under: Strenghten over & Add test_big_andbErik Martin-Dorel
2019-04-23[ssr] under: Extend the test-suite to exemplify most use casesErik Martin-Dorel
2019-04-23[ssr] over: also works on universally quantified goalsErik Martin-Dorel
2019-04-23[ssr] Define both a lemma "over" (in sig UNDER) and an ltac "over"Erik Martin-Dorel
2019-04-02[ssr] under: Add opaque modules for tagging and notation supportErik Martin-Dorel
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
2018-11-07[doc] nodes in ssr are monospaceEnrico Tassi
2018-11-07multi line comments don't have a titleEnrico Tassi
2018-11-07[doc] adapt comments in plugins/ssr/*.v to coqdoc styleEnrico Tassi
2018-10-24[ssreflect] Better use of CoqlibVincent Laporte
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-07-25Replace all the CoInductives with Variants in the SSR pluginKazuhiko Sakaguchi
2018-02-27Update headers following #6543.Théo Zimmermann
2017-06-06Merge the ssr plugin.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:06:35 +0000