coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove fourier plugin	Maxime Dénès	2018-07-17
\| \| \| \|	As stated in the manual, the fourier tactic is subsumed by lra.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Simplify some proofs.	Guillaume Melquiond	2017-04-02
\| \| \| \| \| \| \| \|	This commit does not modify the signature of the involved modules, only the opaque proof terms. One has to wonder how proofs can bitrot so much that several occurrences of "replace 4 with 4" start appearing.
*	Make IZR a morphism for field.	Guillaume Melquiond	2017-03-22
\| \| \| \| \| \|	There are now two field structures for R: one in RealField and one in RIneq. The first one is used to prove that IZR is a morphism which is needed to define the second one.
*	Change the parser and printer so that they use IZR for real constants.	Guillaume Melquiond	2017-03-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There are two main issues. First, (-cst)%R is no longer syntactically equal to (-(cst))%R (though they are still convertible). This breaks some rewriting rules. Second, the ring/field_simplify tactics did not know how to refold real constants. This defect is no longer hidden by the pretty-printer, which makes these tactics almost unusable on goals containing large constants. This commit also modifies the ring/field tactics so that real constant reification is now constant time rather than linear. Note that there is now a bit of code duplication between z_syntax and r_syntax. This should be fixed once plugin interdependencies are supported. Ideally the r_syntax plugin should just disappear by declaring IZR as a coercion. Unfortunately the coercion mechanism is not powerful enough yet, be it for parsing (need the ability for a scope to delegate constant parsing to another scope) or printing (too many visible coercions left).
*	Make IZR use a compact representation of integers.	Guillaume Melquiond	2017-03-22
\| \| \| \| \| \| \| \| \|	That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means that, after reduction, real constants no longer exponentially blow up. Note that I was not able to fix the test-suite for the declarative mode, so the missing proof terms have been admitted.
*	Simplify some proofs using ring and field.	Guillaume Melquiond	2017-03-22
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
\| \| \| \| \|	induction/elim over a dependent elimination principle for Prop arguments.
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
\| \| \| \| \| \| \| \| \|	in Prop of constructors of inductive types independent of these names. Incidentally upgraded/simplified a couple of proofs, mainly in Reals. This prepares to the next commit about using names based on H for such hypotheses in Prop.
*	Remove some uses of excluded middle.	Guillaume Melquiond	2014-04-22
\|
*	Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.	Guillaume Melquiond	2013-12-03
\|
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some cleanup in recent proofs concerning pi	letouzey	2012-07-05
\| \| \| \| \| \| \| \|	Initial idea was to just avoid compat notations such as Z_of_nat --> Z.of_nat, but I ended trying to improve a few proofs... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15520 85f007b7-540e-0410-9357-904b9bb8a0f7
*	These files are displaced from Rtrigo.v and Ranalysis_reg.v	bertot	2012-06-11
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15430 85f007b7-540e-0410-9357-904b9bb8a0f7