aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching/ssrmatching.ml4
Commit message (Collapse)AuthorAge
...
| * | | ssrmatching: fix interpretation of rpatternGravatar Enrico Tassi2016-10-24
| | | |
| | | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | |/ | |/| | | | | | | | | | reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
| | * [pp] Use more convenient pp API in ssrmatchingGravatar Emilio Jesus Gallego Arias2016-10-18
| | |
| | * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |/ | | | | | | | | | | | | | | The current tag system in `Pp` is generic, which implies we must choose a tagging function when calling a printer. For console printing there is a single choice, thus this commits adds it a few missing cases.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
* | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| | | | | | | | | | | | There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
| * Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
| | | | | | | | One of them revealed a true bug.
* | Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-15
| |
* | Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
| |
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | Suggested by @ppedrot
* | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 03:01:29 +0000