aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Removing dead unsafe debugging code in Constrintern.Gravatar Pierre-Marie Pédrot2016-08-16
* Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
* Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
* Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
* Notations with multiple recursive binders: fixing use of alpha-conversion.Gravatar Hugo Herbelin2016-07-19
* Notations: fixing multiple binders used as terms in reverse order.Gravatar Hugo Herbelin2016-07-19
* Removing a source of clash with multiple recursive patterns in notations.Gravatar Hugo Herbelin2016-07-19
* A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
* Partial fix to #4592 (notation requiring alpha-conversion for printing).Gravatar Hugo Herbelin2016-07-17
* Fixing a bug in recognizing a recursive pattern of notationsGravatar Hugo Herbelin2016-07-17
* Fixing interpretation of notations w/ opposite instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17
* Fixing printing of notations with several instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17
* First step in adding printing for notations such as given in #4932.Gravatar Hugo Herbelin2016-07-17
* Fixing #4932 (anomaly when using binders as terms in recursive notations).Gravatar Hugo Herbelin2016-07-17
* Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-07-16
* removing ocamldoc-related syntax errorsGravatar Matej Kosik2016-07-12
* Merge remote-tracking branch 'github/bug4653' into v8.6Gravatar Matthieu Sozeau2016-07-07
|\
| * Do not use implicit type info for (x := t) bindingsGravatar Matthieu Sozeau2016-07-07
* | Program: fix #4873: transparency option not usedGravatar Matthieu Sozeau2016-07-07
| * Univs: fix internalization of (x := T) and castsGravatar Matthieu Sozeau2016-07-06
|/
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Fixing #4865 (deciding on which arguments to recompute scopes was not robust).Gravatar Hugo Herbelin2016-06-29
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Properly handling the only printing flag when parsing rules already exist.Gravatar Pierre-Marie Pédrot2016-06-28
| * Univs: allowing notations to take univ instancesGravatar Matthieu Sozeau2016-06-27
| * Forbidding silently dropped universes instances inGravatar Matthieu Sozeau2016-06-27
* | Merge remote-tracking branch 'github/pr/223' into feedback-locationsGravatar Maxime Dénès2016-06-27
|\ \
* | | minor: comment on the meaning of the 'boolean' variableGravatar Gabriel Scherer2016-06-27
* | | minor: documentation comment for constrintern.ml:sort_fieldsGravatar Gabriel Scherer2016-06-27
* | | minor: interp/constrintern.ml, clarify field completionGravatar Gabriel Scherer2016-06-27
* | | minor: in constrintern.ml:sort_fields, clarify sfGravatar Gabriel Scherer2016-06-27
* | | minor: in constrintern.ml:sort_fields, clarify build_pattGravatar Gabriel Scherer2016-06-27
* | | whitespace: untabity constrinternl.ml:sort_fieldsGravatar Gabriel Scherer2016-06-27
* | | minor clarifications in constrintern.ml:sort_fieldsGravatar Gabriel Scherer2016-06-27
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| * | [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
|/ /
* | Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Gravatar Hugo Herbelin2016-06-24
* | Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* | Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-06-16
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-06-16
* | Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \ \ | | |/ | |/|
| * | Fix bug #4777: Printing time is impacted by large terms that don't print.Gravatar Pierre-Marie Pédrot2016-06-07
| | * Removing the use to Egramcoq.recover_constr_grammar.Gravatar Pierre-Marie Pédrot2016-06-07
| |/ |/|
* | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
* | Removing pointless field NPatVar. It does not make sense to have MetaGravatar Hugo Herbelin2016-06-02