aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...coqbot-app[bot]
2020-11-20Merge PR #13305: Only lower inductives to Prop if the type is syntactically a...Pierre-Marie Pédrot
2020-11-20Merge PR #13360: Fix incorrect name refreshing when interning a generalized b...coqbot-app[bot]
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a primiti...coqbot-app[bot]
2020-11-20Merge PR #13371: Extend hack to use postponed constraints in retyping to temp...coqbot-app[bot]
2020-11-19Fixes #9971: expand_projections failing on primitive projections of unknown t...Hugo Herbelin
2020-11-19Merge PR #12959: Improve the bytecode interpreterPierre-Marie Pédrot
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ...coqbot-app[bot]
2020-11-18[attributes] Add output test suite for errors, improve error printing.Emilio Jesus Gallego Arias
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
2020-11-18Add more explicit tests for next_up and next_down.Pierre Roux
2020-11-18Merge PR #12765: In recursive notations, accept partial application over the ...coqbot-app[bot]
2020-11-18Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas (hopefu...Pierre-Marie Pédrot
2020-11-18In recursive notations, accept partial application over the recursive pattern.Hugo Herbelin
2020-11-17Merge PR #13390: Intern application arguments in left-to-right ordercoqbot-app[bot]
2020-11-17A reimport of notations now put the corresponding notations again in front.Hugo Herbelin
2020-11-17For printing, ordering notations by precision of the pattern.Hugo Herbelin
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
2020-11-16Fix #9569 (notations collect the spine binding variables at printing time).Hugo Herbelin
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named varia...coqbot-app[bot]
2020-11-16Fix incorrect name refreshing when interning a generalized binderGaëtan Gilbert
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context of...coqbot-app[bot]
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part of...coqbot-app[bot]
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
2020-11-16Merge PR #12685: Propagating scope information in indirect application to a r...Pierre-Marie Pédrot
2020-11-16Fix test-suite.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
2020-11-16Extend hack to use postponed constraints in retyping to template polyGaëtan Gilbert
2020-11-16Finish fixing setoid rewrite under anonymous lambdas (hopefully)Gaëtan Gilbert
2020-11-16Only lower inductives to Prop if the type is syntactically an arity.Gaëtan Gilbert
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ...coqbot-app[bot]
2020-11-15Intern application arguments in left-to-right orderGaëtan Gilbert
2020-11-15Ensuring the body of the notation in Locate is printed at level 0.Hugo Herbelin
2020-11-15Adding support for Locate "( x , y )".Hugo Herbelin
2020-11-15Fixing Locate for recursive notations with names.Hugo Herbelin
2020-11-15Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block verbati...Li-yao Xia
2020-11-15Fixes #12348: long-standing de Bruijn indices bug in imitation (solve_simple_...Hugo Herbelin
2020-11-15Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an error...coqbot-app[bot]
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handle...coqbot-app[bot]
2020-11-15Adding an output test to check that the hint commands respect their locality.Pierre-Marie Pédrot
2020-11-15Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.Hugo Herbelin
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
2020-11-15Propagating scope information in indirect application to a reference.Hugo Herbelin
2020-11-15Merge PR #13339: In -noinit mode, add support for Proof using, using is not a...Pierre-Marie Pédrot
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:11:09 +0000