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
*
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
*
|
Command.declare_definition: grab the fix_exn early (follows 77cf18e)
Enrico Tassi
2015-10-30
*
|
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
|
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
|
Univs: fix bug #4375, accept universe binders on (co)-fixpoints
Matthieu Sozeau
2015-10-28
*
|
Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names
Matthieu Sozeau
2015-10-27
*
|
Fix Definition id := Eval <redexpr> in by passing the right universe
Matthieu Sozeau
2015-10-12
*
|
Axioms now support the universe binding syntax.
Pierre-Marie Pédrot
2015-10-08
*
|
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
|
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
*
|
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
|
*
Declare assumptions of well-founded definitions as unsafe.
Arnaud Spiwack
2015-09-25
|
*
Propagate `Guarded` flag from syntax to kernel.
Arnaud Spiwack
2015-09-25
|
*
Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...
Arnaud Spiwack
2015-09-25
*
|
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
|
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
*
|
Fix bug #4254 with the help of J.H. Jourdan
Matthieu Sozeau
2015-06-26
|
*
Add a flag to deactivate guard checking in the kernel.
Arnaud Spiwack
2015-06-26
|
*
When assuming an inductive type positive, then it is declared "unsafe" to the...
Arnaud Spiwack
2015-06-24
|
*
Add corresponding field in `VernacInductive`.
Arnaud Spiwack
2015-06-24
|
*
Add a corresponding field in `mutual_inductive_entry` (part 1).
Arnaud Spiwack
2015-06-24
|
/
[next]