aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2010-10-05test-suite: fix success/AdvancedCanonicalStructure.vglondu
2010-10-05Export definition of type implicits_list for contribs + fixed aherbelin
2010-10-05test-suite: use unified diff output and use expected output as referenceglondu
2010-10-04Fixing bugs in previous commits about implicit arguments:herbelin
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-09-30Improve handling of metas as evars in unification (patch by Hugo)letouzey
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
2010-09-20Fixed test of bug #2360 (use of Fail to check a regular error insteadherbelin
2010-09-19Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weherbelin
2010-09-18Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inherbelin
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-09-17Fixed a problem introduced in r12607 after pattern_of_constr servedherbelin
2010-09-17In the computation of missing arguments for apply, accept that theherbelin
2010-09-11Improving a few error messages in Ltac interpretationherbelin
2010-09-02fixed bug #2375 (congruence)corbinea
2010-07-30Updated test on Nsatz after Loïc moved NsatzR to Nsatz.herbelin
2010-07-29test-case for bug #2105barras
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
2010-07-28fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesbarras
2010-07-27nstaz pour les anneaux integres et les setoides, R Z et Qpottier
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-21Backporting fix to bug #2353 (fixpoint with recursively non-uniformherbelin
2010-07-21Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).herbelin
2010-07-12Fix compilation and test-suite of nsatzglondu
2010-07-08nsatz in an integral domain with specialization to Z and Rpottier
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-26Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.herbelin
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
2010-06-20Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)letouzey
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
2010-06-18add in test-suite the scripts about fsetdec bugsletouzey
2010-06-16test for bug #2141 (include + extraction)letouzey
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
2010-06-13Fixing bug 2295 (omission of option "as" in return clause of "match" was notherbelin
2010-06-13Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).herbelin
2010-06-13Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withherbelin
2010-06-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
2010-06-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
2010-06-12Added regression tests for bugs + miscellaneous improvementsherbelin
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
2010-06-09Fixed bug # 2303 in r 13087.msozeau
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
2010-06-09Automatic introduction of names given before ":" in Lemma's andherbelin
2010-06-09Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.herbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 18:06:09 +0000