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
*
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Matej Kosik
2015-12-22
*
COMMENTS: added to the "Constr.case_info" type.
Matej Kosik
2015-12-18
*
CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified
Matej Kosik
2015-12-18
*
CLEANUP: removing unnecessary alias
Matej Kosik
2015-12-18
*
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
Matej Kosik
2015-12-18
*
TYPOGRAPHY: correction of one particular error in the Reference Manual
Matej Kosik
2015-12-18
*
CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...
Matej Kosik
2015-12-18
*
CLEANUP: simplifying "Coqtop.init_gc" implementation
Matej Kosik
2015-12-18
*
CLEANUP: removing unnecessary wrapper function
Matej Kosik
2015-12-18
*
COMMENTS: added to some variants of "Globalnames.global_reference" type.
Matej Kosik
2015-12-18
*
COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.
Matej Kosik
2015-12-18
*
COMMENTS: added to some variants of "Glob_term.glob_constr" type.
Matej Kosik
2015-12-18
*
COMMENTS: added to some variants of the "Constrexpr.prim_token" type.
Matej Kosik
2015-12-18
*
ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file
Matej Kosik
2015-12-18
*
COMMENTS: added to the "Unicode" module.
Matej Kosik
2015-12-18
*
COMMENTS: updated in the "Option" module.
Matej Kosik
2015-12-18
*
COMMENTS: added to some variants of the "Constr.kind_of_term" type.
Matej Kosik
2015-12-18
*
CLEANUP: Vernacexpr.vernac_expr
Matej Kosik
2015-12-18
*
COMMENTS: added to the "Predicate" module
Matej Kosik
2015-12-18
*
COMMENTS: added to the "Names" module.
Matej Kosik
2015-12-18
*
Tying the loop in tactic printing API.
Pierre-Marie Pédrot
2015-12-18
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-17
|
\
*
|
ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_conv
Matej Kosik
2015-12-17
*
|
ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_conv
Matej Kosik
2015-12-17
*
|
CLEANUP: in the Reduction module
Matej Kosik
2015-12-17
*
|
CLEANUP: in the Reductionops module
Matej Kosik
2015-12-17
*
|
CLEANUP: in the Reduction module
Matej Kosik
2015-12-17
*
|
Getting rid of some hardwired generic arguments.
Pierre-Marie Pédrot
2015-12-17
|
*
Updating credits.
Hugo Herbelin
2015-12-16
|
*
Update version numbers and magic numbers for 8.5rc1 release.
Maxime Dénès
2015-12-16
|
*
FIx parsing of tactic "simple refine".
Maxime Dénès
2015-12-16
|
*
Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".
Guillaume Melquiond
2015-12-16
|
*
Extraction: slightly better heuristic for Obj.magic simplifications
Pierre Letouzey
2015-12-16
|
*
Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplifications
Pierre Letouzey
2015-12-16
|
*
Proof using: do not clear unused section hyps automatically
Enrico Tassi
2015-12-15
|
*
Fix test suite after change in extraction.
Maxime Dénès
2015-12-15
|
*
Extraction: more cautious use of intermediate result caching (fix #3923)
Pierre Letouzey
2015-12-15
|
*
Fix test-suite files after change in refine tactic.
Maxime Dénès
2015-12-15
|
*
Extraction: fix a few little glitches with my last commit (replacing unused v...
Pierre Letouzey
2015-12-15
*
|
Fixing e3cefca41b about supposingly simplifying primitive projections
Hugo Herbelin
2015-12-15
*
|
Fixing unexpected length of context in a typing function, detected by
Hugo Herbelin
2015-12-15
|
*
Adding a test for the unshelve tactical.
Pierre-Marie Pédrot
2015-12-15
|
*
Refine tactic now shelves unifiable holes.
Pierre-Marie Pédrot
2015-12-15
*
|
Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.
Hugo Herbelin
2015-12-15
*
|
API: documenting context_chop and removing a duplicate.
Hugo Herbelin
2015-12-15
|
*
Changing the order of the goals generated by unshelve.
Pierre-Marie Pédrot
2015-12-15
*
|
Adding a token "index" representing positions (1st, 2nd, etc.).
Hugo Herbelin
2015-12-15
*
|
Simplifying documentation of "assert form as pat".
Hugo Herbelin
2015-12-15
*
|
Granting clear_flag in injection, even legacy mode. This is possible
Hugo Herbelin
2015-12-15
*
|
Tactics: Generalizing the use of the experimental clearing modifier to
Hugo Herbelin
2015-12-15
[next]