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
*
Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands
Pierre-Marie Pédrot
2018-07-03
|
\
*
\
Merge PR #7703: Add an option to force parameters to be uniform
Matthieu Sozeau
2018-07-02
|
\
\
|
|
*
hints: add Hint Variables/Constants Opaque/Transparent commands
Matthieu Sozeau
2018-07-02
|
|
/
|
/
|
*
|
Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points...
Emilio Jesus Gallego Arias
2018-07-02
|
\
\
|
|
*
Add flag Uniform Inductive Parameters
Jasper Hugunin
2018-07-01
|
|
*
Implement uniform parameters in ComInductive
Jasper Hugunin
2018-07-01
*
|
|
[api] Fix wrong deprecation warning (#7915)
Emilio Jesus Gallego Arias
2018-07-01
|
|
/
|
/
|
*
|
Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...
Emilio Jesus Gallego Arias
2018-07-01
|
\
\
*
\
\
Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break...
Emilio Jesus Gallego Arias
2018-07-01
|
\
\
\
|
|
|
*
Port g_vernac to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
2018-06-29
|
|
|
*
Port g_proofs to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
2018-06-29
|
|
|
*
Use a homebrew parser to replace the GEXTEND extension points of Camlp5.
Pierre-Marie Pédrot
2018-06-29
|
|
_
|
/
|
/
|
|
|
*
|
Workaround to fix #7731 (printing not splitting line at break hint).
Hugo Herbelin
2018-06-29
|
|
*
Fixes #7712 (an anomaly in reporting bad recursive notation format).
Hugo Herbelin
2018-06-29
|
|
/
*
|
Merge PR #7080: Swapping Context and Constr and defining declarations on cons...
Maxime Dénès
2018-06-29
|
\
\
*
|
|
Make Environ.globals abstract.
Gaëtan Gilbert
2018-06-28
|
|
/
|
/
|
*
|
Merge PR #7866: Implementation of mutual records in the higher strata
Maxime Dénès
2018-06-28
|
\
\
|
|
*
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-06-27
|
|
/
|
/
|
*
|
Merge PR #7863: Remove Sorts.contents
Pierre-Marie Pédrot
2018-06-27
|
\
\
*
\
\
Merge PR #7906: universes_of_constr don't include universes of monomorphic co...
Pierre-Marie Pédrot
2018-06-26
|
\
\
\
*
\
\
\
Merge PR #7775: Fix handling of universe context for expanded program obligat...
Maxime Dénès
2018-06-26
|
\
\
\
\
|
|
|
*
|
Remove Sorts.contents
Gaëtan Gilbert
2018-06-26
|
|
_
|
/
/
|
/
|
|
|
|
|
*
|
universes_of_constr don't include universes of monomorphic constants
Gaëtan Gilbert
2018-06-26
*
|
|
|
Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...
Matthieu Sozeau
2018-06-25
|
\
\
\
\
*
\
\
\
\
Merge PR #7559: Existing Class noop when already a class + warning.
Matthieu Sozeau
2018-06-25
|
\
\
\
\
\
|
|
|
|
|
*
Handle mutual record at the vernac level.
Pierre-Marie Pédrot
2018-06-24
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
|
|
Using more general information for primitive records.
Pierre-Marie Pédrot
2018-06-23
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
Fix handling of universe context for expanded program obligations.
Matthieu Sozeau
2018-06-22
|
|
_
|
/
|
/
|
|
|
|
*
Remove hack skipping comparison of algebraic universes in subtyping.
Gaëtan Gilbert
2018-06-22
|
|
/
|
/
|
*
|
Merge PR #7797: Remove reference name type.
Enrico Tassi
2018-06-19
|
\
\
*
\
\
Merge PR #7801: [vernac] Add option to force building really mutual induction...
Enrico Tassi
2018-06-19
|
\
\
\
|
|
*
|
Remove reference name type.
Maxime Dénès
2018-06-18
|
|
/
/
|
/
|
|
*
|
|
Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...
Pierre-Marie Pédrot
2018-06-14
|
\
\
\
|
|
*
|
[vernac] Add option to force building really mutual induction schemes
Matthieu Sozeau
2018-06-13
|
|
/
/
|
/
|
|
*
|
|
[api] Add compatiblity Misctypes module.
Emilio Jesus Gallego Arias
2018-06-12
*
|
|
[api] Remove Misctypes.
Emilio Jesus Gallego Arias
2018-06-12
*
|
|
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
*
|
|
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-06-12
|
|
*
Existing Class noop when already a class + warning.
Gaëtan Gilbert
2018-06-08
|
|
/
|
/
|
*
|
Merge PR #6874: [econstr] Some minor tweaks
Pierre-Marie Pédrot
2018-06-07
|
\
\
*
\
\
Merge PR #7453: Refuse to parse empty [Context] command.
Matthieu Sozeau
2018-06-05
|
\
\
\
*
\
\
\
Merge PR #7315: An attempt to clarify error message for Arguments needing "re...
Maxime Dénès
2018-06-04
|
\
\
\
\
*
\
\
\
\
Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-
Pierre-Marie Pédrot
2018-06-04
|
\
\
\
\
\
|
|
|
|
*
|
[econstr] Remove some Unsafe.to_constr use.
Emilio Jesus Gallego Arias
2018-06-04
|
|
|
|
*
|
[vernac] Switch back `auto_ind_decl` to Constr.
Emilio Jesus Gallego Arias
2018-06-04
|
|
_
|
_
|
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #7657: Fix a couple typos in deprecation messages
Pierre-Marie Pédrot
2018-06-04
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
|
Refuse to parse empty [Context] command.
Gaëtan Gilbert
2018-06-02
|
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
[next]