aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2011-05-16test-suite: no more ..._beq in the output of the search testsletouzey
2011-05-16Fix order in Search tests.letouzey
2011-05-06Fixes in the test-suite after modularisation of ZArith and coletouzey
2011-04-29Typo in test InitSyntax.outherbelin
2011-04-28Fixed notation printing bug when curly brackets are involved (requestsherbelin
2011-04-27Fixing output of Notations2.v test messed up in r14060herbelin
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
2011-04-15Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".herbelin
2011-04-08Fixing multiple printing bugs with "Notation f x := ..."herbelin
2011-03-31Did that adding a rule for printing applications as "f(x)" works.herbelin
2011-03-16Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)letouzey
2011-03-16Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extractionletouzey
2011-02-21Some fixes of the test-suite scriptsletouzey
2010-12-21Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)letouzey
2010-10-06test-suite: fix output/Existentials.outglondu
2010-10-03Test for non-regression of the display bug fixed in r13486.herbelin
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-10-03Making display of various informations about constants more modular:herbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
2010-06-04Backported r13068 to branch v8.3 (whd_betaiota on inferred returnherbelin
2010-04-18Fixed some printing bugs.herbelin
2010-04-10Optimized need for delimiters when disjoint scopes for strings andherbelin
2010-03-11Minimal test suite for search commandspuech
2010-02-13Fix NumbersSyntax.outletouzey
2010-01-29minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.tletouzey
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-12-03Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)herbelin
2009-12-02Continuing r12485-12486 and r12549 (cleaning around name generation)herbelin
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-12BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)letouzey
2009-11-12Repair interpretation of numeral for BigQ, add a printer (close #2160)letouzey
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-04-20Fix test output mentionning an existential number that changed.msozeau
2009-03-30Add tests for quoteglondu
2009-02-06Fixing #2044 (bad printing of primitive notation at the head ofherbelin
2009-01-19The initial state evar numbering increased. Fix output message in a test.puech
2009-01-13- Standardized prefix use of "Local"/"Global" modifiers as decided inherbelin
2009-01-02Regression test for bug #1967herbelin
2009-01-02Conséquence renommage canonique de refl_equal en eq_refl.herbelin
2008-12-02Miscellaneous fixes and improvements:herbelin
2008-11-27Test case for previous commit.msozeau
2008-11-09- Correction erreur dans test output Notation.vherbelin
2008-11-07- Ajout possibilité de lancer ocamldebug sur coqideherbelin
2008-10-2811511 continued (bug in set.out + incohérence dans "Theorem with"herbelin
2008-10-27- Fixed many "Theorem with" bugs.herbelin
2008-10-22Affichage des notations récursives:herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 04:02:09 +0000