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
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).
herbelin
2010-06-18
*
Added printing of recursive notations in cases pattern (supported by wish 2248).
herbelin
2010-06-14
*
Backported r13068 to branch v8.3 (whd_betaiota on inferred return
herbelin
2010-06-04
*
Fixed some printing bugs.
herbelin
2010-04-18
*
Optimized need for delimiters when disjoint scopes for strings and
herbelin
2010-04-10
*
Minimal test suite for search commands
puech
2010-03-11
*
Fix NumbersSyntax.out
letouzey
2010-02-13
*
minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.t
letouzey
2010-01-29
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)
herbelin
2009-12-03
*
Continuing r12485-12486 and r12549 (cleaning around name generation)
herbelin
2009-12-02
*
Continuing r12485-12486 (cleaning around name generation)
herbelin
2009-12-01
*
BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)
letouzey
2009-11-12
*
Repair interpretation of numeral for BigQ, add a printer (close #2160)
letouzey
2009-11-12
*
Improving abbreviations/notations + backtrack of semantic change in r12439
herbelin
2009-11-11
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Fixing #2090 (occur check missing when trying to solve evar-evar equation).
herbelin
2009-04-25
*
Fix test output mentionning an existential number that changed.
msozeau
2009-04-20
*
Add tests for quote
glondu
2009-03-30
*
Fixing #2044 (bad printing of primitive notation at the head of
herbelin
2009-02-06
*
The initial state evar numbering increased. Fix output message in a test.
puech
2009-01-19
*
- Standardized prefix use of "Local"/"Global" modifiers as decided in
herbelin
2009-01-13
*
Regression test for bug #1967
herbelin
2009-01-02
*
Conséquence renommage canonique de refl_equal en eq_refl.
herbelin
2009-01-02
*
Miscellaneous fixes and improvements:
herbelin
2008-12-02
*
Test case for previous commit.
msozeau
2008-11-27
*
- Correction erreur dans test output Notation.v
herbelin
2008-11-09
*
- Ajout possibilité de lancer ocamldebug sur coqide
herbelin
2008-11-07
*
11511 continued (bug in set.out + incohérence dans "Theorem with"
herbelin
2008-10-28
*
- Fixed many "Theorem with" bugs.
herbelin
2008-10-27
*
Affichage des notations récursives:
herbelin
2008-10-22
*
Correction de bugs:
herbelin
2008-08-05
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Oops... the trunk behaviour is different
glondu
2008-07-29
*
Update test-suite output
glondu
2008-07-29
*
Documentation Prop<=Set et Arguments Scope Global
herbelin
2008-07-01
*
Renommage id dans le test Nametab (suite ajout d'une constante de ce
herbelin
2008-06-05
*
Petites corrections vis à vis des commits 10860, 10859, 10850
herbelin
2008-04-28
*
Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
herbelin
2008-04-25
*
Diverses petites modifs dans la test-suite:
notin
2008-03-26
*
Correction de bugs relatifs a la compostion des substitutions
soubiran
2008-03-25
*
Fix bugs that were reopened due to the change of setoid
msozeau
2008-03-08
*
Beaoucoup de changements dans la representation interne des modules.
soubiran
2008-02-01
*
Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)
notin
2008-01-22
*
Correction de quelques défauts d'affichage (notations sous "as" pour
herbelin
2007-10-05
*
- Fixing bug 1703 ("intros until n" falls back on the variable name when
herbelin
2007-09-21
*
removed thesis
barras
2007-07-23
*
Update (test-suite was not successful).
glondu
2007-07-12
*
Factorisation des paramètres dans l'affichage des inductifs
herbelin
2007-07-02
[next]