aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* 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
* | | Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Adopting the same rules for interpreting @, abbreviations andGravatar Hugo Herbelin2016-03-13
* | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* | | A more explicit name to the asymmetric boolean flag.Gravatar Hugo Herbelin2016-03-12
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ | | |/ | |/|
| * | Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Gravatar Pierre-Marie Pédrot2016-03-03
* | | Printing notations: Cleaning in anticipation of fixing #4592.Gravatar Hugo Herbelin2016-02-28
* | | The tactic generic argument now returns a value rather than a glob_expr.Gravatar Pierre-Marie Pédrot2016-02-22
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ \ | | |/ / | |/| |
| * | | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
| | * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ / |/| |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\| |
| * | Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | | Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
* | | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\| |
| * | Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| * | Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
* | | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | | mergeGravatar Matej Kosik2016-01-11
|\ \ \
| * | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\ \ \ \ | | |/ / | |/| |
* | | | Do not compose List.length with List.filter.Gravatar Guillaume Melquiond2015-12-31
| * | | Do not dump a glob reference when its location is ghost. (Fix bug #4469)Gravatar Guillaume Melquiond2015-12-31
* | | | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | | | Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
* | | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
* | | | Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
* | | | Sharing toplevel representation for several generic types.Gravatar Pierre-Marie Pédrot2015-12-21
* | | | Changing the toplevel type of the int_or_var generic type to int.Gravatar Pierre-Marie Pédrot2015-12-21
* | | | Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
| |/ / |/| |
* | | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18