aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2018-11-27[Typeclasses] Warn when RHS of `:>` is not a classVincent Laporte
This introduces the warning “not-a-class” in the “typeclasses” category.
2018-11-24Merge PR #8996: Fix #8937: inductive conversion in coqchk subtypingHugo Herbelin
2018-11-23Merge PR #8890: Looking for notation both before or after removal of top ↵Emilio Jesus Gallego Arias
coercion
2018-11-23Merge PR #8995: Don't redeclare constraints of fields in IncludeMaxime Dénès
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23Fix #8937: inductive conversion in coqchk subtypingGaëtan Gilbert
As far as I can tell this is similar to what coqtop does. Delta resolvers are complicated so I may be mistaken. The important part is to avoid losing the modified delta resolver returned by strengthen_and_subst in check_mexpr.
2018-11-22Merge PR #8967: Fix #8922 (uncaught pp_diff exception)Hugo Herbelin
2018-11-20Notations: Trying using a notation with or w/o removal of coercions.Hugo Herbelin
Preferring a notation which does require a delimiter, depending on whether the coercion is removed or not, was done for primitive tokens. We do it for all notations.
2018-11-20Merge PR #9016: PRINT_LOGS=1 in appveyor test suite runEnrico Tassi
2018-11-20Rename gh->bug_ test filesGaëtan Gilbert
2018-11-19Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.Pierre-Marie Pédrot
2018-11-19Merge PR #9001: [options] Remove deprecated option automatic introduction.Pierre-Marie Pédrot
2018-11-19Merge PR #9013: Do not Export the init modulesPierre-Marie Pédrot
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-16Print logs in appveyor test suite runGaëtan Gilbert
It seems we forgot to export when moving the script to a separate file.
2018-11-16Print Universes SubgraphGaëtan Gilbert
This adds an optional [Subgraph] part to the Print Universes command, eg [Print Universes Subgraph(i j)] to print only constraints related to i and j (and Prop/Set).
2018-11-16We improve a little bit in printing universe constraints signature mismatch.Hugo Herbelin
Use of boxes to ensure locality of formatting + use of a prlist_with_sep so that there are breaking points only inbetween the elements and not at the end of the list.
2018-11-16Add test for Include in -quick modeGaëtan Gilbert
2018-11-16Do not Export the init modulesGaëtan Gilbert
It seems we started doing the export silently in 47804492bd09c8b13b5aac45800d067dbdf04d00.
2018-11-15Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p"Vincent Laporte
2018-11-14Get hyps and goal the same way Printer does; don't omit infoJim Fehrle
Allow for new goals that don't map to old goals Include background_goals in all_goals return value Fix incorrect change to raw diffs in shorten_diff_span Fixes #8922
2018-11-14Merge PR #8966: coq_makefile: Fix ocamldep ignoring mlg filesEmilio Jesus Gallego Arias
2018-11-14ssr: add another test for elim + TCEnrico Tassi
2018-11-14ssrmatching: unify_HO does not resolve type classesEnrico Tassi
2018-11-13Merge PR #8886: [VM] Fix compilation of int31 eliminatorsMaxime Dénès
2018-11-13Merge PR #8760: Automatically generate names for universes.Pierre-Marie Pédrot
2018-11-13coq_makefile: Fix ocamldep ignoring mlg filesGaëtan Gilbert
If you have file1.mlg and file2.ml, with file2 depending on file1, ocamldep was before generating file1.ml so wouldn't generate [file2.cmx: file1.cmx] (ocamldep is silent on non-found dependencies). This has been causing nondeterministic failures in quickchick recently. I guess it didn't come up in the past because ml4 files tend to be at the end of the dependency chain.
2018-11-13Merge PR #8957: Fix -top for univbinders output test.Emilio Jesus Gallego Arias
2018-11-13Merge PR #8936: Fix #8908: incorrect refresh of algebraic universes.Pierre-Marie Pédrot
2018-11-12Automatically generate names for universes.Gaëtan Gilbert
The names are `uXXX` with `XXX` some number avoiding collision. Note that there may be some collisions with polymorphic binders, eg something like ~~~ Set Universe Polymorphism. Section foo. Universe u0. Definition bar := Type. (* bar@{u0} = Type@{u0} but this isn't the section u0 *) Definition baz := Type@{u0}. (* this one is the section u0 *) Definition foobar := Eval compute in baz -> Type. (* Type@{u0} -> Type@{u0} but these aren't the same u0 *) ~~~ So maybe we should do a nametab lookup too. This is strictly a printing issue (polymorphic binder names have no other use). In the monomorphic case names are qualified by the parent definition so it should be fine (barring module/definition collision but we already have those). Note that there are still unnamed universes as they didn't go through UState (eg schemes).
2018-11-12Do not qualify universe names by section path.Gaëtan Gilbert
2018-11-12Fix incorrect coq-prog-args in unideclsGaëtan Gilbert
2018-11-12Don't declare universe binders for variables.Gaëtan Gilbert
Otherwise ~~~ Unset Strict Universe Declaration. Section bar. Let baz := Type@{u}. Definition k := baz. End bar. Section bar. Let baz := Type@{u}. Definition k' := baz. End bar. ~~~ is broken (and has been since we stopped checking for repeated section names).
2018-11-12Merge PR #8892: Fix part of #8224: grounding open term in fixpointsPierre-Marie Pédrot
2018-11-12Test case for #4771: Substitution of inline global reference in tactics is ↵Maxime Dénès
broken
2018-11-12Fix #8908: incorrect refresh of algebraic universes.Gaëtan Gilbert
2018-11-09Fix -top for univbinders output test.Gaëtan Gilbert
It was good enough for the makefile but not for emacs.
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Add a test for bug #8939.Pierre-Marie Pédrot
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
There is little point in having a list, as there is virtually no sharing nor expansion of bound universe names. This representation is thus more compact.
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
This fixes #8791. We explicitly specify for intro the names of binders which are given by the user. This still can suffer from spurious collisions, see #8819.
2018-11-08[VM] Fix compilation of int31 eliminatorsVincent Laporte
The compilation to bytecode of the elimination schemes for int31 must happen after the int31 type is registered to the retroknowledge. Otherwise, the “decompint” instruction is not emitted.
2018-11-07Revert "Do not allow spliting in res_pf, this is reserved for pretyping"Enrico Tassi
This reverts commit 8d8200d4bff3ffc44efc51ad44dccee9eb14ec6a. Fix #7936 # Conflicts: # proofs/clenvtac.ml
2018-11-06Merge PR #8556: [ssr] use tclDISPATCH for IPatDispatch (fix #8544)Maxime Dénès
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-05Merge PR #8870: Pass native and VM flags to the kernel through environmentPierre-Marie Pédrot
2018-11-05Merge PR #8874: Fix #8873: coqchk on inductive with letin parameterPierre-Marie Pédrot
2018-11-05Merge PR #8882: Fix #8881: validate fails to use inductive equivalence in ↵Pierre-Marie Pédrot
case_info
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
The kernel no longer has to read the configure flag, its value can now be overriden by a coqtop/coqc argument, and more generally is easier to set from a toplevel (such as the checker). We also add a `-bytecode-compiler` flag. Fixes #4607
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 03:17:23 +0000