| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-12 | Silencing warning deprecated-ident-entry | Cyril Cohen | |
| 2021-03-04 | Silence Hint Locality warning | Cyril Cohen | |
| 2020-11-19 | Removing duplicate clears and turning the warning into an error | Cyril Cohen | |
| 2020-11-19 | add declare scopes | Reynald Affeldt | |
| 2020-06-08 | silencing warnings in individual packages | Cyril Cohen | |
| 2020-04-06 | Rewriting with AC (not modulo AC), using a small scale command. | Cyril Cohen | |
| This replaces opA, opC, opAC, opCA, ... and any combinations of them - Right now the rewrite relies on an rather efficient computation of perm_eq using a "spaghetti sort" in O(n log n) - Wrongly formed AC statements send error messages showing the discrepancy between LHS and RHS patterns. Usage : rewrite [pattern](AC operator pattern-shape re-ordering) rewrite [pattern](ACl operator re-ordering) - pattern is optional, as usual, - operator must have a canonical Monoid.com_law structure (additions, multiplications, conjunction and disjunction do) - pattern-shape is expressed using the syntax p := n | p * p' where "*" is purely formal and n > 0 is number of left associated symbols examples of pattern shapes: + 4 represents (n * m * p * q) + (1*2) represents (n * (m * p)) - re-ordering is expressed using the syntax s := n | s * s' where "*" is purely formal and n is the position in the LHS If the ACl variant is used, the pattern-shape defaults to the pattern fully associated to the left i.e. n i.e (x * y * ...) Examples of re-orderings: - ACl op ((0*1)*2) is the identity (and should fail to rewrite) - opAC == ACl op ((0*2)*1) == AC op 3 ((0*2)*1) - opCA == AC op (2*1) (0*1*2) - rewrite opCA -opA == rewrite (ACl op (0*(2*1)) - opACA == AC (2*2) ((0*2)*(1*3)) | |||
| 2019-12-11 | Initial import of order.v into mathcomp | Cohen Cyril | |
| 2018-02-26 | Add ssrmatching.v transitional file | Erik Martin-Dorel | |
| The content of this file is similar to that of ssrfun.v and aims to increase compatibility with Coq 8.6+ for third-party libraries that depend on both math-comp and ssrmatching.v Close #63 | |||
| 2017-07-31 | Fix build of ssreflect/ only on 8.6 | Enrico Tassi | |
| 2017-06-14 | No .ml4 file in the standard Make | Enrico | |
| it is to the caller of coq_makefile to eventually add .ml4 files | |||
| 2017-06-14 | Fix compilation of ssreflect/ submodule | Matej Košík | |
| 2016-06-16 | Port build system to trunk (ssrmatching merged in Coq) | Enrico Tassi | |
| 2015-11-05 | merge basic/ into ssreflect/ | Enrico Tassi | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
| 2015-03-09 | some work on ssreflect and discrete | Enrico Tassi | |
| 2015-03-09 | Initial commit | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |