aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2016-03-12A more explicit name to the asymmetric boolean flag.Hugo Herbelin
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-03Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Pierre-Marie Pédrot
2016-02-28Printing notations: Cleaning in anticipation of fixing #4592.Hugo Herbelin
2016-02-22The tactic generic argument now returns a value rather than a glob_expr.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17Getting rid of the awkward unpack mechanism from Genarg.Pierre-Marie Pédrot
2016-01-17Temporary commit getting rid of Obj.magic unsafety for Genarg.Pierre-Marie Pédrot
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-14Removing ident and var generic arguments.Pierre-Marie Pédrot
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-13Fixing #4467 (continued).Hugo Herbelin
2016-01-12Fixing #4467 (missing shadowing of variables in cases pattern).Hugo Herbelin
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-02Remove some unused functions.Guillaume Melquiond
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-31Do not compose List.length with List.filter.Guillaume Melquiond
2015-12-31Do not dump a glob reference when its location is ghost. (Fix bug #4469)Guillaume Melquiond
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-27Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Pierre-Marie Pédrot
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-21Removing ad-hoc interpretation rules for tactic notations and their genarg.Pierre-Marie Pédrot
2015-12-21Sharing toplevel representation for several generic types.Pierre-Marie Pédrot
2015-12-21Changing the toplevel type of the int_or_var generic type to int.Pierre-Marie Pédrot
2015-12-21Removing the now useless genarg generic argument.Pierre-Marie Pédrot
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-02Fix a bug in externalisation which prevented printing of projectionsMatthieu Sozeau
2015-11-26Make the pretty printer resilient to incomplete nametab (progress on #4363).Enrico Tassi
2015-11-11Fixing bug #3554: Anomaly: Anonymous implicit argument.Pierre-Marie Pédrot
2015-10-26Documenting a bit more interpretation functions in passing.Hugo Herbelin
2015-10-13Fix some typos.Guillaume Melquiond
2015-09-16Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #...Guillaume Melquiond
2015-08-21Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Hugo Herbelin
2015-08-14Move type_scope into user space, fix some output logsJason Gross
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-07-29Fixing bug #3811: "Universe annotations confused inside generalizing binders".Pierre-Marie Pédrot
2015-07-27Fixing #4305 (compatibility wrt 8.4 in not interpreting anHugo Herbelin
2015-07-08Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262)Guillaume Melquiond
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-05-27Fix bug #4159Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 15:31:03 +0000