index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
Commit message (
Expand
)
Author
Age
*
Honor parsing and printing levels for tactic entry in TACTIC EXTEND and
Hugo Herbelin
2016-04-27
*
Being defensive in printing implicit arguments also with manual
Hugo Herbelin
2016-04-27
*
Not taking arguments given by name or position into account when
Hugo Herbelin
2016-04-27
*
A heuristic to add parentheses in the presence of rules such as
Hugo Herbelin
2016-04-27
*
Fixing a "This clause is redundant" error when interpreting the "in"
Hugo Herbelin
2016-04-27
*
Reformatting + removal of some useless data + some cut-elimination
Hugo Herbelin
2016-04-27
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
|
*
Fixing #4677 (collision of a global variable and of a local variable
Hugo Herbelin
2016-04-19
*
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
\
*
|
|
Adding a new Ltac generic argument for forced tactics returing unit.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Removing dead code in Genarg.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Removing the registering of default values for generic arguments.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Adopting the same rules for interpreting @, abbreviations and
Hugo Herbelin
2016-03-13
*
|
|
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-03-13
*
|
|
A more explicit name to the asymmetric boolean flag.
Hugo Herbelin
2016-03-12
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.
Pierre-Marie Pédrot
2016-03-03
*
|
|
Printing notations: Cleaning in anticipation of fixing #4592.
Hugo Herbelin
2016-02-28
*
|
|
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-02-22
*
|
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
\
*
\
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
Do not give a name to anonymous evars anymore. See bug #4547.
Pierre-Marie Pédrot
2016-02-13
|
|
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
|
/
/
|
/
|
|
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
|
*
|
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
Getting rid of the awkward unpack mechanism from Genarg.
Pierre-Marie Pédrot
2016-01-17
*
|
|
Temporary commit getting rid of Obj.magic unsafety for Genarg.
Pierre-Marie Pédrot
2016-01-17
*
|
|
Removing constr generic argument.
Pierre-Marie Pédrot
2016-01-14
*
|
|
Removing ident and var generic arguments.
Pierre-Marie Pédrot
2016-01-14
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-13
|
\
|
|
|
*
|
Fixing #4467 (continued).
Hugo Herbelin
2016-01-13
|
*
|
Fixing #4467 (missing shadowing of variables in cases pattern).
Hugo Herbelin
2016-01-12
*
|
|
CLEANUP: removing unused field
Matej Kosik
2016-01-11
*
|
|
merge
Matej Kosik
2016-01-11
|
\
\
\
|
*
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
|
|
Merge branch 'v8.5' into trunk
Guillaume Melquiond
2015-12-31
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
*
|
|
|
Do not compose List.length with List.filter.
Guillaume Melquiond
2015-12-31
|
*
|
|
Do not dump a glob reference when its location is ghost. (Fix bug #4469)
Guillaume Melquiond
2015-12-31
*
|
|
|
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-28
*
|
|
|
Tentative API fix for tactic arguments to be fed to tclWITHHOLES.
Pierre-Marie Pédrot
2015-12-27
*
|
|
|
Do not compose "str" and "to_string" whenever possible.
Guillaume Melquiond
2015-12-22
*
|
|
|
Removing ad-hoc interpretation rules for tactic notations and their genarg.
Pierre-Marie Pédrot
2015-12-21
*
|
|
|
Sharing toplevel representation for several generic types.
Pierre-Marie Pédrot
2015-12-21
*
|
|
|
Changing the toplevel type of the int_or_var generic type to int.
Pierre-Marie Pédrot
2015-12-21
*
|
|
|
Removing the now useless genarg generic argument.
Pierre-Marie Pédrot
2015-12-21
|
|
/
/
|
/
|
|
*
|
|
CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified
Matej Kosik
2015-12-18
[next]
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau
Matej Kosik
Matthieu Sozeau
Maxime Dénès
Guillaume Melquiond