coq/test-suite/typeclasses, branch master The formal proof system Update headers in the whole code base. 2020-03-18T11:15:43+00:00 Théo Zimmermann 2020-03-18T11:14:26+00:00 a99776e10e0b2198d2b811ad82631111fb450f8a Add headers to a few files which were missing them. 
Add headers to a few files which were missing them.
Update ml-style headers to new year. 2019-06-17T16:08:32+00:00 Théo Zimmermann 2019-06-06T09:22:08+00:00 42e09b6d888a29cc6273b8e77d5f9a2e5582abc4 






Update headers following #6543.
2018-02-27T16:57:50+00:00

Théo Zimmermann

2018-02-27T16:02:31+00:00

629fbc743f8b5e7623a6834f19885b2e379cb782












Ensuring all .v files end with a newline to make "sed -i" work better on them.
2017-08-21T16:29:07+00:00

Hugo Herbelin

2017-08-21T16:29:07+00:00

9dea4814ae928192e23764c09473501e2ecc9937












Bump year in headers.
2017-07-04T12:20:57+00:00

Pierre-Marie Pédrot

2017-07-04T12:19:44+00:00

3e0334dd48b5d0b03046d0aff1a82867dc98d656












Adding a test for the behaviour of open_constr described in #3777.
2016-03-03T20:35:42+00:00

Pierre-Marie Pédrot

2016-03-03T20:35:42+00:00

7461aaedef508570fba6334e18fd10d5b32bda0e












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












Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
2014-09-15T19:37:31+00:00

Matthieu Sozeau

2014-09-15T19:33:48+00:00

62a552b508b747b6cdf4bd818233f001ae4ce555

of resulution for goals whose head is "ref". + means the argument
is an input and shouldn't contain an evar, otherwise resolution
fails. This generalizes the Typeclasses Strict Resolution option
which prevents resolution to fire on underconstrained typeclass
constraints, now the criterion can be applied to specific parameters.
Also cleanup auto/eauto code, uncovering a potential backwards
compatibility issue: in cases the goal contains existentials, we
never use the discrimination net in auto/eauto. We should try to
set this on once the contribs are stabilized (the stdlib goes through
when the dnet is used in these cases).





of resulution for goals whose head is "ref". + means the argument
is an input and shouldn't contain an evar, otherwise resolution
fails. This generalizes the Typeclasses Strict Resolution option
which prevents resolution to fire on underconstrained typeclass
constraints, now the criterion can be applied to specific parameters.
Also cleanup auto/eauto code, uncovering a potential backwards
compatibility issue: in cases the goal contains existentials, we
never use the discrimination net in auto/eauto. We should try to
set this on once the contribs are stabilized (the stdlib goes through
when the dnet is used in these cases).







Avoid backtracking in typeclass search if a solution for a closed
2014-09-15T10:16:52+00:00

Matthieu Sozeau

2014-09-15T10:12:41+00:00

e2c0cd1cb7fd06ef37f87f64e1164766820c16ea

non-dependent or propositional constraint has already been found
(same behavior as before previous patch).





non-dependent or propositional constraint has already been found
(same behavior as before previous patch).