index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Merge remote-tracking branch 'github/pr/223' into feedback-locations
Maxime Dénès
2016-06-27
|
\
*
|
ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTEND
Pierre Letouzey
2016-06-27
*
|
Merge branch 'sort-fields' into trunk
Maxime Dénès
2016-06-27
|
\
\
*
\
\
Merge branch 'funpattern-tests' into trunk.
Maxime Dénès
2016-06-27
|
\
\
\
|
|
*
|
minor: comment on the meaning of the 'boolean' variable
Gabriel Scherer
2016-06-27
|
|
*
|
minor: documentation comment for constrintern.ml:sort_fields
Gabriel Scherer
2016-06-27
|
|
*
|
minor: interp/constrintern.ml, clarify field completion
Gabriel Scherer
2016-06-27
|
|
*
|
minor: in constrintern.ml:sort_fields, clarify sf
Gabriel Scherer
2016-06-27
|
|
*
|
add CList.extract_first
Gabriel Scherer
2016-06-27
|
|
*
|
minor: in constrintern.ml:sort_fields, clarify build_patt
Gabriel Scherer
2016-06-27
|
|
*
|
whitespace: untabity constrinternl.ml:sort_fields
Gabriel Scherer
2016-06-27
|
|
*
|
minor clarifications in constrintern.ml:sort_fields
Gabriel Scherer
2016-06-27
|
|
/
/
|
/
|
|
|
*
|
Patterns in binders: printing tests
Arnaud Spiwack
2016-06-27
|
*
|
Patterns in binders: functional tests
Arnaud Spiwack
2016-06-27
|
/
/
*
|
Merge branch 'funpattern' into trunk. Was PR#142: Binder syntax.
Maxime Dénès
2016-06-27
|
\
\
|
*
|
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
|
|
*
[xmlproto] Remove duplicated deserialization.
Emilio Jesus Gallego Arias
2016-06-25
|
|
*
[doc] Update changes for feedback.
Emilio Jesus Gallego Arias
2016-06-25
|
|
*
[feedback] Remove `ErrorMsg` in favor of `Message Error`.
Emilio Jesus Gallego Arias
2016-06-25
|
|
*
[feedback] Allow messages to carry a location.
Emilio Jesus Gallego Arias
2016-06-25
|
|
*
[feedback] Add optional ?loc parameter to loggers.
Emilio Jesus Gallego Arias
2016-06-25
|
|
*
[feedback] Remove unused tag on `Debug` level.
Emilio Jesus Gallego Arias
2016-06-25
|
|
*
[merlin] Fix .merlin STM includes.
Emilio Jesus Gallego Arias
2016-06-25
|
|
/
*
|
Several easy but efficient optimizations for subst and clear tactics.
Pierre-Marie Pédrot
2016-06-24
|
\
|
|
*
Optimize the subst tactic.
Pierre-Marie Pédrot
2016-06-24
|
*
Optmimize the subst tactic.
Pierre-Marie Pédrot
2016-06-24
|
*
Optim in Clenv: use noccurn instead of depends.
Pierre-Marie Pédrot
2016-06-24
|
*
Optimize the subst tactic.
Pierre-Marie Pédrot
2016-06-24
|
*
Optimize the clear tactic.
Pierre-Marie Pédrot
2016-06-24
|
*
Optimize the clear tactic.
Pierre-Marie Pédrot
2016-06-24
|
*
Optimization in the subst tactic.
Pierre-Marie Pédrot
2016-06-24
|
*
Optimization in the subst tactic.
Pierre-Marie Pédrot
2016-06-24
|
*
Optimization in the subst tactic.
Pierre-Marie Pédrot
2016-06-24
|
/
*
Removing tactic compatibility layers in setoid_ring.
Pierre-Marie Pédrot
2016-06-24
*
Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).
Hugo Herbelin
2016-06-24
*
Makefile.install: fix a typo in last commit c954bb5, sorry
Pierre Letouzey
2016-06-24
*
remove an old workaround for OCaml 3.11 + MacOS natdynlink
Pierre Letouzey
2016-06-24
*
Makefile.build: mitigate potential issues with multiple creations of pack .cmi
Pierre Letouzey
2016-06-24
*
Makefile.install: fix the install of plugin cmi
Pierre Letouzey
2016-06-24
*
Better algorithm for variable deambiguation in term printing.
Pierre-Marie Pédrot
2016-06-23
*
Makefile.doc: fix 'make doc'
Pierre Letouzey
2016-06-23
*
Makefile.build: "make;make" should redo nothing
Pierre Letouzey
2016-06-22
*
Makefile: compat5* moved in grammar/, less -I given to camlp4o
Pierre Letouzey
2016-06-21
*
Parsing/compat.ml4: avoid "let open" syntax, unsupported by my camlp5 6.11
Pierre Letouzey
2016-06-21
*
Merge remote-tracking branch 'github/pr/212' into trunk
Maxime Dénès
2016-06-20
|
\
|
*
Add file name, line number and beginning of line position to locations.
Maxime Dénès
2016-06-20
*
|
LtacProf reports structured results (pr/209)
CJ Bell
2016-06-20
*
|
COMMENTS: Vernacexpr.extend_name
Matej Kosik
2016-06-20
*
|
Small optimization in clear_body.
Pierre-Marie Pédrot
2016-06-20
*
|
Fix bug #4825: [clear] should not dependency-check hypotheses that come above...
Pierre-Marie Pédrot
2016-06-20
[next]