aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2016-06-27minor: documentation comment for constrintern.ml:sort_fieldsGabriel Scherer
2016-06-27minor: interp/constrintern.ml, clarify field completionGabriel Scherer
2016-06-27minor: in constrintern.ml:sort_fields, clarify sfGabriel Scherer
2016-06-27minor: in constrintern.ml:sort_fields, clarify build_pattGabriel Scherer
2016-06-27whitespace: untabity constrinternl.ml:sort_fieldsGabriel Scherer
2016-06-27minor clarifications in constrintern.ml:sort_fieldsGabriel Scherer
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-25[feedback] Add optional ?loc parameter to loggers.Emilio Jesus Gallego Arias
2016-06-24Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Hugo Herbelin
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-16Being defensive in printing implicit arguments also with manualHugo Herbelin
2016-06-16Not taking arguments given by name or position into account whenHugo Herbelin
2016-06-16Merge remote-tracking branch 'github/pr/194' into trunkMaxime Dénès
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-07Fix bug #4777: Printing time is impacted by large terms that don't print.Pierre-Marie Pédrot
2016-06-07Removing the use to Egramcoq.recover_constr_grammar.Pierre-Marie Pédrot
2016-06-02Remove tabulation support from pretty-printing.Guillaume Melquiond
2016-06-02A slight phase of documentation and uniformization of names ofHugo Herbelin
2016-06-02Removing pointless field NPatVar. It does not make sense to have MetaHugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04Increase the size of the dumpglob buffer for cooking notations (bug #4708).Guillaume Melquiond
2016-05-03Fix bug #3825: Universe annotations on notations should pass through or be re...Pierre-Marie Pédrot
2016-04-27Revert "A heuristic to add parentheses in the presence of rules such as"Hugo Herbelin
2016-04-27Revert "Not taking arguments given by name or position into account when"Hugo Herbelin
2016-04-27Revert "Being defensive in printing implicit arguments also with manual"Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Revert "Warn about possible shadowing of a name occurring in a "in" clause."Hugo Herbelin
2016-04-27Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Warn about possible shadowing of a name occurring in a "in" clause.Hugo Herbelin
2016-04-27Honor parsing and printing levels for tactic entry in TACTIC EXTEND andHugo Herbelin
2016-04-27Being defensive in printing implicit arguments also with manualHugo Herbelin
2016-04-27Not taking arguments given by name or position into account whenHugo Herbelin
2016-04-27A heuristic to add parentheses in the presence of rules such asHugo Herbelin
2016-04-27Fixing a "This clause is redundant" error when interpreting the "in"Hugo Herbelin
2016-04-27Reformatting + removal of some useless data + some cut-eliminationHugo Herbelin
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-03-20Adding a new Ltac generic argument for forced tactics returing unit.Pierre-Marie Pédrot
2016-03-19Removing dead code in Genarg.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-03-13Adopting the same rules for interpreting @, abbreviations andHugo Herbelin
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 14:00:44 +0000