index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
vernac
Commit message (
Expand
)
Author
Age
*
Obligations shrinking: shrink abstraction too
Matthieu Sozeau
2017-05-11
*
Fix two new unused opens.
Maxime Dénès
2017-05-02
*
Merge PR#582: Fix warnings
Maxime Dénès
2017-05-02
|
\
*
|
More consistent writing of de Bruijn.
Théo Zimmermann
2017-05-01
*
|
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...
Maxime Dénès
2017-04-28
|
\
\
|
|
*
Post-rebase warnings (unused opens and 2 unused values)
Gaetan Gilbert
2017-04-27
|
|
*
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
|
|
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
|
|
*
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-27
|
|
/
|
/
|
*
|
Merge PR#583: [toplevel] More work on error handling.
Maxime Dénès
2017-04-27
|
\
\
|
*
|
[toplevel] Use exception information for error printing.
Emilio Jesus Gallego Arias
2017-04-25
*
|
|
Removing tactic compatibility layer in Command.
Pierre-Marie Pédrot
2017-04-24
|
/
/
*
|
Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.
Maxime Dénès
2017-04-24
|
\
\
*
\
\
Merge PR#565: Remove VernacError
Maxime Dénès
2017-04-24
|
\
\
\
*
|
|
|
[toplevel] [emacs] Don't quote errors in emacs mode.
Emilio Jesus Gallego Arias
2017-04-23
|
*
|
|
Remove VernacError
Gaetan Gilbert
2017-04-21
|
/
/
/
|
*
|
[flags] Deprecate is_silent/is_verbose in favor of single flag.
Emilio Jesus Gallego Arias
2017-04-21
*
|
|
[toplevel] Fix #5475
Emilio Jesus Gallego Arias
2017-04-18
|
/
/
*
|
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-15
*
|
Merge PR#441: Port Toplevel to the Stm API
Maxime Dénès
2017-04-12
|
\
\
|
*
|
[flags] Documentation and a minor tweak.
Emilio Jesus Gallego Arias
2017-04-12
|
*
|
[vernac] vernacentries.mli cleanup
Emilio Jesus Gallego Arias
2017-04-12
|
*
|
[stm] Port the toplevel to the STM.
Emilio Jesus Gallego Arias
2017-04-12
*
|
|
Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...
Maxime Dénès
2017-04-12
|
\
\
\
*
\
\
\
Merge PR#379: Introducing evar-insensitive constrs
Maxime Dénès
2017-04-11
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
Fixing #5420 as well as many related bugs due to miscounting let-ins.
Hugo Herbelin
2017-04-09
|
|
|
*
Fixing several wrong computations of implicit arguments by position
Hugo Herbelin
2017-04-09
|
|
|
*
Minor cosmetic commit.
Hugo Herbelin
2017-04-09
|
|
|
*
Removing internal support for accepting "{struct x}" and co in "Theorem with".
Hugo Herbelin
2017-04-09
|
|
_
|
/
|
/
|
|
|
*
|
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-04-07
|
|
\
\
*
|
|
|
[camlpX] Remove camlp4 compat layer.
Emilio Jesus Gallego Arias
2017-04-07
|
|
/
/
|
/
|
|
*
|
|
Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ...
Maxime Dénès
2017-04-07
|
\
\
\
*
\
\
\
Merge PR#508: Optimize pending evars
Maxime Dénès
2017-04-06
|
\
\
\
\
|
|
*
|
|
[toplevel] Remove exception error printer in favor of feedback printer.
Emilio Jesus Gallego Arias
2017-04-05
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR#502: [pp] Add anomaly header to error messages.
Maxime Dénès
2017-04-04
|
\
\
\
\
|
|
|
*
\
Merge branch 'trunk' into pr379
Maxime Dénès
2017-04-04
|
|
|
|
\
\
|
|
_
|
_
|
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-03
*
|
|
|
|
Merge PR#417: No cast surgery in let in
Maxime Dénès
2017-04-03
|
\
\
\
\
\
|
|
|
|
*
|
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
|
|
|
|
*
|
Actually exporting delayed universes in the EConstr implementation.
Pierre-Marie Pédrot
2017-04-01
*
|
|
|
|
|
Merge PR#511: [stm] Remove some obsolete vernacs/classification.
Maxime Dénès
2017-03-30
|
\
\
\
\
\
\
|
|
|
|
|
*
|
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
|
*
|
|
|
|
|
[stm] Remove some obsolete vernacs/classification.
Emilio Jesus Gallego Arias
2017-03-24
|
|
|
_
|
_
|
/
/
|
|
/
|
|
|
|
*
/
|
|
|
|
[nit] Fix a couple incorrect uses of msg_error.
Emilio Jesus Gallego Arias
2017-03-24
|
/
/
/
/
/
|
*
|
|
|
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
|
*
|
|
|
Unifying standard "constr_level" names for constructors of local_binder_expr.
Hugo Herbelin
2017-03-24
|
*
|
|
|
Renaming local_binder into local_binder_expr.
Hugo Herbelin
2017-03-24
|
*
|
|
|
"Standardizing" the name LocalPatten into LocalRawPattern.
Hugo Herbelin
2017-03-24
|
/
/
/
/
|
|
|
*
Improving the API of constrexpr_ops.mli.
Hugo Herbelin
2017-03-23
|
|
_
|
/
|
/
|
|
|
|
*
Ensuring static invariants about handling of pending evars in Pretyping.
Pierre-Marie Pédrot
2017-03-23
|
|
/
|
/
|
[next]