aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
2013-03-21Firstorder: record with defined field aren't conjonctions (fix #2629)letouzey
2013-03-21Using hnf instead of "intro H" for forcing reduction to a product.herbelin
2013-03-21Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)letouzey
2013-03-20Check a list length before doing a List.chop (fix #3000)letouzey
2013-03-18Fix for bug #3004 (thanks Hugo!)letouzey
2013-02-25Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...pboutill
2013-02-21A slightly more efficient test of well-typedness of restriction ofherbelin
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2013-02-05Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenherbelin
2013-01-29Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).herbelin
2013-01-29Added a file for testing regression of bug #2955 (anomaly in simpl inherbelin
2013-01-29Fixing bug #2969 (admit failing after Grab Existential Variables dueherbelin
2013-01-28Fixed bug #2966 (de Bruijn error in computation of heads for coercions).herbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28Fixing one part of #2830 (anomaly "defined twice" due to nested calls toherbelin
2013-01-21Fix bug 2958: Inductive deep in in clause are impossiblepboutill
2013-01-21Last test-suite not in Symmetric Patterns syntaxpboutill
2013-01-18Unset Asymmetric Patternspboutill
2012-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
2012-12-18Taking into account the possibility of having a type of type which isherbelin
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-12-04Backtrack on activating scopes with type casts (was r15978).herbelin
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
2012-11-28Evarconv: Fix #2936 + commentspboutill
2012-11-25Fixed bug #2930: folded let-in's were hiding a violation to the occurherbelin
2012-11-21Fixing test-suite: Scope.vppedrot
2012-11-18Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)herbelin
2012-11-17Update output/Search.out after hint-related extra defs in Peanoletouzey
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-10-17Fix test-suite output/* in benchpboutill
2012-09-04test-suite: fix grep rule for output testspboutill
2012-09-04test-suite uses coqtop instead of coqtop.bytepboutill
2012-08-24In the output tests, ignore dynlink messagesletouzey
2012-08-23test-suite: Local Tactic Notation is now legal since r15731letouzey
2012-08-23No more coqtop.opt, produce directly a coqtop binaryletouzey
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
2012-08-08Updating headers.herbelin
2012-07-29Fixing #2836 (materialize_evar might refine as a side effect theherbelin
2012-07-21Fixing bug #2835 (the rationale for printing notations was notherbelin
2012-07-21Improving management of notations with binders (see #2708 where aherbelin
2012-07-10Restore test file induct.v where the "in |- *" is mandatoryletouzey
2012-07-06Continuing r15459: it helps testing occur-check early in someherbelin
2012-07-06Minor fixes in the test-suite after my recent commitsletouzey
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-16 02:36:25 +0000