| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-25 | Using `only printing` and fixing coercion in notations | Cyril Cohen | |
| 2020-11-23 | fixing [dup] for Coq 8.12 | Cyril Cohen | |
| 2020-11-11 | Intro pattern extensions for dup, swap and apply | Cyril Cohen | |
| 2020-10-07 | Turn class_of records into primitive records and get rid of the xclass idiom | Kazuhiko Sakaguchi | |
| 2020-09-14 | don't use all.v in output.v | Enrico Tassi | |
| 2020-09-11 | fix 8.9, 8.8 and 8.7 | Enrico Tassi | |
| 2020-09-10 | new attempt | Enrico Tassi | |
| 2020-09-09 | default reference file for < 8.12 | Enrico Tassi | |
| 2020-09-07 | [test suite] infrastructure to test how some statements are printed | Enrico Tassi | |
| 2020-06-13 | Add more test cases for higher-order recursive functions in seq.v w.r.t. the ↵ | Kazuhiko Sakaguchi | |
| guard condition | |||
| 2020-04-10 | adding guard conditions check to the test_suite | 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-04-30 | Reimplement the hierarchy related tools in OCaml | Kazuhiko Sakaguchi | |
| The functionalities of the structure hierarchy related tools `hierarchy-diagram` and `hierarchy_test.py` are provided by an OCaml script `hierarchy.ml`. `test_suite/hierarchy_test.v` is deleted. Now make can generate it. | |||
| 2019-04-08 | New test cases generation: corrent implementation of least common children | Kazuhiko Sakaguchi | |
| Add a new option `-raw-inheritances` to `hierarchy-diagram` to generate an intermediate file for `hierarchy_test.py`. So the typical usage is: $ python3.5 etc/utils/hierarchy_test.py \ <(etc/utils/hierarchy-diagram -raw-inheritances -R mathcomp mathcomp) \ > mathcomp/test_suite/hierarchy_test.v | |||
| 2019-04-04 | no output on success in test_suite/hierarchy_test.v (#323) | Cyril Cohen | |
| 2019-04-03 | rename test-suite -> test_suite to make coq happy | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |