index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
output
Commit message (
Expand
)
Author
Age
*
Adapted test file for About.
Pierre Courtieu
2014-12-15
*
About now accepts hypothesis names and goal selector.
Pierre Courtieu
2014-12-15
*
Tests for Searchxxx commands added and modified.
Pierre Courtieu
2014-12-15
*
Adapting output tests to current naming of evars, even if unclear
Hugo Herbelin
2014-11-11
*
Consequence of changing the definition of Nat.shiftl and Nat.shiftr.
Hugo Herbelin
2014-11-06
*
Fixing clash in output test-suite Cases.
Hugo Herbelin
2014-10-23
*
Taking into account factorization of consecutive names of same types
Hugo Herbelin
2014-10-23
*
Fixing typo in output test Notations.
Hugo Herbelin
2014-10-22
*
Adapting output tests to the removal of the new token warning and to
Hugo Herbelin
2014-10-21
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Adapting output/Arguments_renaming continued.
Hugo Herbelin
2014-10-03
*
An evar name changed in output test.
Hugo Herbelin
2014-10-02
*
Adapting the output test Notations:
Hugo Herbelin
2014-10-02
*
Revert "test-suite: New names for vars but the expected invariant is preserved"
Hugo Herbelin
2014-10-02
*
Adapting output/Arguments_renaming.out after fixing printing of
Hugo Herbelin
2014-10-02
*
Adapting to naming of evars.
Hugo Herbelin
2014-09-27
*
Reductionops: (Co)Fixpoints are always refolded during iota
Pierre Boutillier
2014-09-18
*
Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.
Hugo Herbelin
2014-09-15
*
Grammar: "avoiding to" isn't proper, either
Jason Gross
2014-08-25
*
Upgrading output tests.
Hugo Herbelin
2014-08-12
*
Fixing output test-suite.
Pierre-Marie Pédrot
2014-07-21
*
cbn understand ! Arguments directive
Pierre Boutillier
2014-06-04
*
Fixing output test-suite: since universe polymorphism, the Print command
Pierre-Marie Pédrot
2014-05-08
*
Fixing #3293 (eta-expansion at "match" printing time was failing
Hugo Herbelin
2014-04-28
*
Never suppress the typing constraint of bound variables whose name was
Pierre-Marie Pédrot
2014-03-01
*
test-suite: opaque term -> opaque proof
Pierre Boutillier
2014-02-28
*
test-suite: New names for vars but the expected invariant is preserved
Pierre Boutillier
2014-02-28
*
Fix output test-suite 'simpl tactic' -> 'reduction tactics'
Pierre Boutillier
2014-02-28
*
test-suite/output/Notations : evar number change
Pierre Boutillier
2013-12-19
*
Test suite: update output reference.
xclerc
2013-12-02
*
Print logical name rather than path (thus allowing reproducible tests).
xclerc
2013-12-02
*
test-suite fixup
pboutill
2013-11-03
*
Fixing 2 output test-suites.
ppedrot
2013-10-08
*
Fixing some tests from the test-suite.
ppedrot
2013-09-03
*
Fix testsuite so that it works with STM
gareuselesinge
2013-08-08
*
better error message for unexpected renaming (closes #2987)
gareuselesinge
2013-07-29
*
Updating some output tests in test-suite:
herbelin
2013-05-09
*
Renaming SearchAbout into Search and Search into SearchHead.
herbelin
2013-04-17
*
Using Parameter instead of Variable in test-suite/output
herbelin
2013-04-17
*
Continuation of r16346 on filtering local definitions. Refined
herbelin
2013-03-30
*
Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...
pboutill
2013-02-25
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Fixing parsing of specific primitive tokens used as notations for patterns
herbelin
2012-12-18
*
Revised the strategy for automatic insertion of spaces when printing
herbelin
2012-12-04
*
Update output/Search.out after hint-related extra defs in Peano
letouzey
2012-11-17
*
Fixing bug #2835 (the rationale for printing notations was not
herbelin
2012-07-21
*
Minor fixes in the test-suite after my recent commits
letouzey
2012-07-06
*
Constrextern is allow to use partially applied notations
pboutill
2012-06-14
[next]