index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernacentries.ml
Commit message (
Expand
)
Author
Age
*
rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...
Pierre Letouzey
2016-07-03
*
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
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
|
\
|
*
Remove the syntax changes introduced by this branch.
Pierre-Marie Pédrot
2016-06-15
|
*
Assume totality: dedicated type rather than bool
Arnaud Spiwack
2016-06-14
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
|
Put the "exact_constr" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
Put the "clear" tactic into the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
\
|
*
|
Call hooks when terminating a definition proof (bug #4663).
Guillaume Melquiond
2016-05-03
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
|
|
|
*
|
Building lazily a few debugging messages involving expressions of commands
Hugo Herbelin
2016-04-17
*
|
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
\
\
*
|
|
|
Moving Tacintern to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Moving Print Ltac to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Moving Tacinterp to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
Moving VernacSolve to an EXTEND-based definition.
Pierre-Marie Pédrot
2016-03-19
*
|
|
|
Replacing the interpretation of Proof using ... with a proper code.
Pierre-Marie Pédrot
2016-03-19
*
|
|
|
Removing OCaml deprecated function names from the Lazy module.
Pierre-Marie Pédrot
2016-03-10
*
|
|
|
Moving Autorewrite to Hightatctic.
Pierre-Marie Pédrot
2016-03-06
*
|
|
|
Moving Tactic_debug to tactics/ folder.
Pierre-Marie Pédrot
2016-03-06
*
|
|
|
Moving the "clear" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
|
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
|
*
|
|
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
/
/
/
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
|
merge
Matej Kosik
2016-01-11
|
\
\
\
\
|
*
|
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
|
|
Do not compose "str" and "to_string" whenever possible.
Guillaume Melquiond
2015-12-22
|
/
/
/
/
*
|
|
|
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
Matej Kosik
2015-12-18
*
|
|
|
CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...
Matej Kosik
2015-12-18
*
|
|
|
CLEANUP: Vernacexpr.vernac_expr
Matej Kosik
2015-12-18
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
|
|
*
|
|
Fix [Polymorphic Hint Rewrite].
Matthieu Sozeau
2015-11-27
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
|
|
*
|
|
Fix output of universe arcs. (Fix bug #4422)
Guillaume Melquiond
2015-11-23
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
|
|
*
|
|
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-11-02
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
|
|
*
|
|
Univs: local names handling.
Matthieu Sozeau
2015-10-28
|
*
|
|
Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names
Matthieu Sozeau
2015-10-27
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
|
|
[next]
Pierre Letouzey
Maxime Dénès
Pierre-Marie Pédrot
Arnaud Spiwack
Emilio Jesus Gallego Arias
Guillaume Melquiond
Hugo Herbelin
Matthieu Sozeau
Matej Kosik
Matthieu Sozeau