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
*
Update coq_makefile timing test
Jason Gross
2018-04-02
*
Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)
Pierre-Marie Pédrot
2018-04-01
|
\
*
|
Change Implicit Arguments to Arguments in test-suite
Jasper Hugunin
2018-03-30
*
|
Fix #6631: Derive Plugin gives "Anomaly: more than one statement".
Pierre-Marie Pédrot
2018-03-29
|
*
Supporting fix/cofix in Ltac pattern-matching (wish #7092).
Hugo Herbelin
2018-03-28
*
|
Merge PR #7090: stm: don't propagate side effects when editing a proof
Emilio Jesus Gallego Arias
2018-03-28
|
\
\
*
\
\
Merge PR #6961: [test-suite] Add backtracking test for `Load`.
Enrico Tassi
2018-03-28
|
\
\
\
|
|
*
|
stm: don't propagate side effects when editing a proof
Enrico Tassi
2018-03-27
|
|
|
/
*
|
/
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
[next]