coq/theories/Numbers/Rational/SpecViaQ, branch master The formal proof system BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) 2017-06-13T08:30:29+00:00 Pierre Letouzey 2017-03-22T10:24:27+00:00 295107103aaa86db8a31abb0e410123212648d45 See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude. 
 See now https://github.com/coq/bignums
 Int31 is still in the stdlib.
 Some proofs there has be adapted to avoid the need for BigNumPrelude.
Typeclasses: stdlib fixes for new search algorithm 2016-06-16T16:21:08+00:00 Matthieu Sozeau 2016-03-14T10:16:19+00:00 d4a421e57d74d305a797897f43ce216fb4c39719 






Update copyright headers.
2016-01-20T16:33:09+00:00

Maxime Dénès

2016-01-20T16:25:10+00:00

86f5c0cbfa64c5d0949365369529c5b607878ef8












Update headers.
2015-01-12T13:24:46+00:00

Maxime Dénès

2015-01-12T13:24:46+00:00

d90a5d4bfb05cd832b439044542a8c22ad5bd3ee












instanciation is French, instantiation is English
2014-08-25T13:22:40+00:00

Jason Gross

2014-08-12T15:03:05+00:00

876b1b39a0304c93c2511ca8dd34353413e91c9d












Updating headers.
2012-08-08T18:56:15+00:00

herbelin

2012-08-08T18:56:15+00:00

a234672e9d669397b40b59254c482f49007000df

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7







CompareSpec: a slight generalization/reformulation of CompSpec
2011-03-17T21:46:43+00:00

letouzey

2011-03-17T21:46:43+00:00

ce5a3cd114d3a570cdd569e65f1a2a71f81c39f4

 CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations
 eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y),
 (Plt=lt x y) (Pgt=lt y x), but this may not be always the case,
 especially for Pgt. The former CompSpec is now defined in term of
 CompareSpec. Compatibility is preserved (except maybe a rare unfold
 or red to break the CompSpec definition).

 Typically, CompareSpec looks nicer when we have infix notations, e.g.

  forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x)

 while CompSpec is shorter when we directly refer to predicates:

  forall x y, CompSpec eq lt x y (compare x y)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7





 CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations
 eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y),
 (Plt=lt x y) (Pgt=lt y x), but this may not be always the case,
 especially for Pgt. The former CompSpec is now defined in term of
 CompareSpec. Compatibility is preserved (except maybe a rare unfold
 or red to break the CompSpec definition).

 Typically, CompareSpec looks nicer when we have infix notations, e.g.

  forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x)

 while CompSpec is shorter when we directly refer to predicates:

  forall x y, CompSpec eq lt x y (compare x y)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7







- Add modulo_delta_types flag for unification to allow full
2011-03-13T14:41:09+00:00

msozeau

2011-03-13T14:41:09+00:00

c9931180560b7b343427811be0f14281bc791bda

conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes 
declared in sections.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7





conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes 
declared in sections.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7







First release of Vector library.
2010-12-10T13:22:29+00:00

pboutill

2010-12-10T13:22:29+00:00

05085e80668a4d1dedc522c6af343168870cc648

To avoid names&notations clashs with list, Vector shouldn't be
"Import"ed but one can "Import Vector.VectorNotations." to have
notations.

SetoidVector at least remains to do.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7





To avoid names&notations clashs with list, Vector shouldn't be
"Import"ed but one can "Import Vector.VectorNotations." to have
notations.

SetoidVector at least remains to do.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7







Updated all headers for 8.3 and trunk
2010-07-24T15:57:30+00:00

herbelin

2010-07-24T15:57:30+00:00

8d99bfcdc0915c006bffba6d5ffe14c683b9eb65

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7