aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2016-07-12removing ocamldoc-related syntax errorsMatej Kosik
2016-07-07Merge remote-tracking branch 'github/bug4653' into v8.6Matthieu Sozeau
2016-07-07Do not use implicit type info for (x := t) bindingsMatthieu Sozeau
2016-07-07Program: fix #4873: transparency option not usedMatthieu Sozeau
2016-07-06Univs: fix internalization of (x := T) and castsMatthieu Sozeau
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29Fixing #4865 (deciding on which arguments to recompute scopes was not robust).Hugo Herbelin
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-28Properly handling the only printing flag when parsing rules already exist.Pierre-Marie Pédrot
2016-06-27Univs: allowing notations to take univ instancesMatthieu Sozeau
2016-06-27Forbidding silently dropped universes instances inMatthieu Sozeau
2016-06-27Merge remote-tracking branch 'github/pr/223' into feedback-locationsMaxime Dénès
2016-06-27minor: comment on the meaning of the 'boolean' variableGabriel Scherer
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 00:39:10 +0000