coq - The formal proof system

Age	Commit message (Expand)	Author
2019-05-23	Fixing typos - Part 2	JPR
2019-04-30	fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interface	Georges Gonthier
2019-04-23	[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations	Erik Martin-Dorel
2019-04-23	[ssr] under: Add iff support in side-conditions	Erik Martin-Dorel
2019-04-23	[ssr] under: Simplify the over tactic	Erik Martin-Dorel
2019-04-23	[ssr] Remove the unify_helper tactic that appears unnecessary	Erik 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_andb	Erik Martin-Dorel
2019-04-23	[ssr] under: Extend the test-suite to exemplify most use cases	Erik Martin-Dorel
2019-04-23	[ssr] over: also works on universally quantified goals	Erik 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 support	Erik Martin-Dorel
2018-12-19	Put #[universes(template)] on all auto template spots in stdlib	Gaëtan Gilbert
2018-12-18	[ssr] extended intro patterns: + > [^] /ltac:	Enrico Tassi
2018-11-07	[doc] nodes in ssr are monospace	Enrico Tassi
2018-11-07	multi line comments don't have a title	Enrico Tassi
2018-11-07	[doc] adapt comments in plugins/ssr/*.v to coqdoc style	Enrico Tassi
2018-10-24	[ssreflect] Better use of Coqlib	Vincent Laporte
2018-09-10	Adapting standard library to the introduction of "Declare Scope".	Hugo Herbelin
2018-07-25	Replace all the CoInductives with Variants in the SSR plugin	Kazuhiko Sakaguchi
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-06-06	Merge the ssr plugin.	Maxime Dénès