coq/test-suite/ssr, branch master The formal proof system Fixing [dup] and [swap] 2020-11-24T16:03:31+00:00 Cyril Cohen 2020-11-23T16:55:27+00:00 5eb18289189a8a3d71086b12998e85d651970b28 






fixup
2020-11-07T23:22:53+00:00

Cyril Cohen

2020-11-07T23:22:53+00:00

7bd93b0d6000766d766da4a73dbe44e4189b2085












Intro pattern extensions for dup, swap and apply
2020-11-06T11:02:43+00:00

Cyril Cohen

2020-11-06T10:32:17+00:00

79c45ec7696923c9d2867b094ca30d6af142dbc8












[ssr] turn "nothing to inject" into a real warning (fix #12746)
2020-08-10T12:52:13+00:00

Enrico Tassi

2020-07-24T14:01:57+00:00

0aa3f871051c737192f9a19b79957b32b6ecafea












make the linter happy
2020-06-16T12:09:50+00:00

Enrico Tassi

2020-06-16T12:09:50+00:00

22ea81efe0111381be372d88821da8b2fa76be71












[ssr] fix env handling in error message (fix #12507)
2020-06-15T08:59:53+00:00

Enrico Tassi

2020-06-13T19:17:17+00:00

8cbb01a852c950f044c6f2c9a9ada2626d2bbfc5












Add tests uncovered during bug chasing in the CI.
2020-05-03T11:09:50+00:00

Pierre-Marie Pédrot

2020-05-02T16:58:39+00:00

4add482cfde2e3734be567c9824b2774871deb52












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.







fix: Shorten ssrsetoid.v
2019-12-26T23:30:26+00:00

Erik Martin-Dorel

2019-12-26T23:13:52+00:00

ec2d1bc0d0f0447f8824def545697b8c05fcb670

* This patch is a quick fix that removes part of the features of coq/coq#10022,
  namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged
  relation R. This just means we'll need to do an extra step [rewrite UnderE.]
  which was unnecessary with Coq 8.11+alpha.
* This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient
  feature of coq/coq#10022 (generalize under & over to any Reflexive relation).
* Related: coq-community/atbr#23





* This patch is a quick fix that removes part of the features of coq/coq#10022,
  namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged
  relation R. This just means we'll need to do an extra step [rewrite UnderE.]
  which was unnecessary with Coq 8.11+alpha.
* This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient
  feature of coq/coq#10022 (generalize under & over to any Reflexive relation).
* Related: coq-community/atbr#23







Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) relation
2019-11-01T17:20:50+00:00

Enrico Tassi

2019-11-01T17:20:50+00:00

1e0e9dc1d9afdec7b33b72178487ede494520e06

Reviewed-by: gares





Reviewed-by: gares