coq-mathcomp/mathcomp/ssreflect/plugin/trunk, branch masterLibrary of mathematical components formalized in Coqremove ssr plugin for 8.4 and 8.52018-04-20T12:15:22+00:00Enrico Tassi2018-04-20T12:15:22+00:00e418a8b26b66ce88e22cff5978823e25aab03d94
For trunk, use merged ssr plugin.2017-06-07T09:15:26+00:00Maxime Dénès2017-05-03T07:32:34+00:0096a3c59b4586164e8aa80f53f0f9031fd1167ce8
Fix plugin after Sigma removal.2017-06-06T08:43:00+00:00Maxime Dénès2017-05-10T14:35:08+00:007e5f7949de0f1be496a7e6c3376f9858142f3e75
Merge pull request #127 from herbelin/trunk+interp_closed_glob_constr2017-06-06T07:09:24+00:00Maxime Dénès2017-06-06T07:09:24+00:00c8d04cb7e9fa6c6717ae8021d0ce86b9c134cbe6
Binding glob_constr to interp_glob_closure so as to factorize low-level code.
Binding glob_constr to interp_glob_closure so as to factorize low-level code.
Adapting to PR #590 (a more explicit algebraic type for evars of kind MatchingVar).2017-05-31T00:08:42+00:00Hugo Herbelin2017-05-12T17:33:52+00:0013458380eaef14078bb5805db3d8027bc76adeba
Binding glob_constr to interp_glob_closure so as to factorize low-level code.2017-05-30T22:46:01+00:00Hugo Herbelin2017-04-30T21:35:35+00:00679d8ba37c05a43b0480a4200bfb1347481a5d1a
[coqlib] Update to explicitly build terms from references.2017-05-25T13:25:46+00:00Emilio Jesus Gallego Arias2017-05-25T13:25:46+00:00039aa8b0e6c5eb9fd0622494efa57acfaae7749e
See coq/coq#678
See coq/coq#678
Merge pull request #125 from ejgallego/options+remove_non_sync2017-05-25T10:51:40+00:00Maxime Dénès2017-05-25T10:51:40+00:0020d1012d25093970ea72b928794cfdde27757e50
[options] Sync with upstream API changes.
[options] Sync with upstream API changes.
[options] Sync with upstream API changes.2017-05-23T15:27:02+00:00Emilio Jesus Gallego Arias2017-03-14T18:59:12+00:007625fdb52bf22ea4c332eafbc088675517b202d3
[ast] Adapt to Coq's #402 new generic AST node.2017-04-18T23:05:19+00:00Emilio Jesus Gallego Arias2017-04-18T23:05:19+00:003500ccbc0c5e06dfe3f053d1ee80185b1930b900