index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
command.ml
Commit message (
Expand
)
Author
Age
*
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
2017-02-15
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-12-07
|
\
|
*
Merge remote-tracking branch 'github/pr/366' into v8.6
Maxime Dénès
2016-12-04
|
|
\
|
*
|
Comment on universe handling in Parameters
Matthieu Sozeau
2016-12-02
|
*
|
Univs: fix bug #5188
Matthieu Sozeau
2016-12-02
|
|
*
Fix UGraph.check_eq!
Matthieu Sozeau
2016-11-30
|
|
/
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
\
|
|
*
Renamings to avoid confusion deprecating old names
Matthieu Sozeau
2016-10-22
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-23
|
\
|
*
|
Revert "Merge remote-tracking branch 'github/pr/283' into trunk"
Maxime Dénès
2016-09-22
*
|
Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.
Maxime Dénès
2016-09-20
*
|
Stylistic improvements in intf/decl_kinds.mli.
Maxime Dénès
2016-09-20
|
*
Fix warning when using Variables at toplevel.
Maxime Dénès
2016-09-19
*
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
*
|
|
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-30
*
|
|
CLEANUP: taking advantage of "_ % _" operator to express function composition...
Matej Kosik
2016-08-29
*
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
|
/
|
/
|
|
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
*
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-07-29
|
\
|
*
Fix bug #3886, generation of obligations of fixes
Matthieu Sozeau
2016-07-29
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
|
Univs: earlier errors for strict univ decls #4527
Matthieu Sozeau
2016-06-29
*
|
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-27
|
\
|
*
|
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
*
|
Reuse the typing_flags datatype for inductives.
Pierre-Marie Pédrot
2016-06-18
*
|
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-18
*
|
Factorizing the uses of Declareops.safe_flags.
Pierre-Marie Pédrot
2016-06-16
*
|
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
\
|
*
|
Allow `Pretyping.search_guard` to not check guard
Arnaud Spiwack
2016-06-15
|
*
|
Assume totality: dedicated type rather than bool
Arnaud Spiwack
2016-06-14
*
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
|
*
Univs/Program/Function: Fix bug #4725
Matthieu Sozeau
2016-05-26
*
|
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
|
Removing OCaml deprecated function names from the Lazy module.
Pierre-Marie Pédrot
2016-03-10
*
|
|
Renaming variants of Entries.local_entry
Matej Kosik
2016-02-16
*
|
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
\
*
|
|
|
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-02-15
*
|
|
|
Renaming functions in Typing to stick to the standard e_* scheme.
Pierre-Marie Pédrot
2016-02-15
|
*
|
|
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
*
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
|
/
/
*
|
Univs: correctly register universe binders for lemmas.
Matthieu Sozeau
2015-11-28
*
|
Allow program hooks to see the refined universe_context at the end of a
Matthieu Sozeau
2015-11-19
[next]