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
*
Extraction: cosmetically avoid generating spaces on empty lines
Pierre Letouzey
2015-12-14
*
Extraction: also get rid of explicit '\n' for haskell
Pierre Letouzey
2015-12-14
*
Extraction: fix a pretty-print issue
Pierre Letouzey
2015-12-14
*
Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")
Pierre Letouzey
2015-12-14
*
Extraction: documentation of the new option Unset Extraction SafeImplicits
Pierre Letouzey
2015-12-12
*
Extraction: nicer implementation of Implicits
Pierre Letouzey
2015-12-12
*
Extraction: check for remaining implicits after dead code removal (fix #4243)
Pierre Letouzey
2015-12-12
*
Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)
Pierre Letouzey
2015-12-12
*
Extraction: avoid generating some blanks at end-of-line
Pierre Letouzey
2015-12-12
*
Indexing and documenting some options.
Pierre-Marie Pédrot
2015-12-12
*
Optimize occur_evar_upto_types, avoiding repeateadly looking into the
Matthieu Sozeau
2015-12-11
*
Univs: Fix bug #4363, nested abstract.
Matthieu Sozeau
2015-12-11
*
Document removal of Set Virtual Machine and -vm in CHANGES.
Maxime Dénès
2015-12-11
*
Remove Set Virtual Machine from doc, since the command itself has been removed.
Maxime Dénès
2015-12-11
*
Add tactic native_cast_no_check, analog to vm_cast_no_check.
Maxime Dénès
2015-12-11
*
Fixing a pat%constr bug. Thanks to Enrico for reporting.
Hugo Herbelin
2015-12-10
*
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Hugo Herbelin
2015-12-10
*
Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing
Hugo Herbelin
2015-12-10
*
Silently ignore requests to _not_ clear something when that something cannot ...
Guillaume Melquiond
2015-12-10
*
Refman, ch. 4: A few fixes.
Hugo Herbelin
2015-12-10
*
ENH: redundant examples were removed
Matej Kosik
2015-12-10
*
FIX: wrong reference to a figure
Matej Kosik
2015-12-10
*
CLEANUP: putting examples inside "figure" environment
Matej Kosik
2015-12-10
*
ENH: The definition of the "_ ; _" operation on local context was added.
Matej Kosik
2015-12-10
*
TYPOGRAPHY: adjustments
Matej Kosik
2015-12-10
*
PROPOSITION: the side-condition was made more specific.
Matej Kosik
2015-12-10
*
PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'
Matej Kosik
2015-12-10
*
PROPOSITION: Added an explicit definition of the notation for enriching the g...
Matej Kosik
2015-12-10
*
PROPOSITION: Added "if" and "then" words missing in the original sentence.
Matej Kosik
2015-12-10
*
PROPOSITION: Example was simplified
Matej Kosik
2015-12-10
*
DONE
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
TYPOGRAPHY
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: to do
Matej Kosik
2015-12-10
*
GRAMMAR: added punctuation
Matej Kosik
2015-12-10
*
CLEANUP PROPOSITION: rephrasing the original idea in a simpler way
Matej Kosik
2015-12-10
*
CLEANUP PROPOSITION: existing example was removed because it is not urgently ...
Matej Kosik
2015-12-10
*
ENH: existing example was changed so that it is now linked to the results sho...
Matej Kosik
2015-12-10
*
ENH: an existing example was further expanded.
Matej Kosik
2015-12-10
*
CLEANUP: Existing example was removed.
Matej Kosik
2015-12-10
*
ENH: existing example was expanded
Matej Kosik
2015-12-10
*
ENH: define the meaning of 'p'
Matej Kosik
2015-12-10
*
CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive definit...
Matej Kosik
2015-12-10
*
CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive de...
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
[next]