index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
output
Age
Commit message (
Expand
)
Author
2018-09-21
Add test for univ names of polymorphic inductives in sections.
Gaëtan Gilbert
2018-09-21
Universe binders are Id, not Name. Never print Var.
Gaëtan Gilbert
2018-09-21
Best-effort hack to provide a meaningful name for anonymous bound universes.
Pierre-Marie Pédrot
2018-09-21
Removing calls to AUContext.instance.
Pierre-Marie Pédrot
2018-09-14
Fixing yet a source of dependency on alphabetic order in unification.
Hugo Herbelin
2018-09-12
Remove quote plugin
Maxime Dénès
2018-09-11
Merge PR #7288: Isolating ltac naming out of pretyping + fixing renaming
Pierre-Marie Pédrot
2018-09-11
Merge PR #7135: Introducing an explicit `Declare Scope` command
Emilio Jesus Gallego Arias
2018-09-10
Merge PR #8417: Fixing #8416: Print Assumptions missing module information fr...
Matthieu Sozeau
2018-09-10
Adapting standard library to the introduction of "Declare Scope".
Hugo Herbelin
2018-09-10
Fixing an inconsistency in interpreting Ltac names linking to binder names.
Hugo Herbelin
2018-09-05
Fixing #8416 (Print Assumptions missing module information from compiled files).
Hugo Herbelin
2018-08-28
Close #8091: print universe context for Eval when option on.
Gaëtan Gilbert
2018-08-28
Fix #8291: print universe names in universe context for Check.
Gaëtan Gilbert
2018-07-29
Adding support for custom entries in notations.
Hugo Herbelin
2018-07-26
Add information to option type errors
Tej Chajed
2018-07-26
Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...
Pierre-Marie Pédrot
2018-07-25
In "redundant clause" pattern-matching error, show also the pattern (#7777).
Hugo Herbelin
2018-07-24
Fixes #8126 (issue with notations and nested applications).
Hugo Herbelin
2018-07-17
Change QuestionMark for better record field missing error message.
Siddharth Bhat
2018-07-12
Tactic deprecation machinery
Maxime Dénès
2018-06-29
Workaround to fix #7731 (printing not splitting line at break hint).
Hugo Herbelin
2018-06-14
Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...
Pierre-Marie Pédrot
2018-06-10
Tweak printing boxes for unicode binders
Ralf Jung
2018-05-25
An attempt to clarify error message for Arguments needing "rename" flag.
Hugo Herbelin
2018-05-17
Introduce an option to allow nested lemma, and turn it off by default.
Théo Zimmermann
2018-05-15
[ssr] import ssreflect test suite from math-comp
Enrico Tassi
2018-05-13
Fixing a bug in printing the body of a located notation.
Hugo Herbelin
2018-05-02
Making explicit that errors happen in one of five executation phases.
Hugo Herbelin
2018-04-09
Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...
Emilio Jesus Gallego Arias
2018-04-09
Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)
Maxime Dénès
2018-04-07
Fixes #7192 (Print Assumptions does not enter implementation of submodules).
Hugo Herbelin
2018-04-04
Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.
Hugo Herbelin
2018-04-04
ssr: check cleared hyps do exist (fix #7050)
Enrico Tassi
2018-04-02
Fix #6404 - Print tactics called by ML tactics
Jason Gross
2018-03-30
Fix #6257: anomaly with Printing Projections and Context.
Gaëtan Gilbert
2018-03-29
Fixes #7110 ("as" untested while looking for notation for nested patterns).
Hugo Herbelin
2018-03-24
Slightly refining some error messages about unresolvable evars.
Hugo Herbelin
2018-03-09
Revert "Merge PR #873: New strategy based on open scopes for deciding which n...
Maxime Dénès
2018-03-09
Merge PR #6895: [compat] Remove "Refolding Reduction" option.
Maxime Dénès
2018-03-09
Merge PR #6945: Fix error with univ binders on monomorphic records.
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
[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-04
Merge PR #6791: Removing compatibility support for versions older than 8.5.
Maxime Dénès
2018-03-02
Turn warning for deprecated notations on.
Théo Zimmermann
2018-02-28
[test-suite] Add a basic test-case for `Load`.
Emilio Jesus Gallego Arias
2018-02-28
Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...
Maxime Dénès
2018-02-24
Merge PR #6599: Decimals in prelude
Maxime Dénès
2018-02-23
Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).
Hugo Herbelin
[prev]
[next]