index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
Commit message (
Expand
)
Author
Age
*
Merge PR #6961: [test-suite] Add backtracking test for `Load`.
Enrico Tassi
2018-03-28
|
\
*
|
Slightly refining some error messages about unresolvable evars.
Hugo Herbelin
2018-03-24
|
*
[test-suite] Add backtracking test for `Load`.
Emilio Jesus Gallego Arias
2018-03-10
|
/
*
Merge PR #6946: Fix expected number of arguments for cumulative constructors.
Maxime Dénès
2018-03-09
|
\
*
\
Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...
Maxime Dénès
2018-03-09
|
\
\
|
|
*
Fix expected number of arguments for cumulative constructors.
Gaëtan Gilbert
2018-03-09
|
|
/
|
/
|
*
|
Merge PR #6775: Allow using cumulativity without forcing strict constraints.
Maxime Dénès
2018-03-09
|
\
\
|
|
*
Revert "Merge PR #873: New strategy based on open scopes for deciding which n...
Maxime Dénès
2018-03-09
|
|
/
|
/
|
|
*
Delayed weak constraints for cumulative inductive types.
Gaëtan Gilbert
2018-03-09
|
*
Cumulativity: improve treatment of irrelevant universes.
Gaëtan Gilbert
2018-03-09
|
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
*
|
Merge PR #6480: Allow Prop as source for coercions
Maxime Dénès
2018-03-09
|
\
\
|
|
/
|
/
|
*
|
Merge PR #6895: [compat] Remove "Refolding Reduction" option.
Maxime Dénès
2018-03-09
|
\
\
|
|
*
added test for coercion from type
charguer
2018-03-09
|
|
*
allow Prop as source for coercions
charguer
2018-03-09
|
|
/
|
/
|
*
|
Merge PR #6945: Fix error with univ binders on monomorphic records.
Maxime Dénès
2018-03-09
|
\
\
*
\
\
Merge PR #6155: Get rid of ' notation for Zpos in QArith
Maxime Dénès
2018-03-09
|
\
\
\
*
\
\
\
Merge PR #6747: Relax conversion of constructors according to the pCuIC model
Maxime Dénès
2018-03-09
|
\
\
\
\
*
\
\
\
\
Merge PR #6328: Fix #6313: lost goals in nested ltac in refine
Maxime Dénès
2018-03-09
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values
Maxime Dénès
2018-03-09
|
\
\
\
\
\
\
|
|
*
|
|
|
|
More examples about shelve/given_up in tactic-in-terms.
Hugo Herbelin
2018-03-08
|
|
*
|
|
|
|
Proof engine: support for nesting tactic-in-term within other tactics.
Hugo Herbelin
2018-03-08
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6522: Fix core hint database issue #6521
Maxime Dénès
2018-03-08
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials
Maxime Dénès
2018-03-08
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...
Maxime Dénès
2018-03-08
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
*
[compat] Remove "Refolding Reduction" option.
Emilio Jesus Gallego Arias
2018-03-08
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Fix error with univ binders on monomorphic records.
Gaëtan Gilbert
2018-03-08
|
|
|
|
*
|
|
|
Fix SR breakage due to allowing fixpoints on non-rec values
Matthieu Sozeau
2018-03-08
|
|
|
|
|
*
|
|
Add test-suite file for cumulative constructors
Matthieu Sozeau
2018-03-08
|
|
|
|
|
|
|
/
|
|
|
|
|
|
/
|
*
|
|
|
|
|
|
Merge PR #6899: [compat] Remove "Standard Proposition Elimination"
Maxime Dénès
2018-03-08
|
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge PR #6582: Mangle auto-generated names
Maxime Dénès
2018-03-08
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6903: [compat] Remove "Shrink Abstract"
Maxime Dénès
2018-03-08
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)
Maxime Dénès
2018-03-08
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`
Maxime Dénès
2018-03-07
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #6790: Allow universe declarations for [with Definition].
Maxime Dénès
2018-03-07
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)
Maxime Dénès
2018-03-07
|
\
\
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
*
|
|
|
|
An experimental 'Show Extraction' command (grant feature wish #4129)
Pierre Letouzey
2018-03-06
|
|
|
|
|
*
|
|
|
|
|
|
|
[compat] Remove "Shrink Abstract"
Emilio Jesus Gallego Arias
2018-03-06
|
|
_
|
_
|
_
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
|
Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...
Maxime Dénès
2018-03-06
|
\
\
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
|
|
|
|
ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)
Enrico Tassi
2018-03-06
*
|
|
|
|
|
|
|
|
|
|
|
|
Merge PR #6896: [compat] Remove NOOP deprecated options.
Maxime Dénès
2018-03-06
|
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6824: Remove deprecated options related to typeclasses.
Maxime Dénès
2018-03-06
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
CHANGES and tests for with Definition @{univs}
Gaëtan Gilbert
2018-03-05
|
|
|
|
*
|
|
|
|
|
|
|
|
|
Sanitize universe declaration in Context (stop using a ref...)
Gaëtan Gilbert
2018-03-05
|
|
|
|
|
/
/
/
/
/
/
/
/
/
*
|
|
|
|
|
|
|
|
|
|
|
|
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
\
\
\
\
\
\
\
\
\
\
\
\
|
|
|
*
|
|
|
|
|
|
|
|
|
|
[compat] Remove NOOP and alias deprecated options.
Emilio Jesus Gallego Arias
2018-03-04
|
|
|
|
|
/
/
/
/
/
/
/
/
/
|
|
|
|
/
|
|
|
|
|
|
|
|
|
|
|
*
/
|
|
|
|
|
|
|
|
|
Remove deprecated options related to typeclasses.
Théo Zimmermann
2018-03-04
|
|
|
/
/
/
/
/
/
/
/
/
/
|
|
|
|
*
/
/
/
/
/
/
/
ssr: add Prenex Implicits for Some_inj to use it as a view
Anton Trunov
2018-03-04
|
|
|
|
/
/
/
/
/
/
/
/
|
|
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
Merge PR #935: Handling evars in the VM
Maxime Dénès
2018-03-04
|
\
\
\
\
\
\
\
\
\
\
\
|
|
_
|
/
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
Merge PR #6791: Removing compatibility support for versions older than 8.5.
Maxime Dénès
2018-03-04
|
\
\
\
\
\
\
\
\
\
\
\
[next]