aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2018-03-05Sanitize universe declaration in Context (stop using a ref...)Gaëtan Gilbert
When there is more than one variable to declare we stop trying to attach global universes (ie monomorphic or section polymorphic) to one of them.
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04ssr: add Prenex Implicits for Some_inj to use it as a viewAnton Trunov
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-03Removing test for bug #2850.Pierre-Marie Pédrot
This test was actually checking that evar-containing terms were making the VM fail. Obviously this is not the case anymore, so the test is now invalid.
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
Following up on #6791, we remove the option "Standard Proposition Elimination"
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-02-24Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Maxime Dénès
2018-02-21Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Maxime Dénès
2018-02-21Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Maxime Dénès
2018-02-21Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just ↵Maxime Dénès
the concl
2018-02-20Fixes bug #6774 (anomaly with ill-typed template polymorphism).Hugo Herbelin
Computation of the sort of the inductive type was done before ensuring that the arguments of the inductive type had the correct types, possibly brutally failing with `NotArity` in case one of the types expected to be typed with an arity was not so.
2018-02-20Adding a test for wish #5532.Hugo Herbelin
2018-02-19Fix #6529: nf_evar_info and check the env evars' not just the conclMatthieu Sozeau
2018-02-14Extend `zify_N` with knowledge about `N.pred`Joachim Breitner
by doing the same thing as `zify_nat` does for `nat.pred`. This fixes #6602.
2018-02-14Merge PR #6713: Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-12Add test case for #6677.Maxime Dénès
2018-02-12Merge PR #1047: Support universe instances on the literal TypeMaxime Dénès
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-29Add test case for #5286.Maxime Dénès
2018-01-26Support universe instances on the literal TypeTej Chajed
Fixes BZ#5726.
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-22Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Maxime Dénès
2018-01-19Add test-suite file for issue #6617.Cyprien Mangin
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-17Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Maxime Dénès
2018-01-17Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionJasper Hugunin
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt).
2018-01-02Cleanup name-binding structure for fresh evar name generation.Pierre-Marie Pédrot
We simply use a record and pack the rel and var substitutions in it. We also properly compose variable substitutions. Fixes #6534: Fresh variable generation in case of clash is buggy.
2017-12-18Merge PR #6436: Fix #5368: Canonical structure unification fails.Maxime Dénès
2017-12-15Fix #5368: Canonical structure unification fails.Pierre-Marie Pédrot
Universe instances were lost during constructions of the canonical instance.
2017-12-14Add tactics to reset and display the Ltac profileJason Gross
This is useful for tactics that run a bunch of tests and need to display the profile for each of them.
2017-12-14Merge PR #6386: Catch errors while coercing 'and' intro patternsMaxime Dénès
2017-12-11Allow LtacProf tactics to be calledJason Gross
This fixes #6378. Previously the ML module was never declared anywhere. Thanks to @cmangin for the pointer.
2017-12-11Catch errors while coercing 'and' intro patternsTej Chajed
Fixes GH#6384 and GH#6385.
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c].
2017-12-01Fix #6297: handle constraints like (u+1 <= Set/Prop)Gaëtan Gilbert
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
2017-11-30Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵Maxime Dénès
#3125)
2017-11-28In injection/inversion, consider all template-polymorphic types as injectable.Hugo Herbelin
In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273).
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-25Fix #5347: unify declaration of axioms with and without bound univs.Gaëtan Gilbert
Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list).
2017-11-25Make restrict_universe_context stronger.Gaëtan Gilbert
This fixes BZ#5717. Also add a test and fix a changed test.
2017-11-24Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingMaxime Dénès
2017-11-24Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionMaxime Dénès
2017-11-23Merge PR #6203: Fix universe polymorphic Program obligations.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 12:05:27 +0000