coq-mathcomp/mathcomp/discrete, branch masterLibrary of mathematical components formalized in CoqUpdating files + reorganizing everything2015-07-17T16:03:31+00:00Cyril Cohen2015-07-17T16:03:31+00:00532de9b68384a114c6534a0736ed024c900447f9
Using the From X Require Y for v8.42015-04-09T11:53:46+00:00Cyril Cohen2015-04-09T11:53:46+00:00634ee874ec11a5a90617ca5723228d4de1fe479c
Makefile, testing for v8.5 and uncommenting stuff2015-04-03T15:45:38+00:00Cyril Cohen2015-04-03T15:45:38+00:00abe2354abf63ad98dbe7e54a34e59e20b38d3d55
This is a temporary solution, but there is a better one :
one could patch ssreflect.ml4 plugin for v8.4 to interpret
From ... Require Import ... as a simple Require Import.
This is a temporary solution, but there is a better one :
one could patch ssreflect.ml4 plugin for v8.4 to interpret
From ... Require Import ... as a simple Require Import.
prepared discrete for compilation in v8.52015-04-03T15:22:31+00:00Cyril Cohen2015-04-03T15:22:31+00:009fa572c64085bc020edee574a694fe0805fefdfa
some work on ssreflect and discrete2015-03-09T15:21:23+00:00Enrico Tassi2015-03-09T12:35:08+00:00155e671f7b83293ae327ddbd252d1d1ac961ab9a