aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
Commit message (Collapse)AuthorAge
...
* | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ | | | | | | | | | | | | | In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTENDGravatar Pierre Letouzey2016-06-27
| | | | | | | | | The warnings were: Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND cpattern]. Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND cpattern]. Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND lcpattern]. Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND lcpattern].
* ssrmatching: giving proper credits to the original author(s)Gravatar Enrico Tassi2016-06-15
| | | | | Following CeCILL-B 5.3.2, we are allowed to redistribute the software under the same license of Coq as long as we credit.
* ssrmatching: ltac argument parsing made more robustGravatar Enrico Tassi2016-06-15
|
* ssrmatching: debug prints sent via msg_debugGravatar Enrico Tassi2016-06-15
|
* Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"Gravatar Enrico Tassi2016-06-15
| | | | for uniformity with other Debug options.
* port ssrmatching plugin to the new makefileGravatar Enrico Tassi2016-06-14
|
* Ssreflect pattern matching facilitiesGravatar Enrico Tassi2016-03-02