aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Collapse)AuthorAge
* Merge PR #6713: Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-14
|\
| * Add test case for #6677.Gravatar Maxime Dénès2018-02-12
| |
* | Merge PR #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\ \ | |/ |/|
* | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \
* | | Add test case for #5286.Gravatar Maxime Dénès2018-01-29
| | |
| | * Support universe instances on the literal TypeGravatar Tej Chajed2018-01-26
| |/ |/| | | | | Fixes BZ#5726.
* | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \
* \ \ Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Gravatar Maxime Dénès2018-01-22
|\ \ \
| * | | Add test-suite file for issue #6617.Gravatar Cyprien Mangin2018-01-19
| | | |
* | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \ \ \ | |/ / / |/| | |
* | | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Maxime Dénès2018-01-17
|\ \ \ \
| | | * | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionGravatar Jasper Hugunin2018-01-17
| |_|/ / |/| | |
| | * | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| | * Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
| |/ |/| | | | | | | | | | | 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.
* | Merge PR #6436: Fix #5368: Canonical structure unification fails.Gravatar Maxime Dénès2017-12-18
|\ \
| * | Fix #5368: Canonical structure unification fails.Gravatar Pierre-Marie Pédrot2017-12-15
| | | | | | | | | | | | Universe instances were lost during constructions of the canonical instance.
* | | Add tactics to reset and display the Ltac profileGravatar Jason Gross2017-12-14
|/ / | | | | | | | | This is useful for tactics that run a bunch of tests and need to display the profile for each of them.
* | Merge PR #6386: Catch errors while coercing 'and' intro patternsGravatar Maxime Dénès2017-12-14
|\ \
* | | Allow LtacProf tactics to be calledGravatar Jason Gross2017-12-11
| | | | | | | | | | | | | | | | | | This fixes #6378. Previously the ML module was never declared anywhere. Thanks to @cmangin for the pointer.
| * | Catch errors while coercing 'and' intro patternsGravatar Tej Chajed2017-12-11
|/ / | | | | | | Fixes GH#6384 and GH#6385.
* | Fix #6323: stronger restrict universe context vs abstract.Gravatar Gaëtan Gilbert2017-12-06
| | | | | | | | | | | | | | | | 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].
| * Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Gaëtan Gilbert2017-12-01
| |
* | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
|/ | | | | | | | 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
* Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵Gravatar Maxime Dénès2017-11-30
|\ | | | | | | #3125)
| * In injection/inversion, consider all template-polymorphic types as injectable.Gravatar Hugo Herbelin2017-11-28
| | | | | | | | | | | | | | 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).
* | Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
| |
* | Fix #5347: unify declaration of axioms with and without bound univs.Gravatar Gaëtan Gilbert2017-11-25
| | | | | | | | | | | | | | | | | | 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).
* | Make restrict_universe_context stronger.Gravatar Gaëtan Gilbert2017-11-25
|/ | | | | | This fixes BZ#5717. Also add a test and fix a changed test.
* Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingGravatar Maxime Dénès2017-11-24
|\
* \ Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionGravatar Maxime Dénès2017-11-24
|\ \
* \ \ Merge PR #6203: Fix universe polymorphic Program obligations.Gravatar Maxime Dénès2017-11-23
|\ \ \
| | * | Recognizing Z in romega up to conversion.Gravatar Hugo Herbelin2017-11-23
| | | |
| | * | Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Gravatar Hugo Herbelin2017-11-23
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
| | * Fixing a 8.7 regression of ring_simplify in ArithRing.Gravatar Hugo Herbelin2017-11-23
| |/ |/| | | | | | | With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191).
* | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Maxime Dénès2017-11-23
|\ \
| | * Fix universe polymorphic Program obligations.Gravatar Matthieu Sozeau2017-11-22
| |/ |/| | | | | | | | | The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments.
* | Merge PR #6166: Fix regression in treating Defined as definedGravatar Maxime Dénès2017-11-20
|\ \
* \ \ Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ | | | | | | | | | | | | (clause "where" with implicit arguments)
* \ \ \ Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ | | | | | | | | | | | | | | | unbound rel
| | | | * Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Gaëtan Gilbert2017-11-19
| |_|_|/ |/| | |
| | | * Fix regression in treating Defined as definedGravatar Tej Chajed2017-11-15
| | | | | | | | | | | | | | | | Fixes #6165.
| * | | Fix #5761: cbv on undefined evars under binders produces unbound relGravatar Gaëtan Gilbert2017-11-15
| | |/ | |/| | | | | | | | | | | | | | | | When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case.
* / | Fixes #6129 (declaration of coercions made compatible with local definitions).Gravatar Hugo Herbelin2017-11-14
|/ /
| * One more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2017-11-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not.
* | Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Maxime Dénès2017-11-13
|\ \ | |/ |/|
* | Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵Gravatar Maxime Dénès2017-11-06
|\ \ | | | | | | | | | alphabet).
* \ \ Merge PR #1139: Add a linter.Gravatar Maxime Dénès2017-11-06
|\ \ \
| | * | Refining PR#924 (insensitivity of projection heuristics to alphabet).Gravatar Hugo Herbelin2017-11-05
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed).
| | * Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Hugo Herbelin2017-11-04
| |/ |/| | | | | Adding a file fixing #5996 and which uses this feature.
* | Merge PR #6047: A generic printer for ltac valuesGravatar Maxime Dénès2017-11-03
|\ \