aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* 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
* 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
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* | More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Increase the size of the dumpglob buffer for cooking notations (bug #4708).Gravatar Guillaume Melquiond2016-05-04
| * Fix bug #3825: Universe annotations on notations should pass through or be re...Gravatar Pierre-Marie Pédrot2016-05-03
* | Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
* | Revert "Not taking arguments given by name or position into account when"Gravatar Hugo Herbelin2016-04-27
* | Revert "Being defensive in printing implicit arguments also with manual"Gravatar Hugo Herbelin2016-04-27
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* | Revert "Warn about possible shadowing of a name occurring in a "in" clause."Gravatar Hugo Herbelin2016-04-27
* | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Gravatar Hugo Herbelin2016-04-27
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* | Warn about possible shadowing of a name occurring in a "in" clause.Gravatar Hugo Herbelin2016-04-27
* | Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
* | Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-04-27
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-04-27
* | A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
* | Fixing a "This clause is redundant" error when interpreting the "in"Gravatar Hugo Herbelin2016-04-27
* | Reformatting + removal of some useless data + some cut-eliminationGravatar Hugo Herbelin2016-04-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \
* | | Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Removing dead code in Genarg.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 10:28:55 +0000