aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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
2008-08-05Correction de bugs:herbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-29Oops... the trunk behaviour is differentglondu
2008-07-29Update test-suite outputglondu
2008-07-01Documentation Prop<=Set et Arguments Scope Globalherbelin
2008-06-05Renommage id dans le test Nametab (suite ajout d'une constante de ceherbelin
2008-04-28Petites corrections vis à vis des commits 10860, 10859, 10850herbelin
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-03-26Diverses petites modifs dans la test-suite:notin
2008-03-25Correction de bugs relatifs a la compostion des substitutionssoubiran
2008-03-08Fix bugs that were reopened due to the change of setoidmsozeau
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2008-01-22Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)notin
2007-10-05Correction de quelques défauts d'affichage (notations sous "as" pourherbelin
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
2007-07-23removed thesisbarras
2007-07-12Update (test-suite was not successful).glondu
2007-07-02Factorisation des paramètres dans l'affichage des inductifsherbelin
2007-05-10Prise en compte réversibilité des notations de la forme "Notation Nil := @n...herbelin
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-04-13Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantherbelin
2006-12-12MAJherbelin
2006-10-13Correction test-suite suite à r9186notin
2006-10-09Exemple avec liaison des variables de filtrage du matchherbelin
2006-10-09Notations:herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:06:05 +0000