aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-16Fix lifting in foo_with_full_binders for (co)fixpointsGaëtan Gilbert
2018-11-16Small simplification in fold_constr_with_bindersGaëtan Gilbert
2018-11-16Merge PR #8888: Proof runcountable rebaseHugo Herbelin
2018-11-15Merge PR #8991: coqide: use correct toplevel name in filesEmilio Jesus Gallego Arias
2018-11-15Move generating library dirpath to stm in compile mode.Gaëtan Gilbert
2018-11-15coqide: use correct toplevel name in filesGaëtan Gilbert
Fix #8989. This adds an option -topfile taking a path so that inferring the right dirpath is done by the toplevel after processing -Q/-R instead of the client having to do it.
2018-11-15Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p"Vincent Laporte
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-14ssr: rewrite: do resolve TC once and forall at the very endEnrico Tassi
2018-11-14ssr: elim: do resolve TC once and forall at the very endEnrico Tassi
2018-11-14ssrcommon: API to call resolve_tyclasses on a termEnrico 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 #8906: [Goptions] More detailed error messagesMaxime 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 #8976: CoqHammer CIGaëtan Gilbert
2018-11-13Merge PR #8957: Fix -top for univbinders output test.Emilio Jesus Gallego Arias
2018-11-13Merge PR #8919: [vernac] Rename Vernacinterp to Vernacextend and move ↵Pierre-Marie Pédrot
extension functions there
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API.
2018-11-13[configure] Remove grammar and dev from core_src_dirs.Emilio Jesus Gallego Arias
These directories don't contain Coq sources but internal developer files. This can create problems, for example, in #8919.
2018-11-13Merge PR #8978: nix helpers for debugging external projects from CIEmilio Jesus Gallego Arias
2018-11-13Merge PR #8936: Fix #8908: incorrect refresh of algebraic universes.Pierre-Marie Pédrot
2018-11-12Merge PR #8979: Skip submodules in HoTT CI script.Emilio Jesus Gallego Arias
2018-11-12Merge PR #8960: [dune] Build `cmxs` files instead of `cmxa` in "quick" target.Enrico Tassi
2018-11-12Skip submodules in HoTT CI script.Gaëtan Gilbert
Avoid downloading Coq.
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-12Only declare univ binders once for mutindGaëtan Gilbert
2018-11-12Merge PR #8962: [ci] Add paramcoq to CI.Gaëtan Gilbert
2018-11-12Merge PR #8892: Fix part of #8224: grounding open term in fixpointsPierre-Marie Pédrot
2018-11-12Merge PR #8972: Fix #4771: Substitution of inline global reference in ↵Pierre-Marie Pédrot
tactics is broken
2018-11-12CoqHammer CILukasz Czajka
2018-11-12Set codeowners for dev/ci/nixVincent Laporte
2018-11-12Helpers for debugging external projects from CIVincent Laporte
2018-11-12Merge PR #8938: [Plugins] Remove some dead codePierre-Marie Pédrot
2018-11-12Merge PR #8958: [clib] Remove unneeded `get_extension` function.Pierre-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 #4771: Substitution of inline global reference in tactics is brokenMaxime Dénès
2018-11-12Fix #8908: incorrect refresh of algebraic universes.Gaëtan Gilbert
2018-11-12[clib] Remove unneeded `get_extension` function.Emilio Jesus Gallego Arias
This has been in OCaml since 4.04.
2018-11-11Merge PR #8795: Encapsulating declarations of primitive string syntax in a ↵Jason Gross
module
2018-11-10[ci] Add paramcoq to CI.Emilio Jesus Gallego Arias
2018-11-09Merge PR #8949: Remove checker printersEmilio Jesus Gallego Arias
2018-11-09Merge PR #8956: Fix dune runtest invocationEmilio Jesus Gallego Arias
2018-11-09[dune] Build `cmxs` files instead of `cmxa` in "quick" target.Emilio Jesus Gallego Arias
This fixes #8954
2018-11-09Fix -top for univbinders output test.Gaëtan Gilbert
It was good enough for the makefile but not for emacs.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:28:08 +0000