| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-17 | Merge PR #8992: put protocol/ in ide/.merlin | Pierre-Marie Pédrot | |
| 2018-11-17 | Merge PR #8914: [CoqProject] Abstract warning function for CoqProject readers. | Pierre-Marie Pédrot | |
| 2018-11-17 | Merge PR #8968: Miscellaneous CoqIDE fixes | Pierre-Marie Pédrot | |
| 2018-11-17 | [CoqProject] Abstract warning function for CoqProject readers. | Emilio Jesus Gallego Arias | |
| `CoqProject_file` uses the feedback system, however this is not very convenient in some scenarios such as `coqdep` that has to be run very early in the build process [and thus in "boot" mode]. We thus make the warning function a paramater. Should fix #8913. | |||
| 2018-11-16 | Merge PR #8779: Remove the implicit tactic feature following #7229. | Matthieu Sozeau | |
| 2018-11-16 | Merge PR #8781: Remove primproj <-> constant dependency in Heads | Pierre-Marie Pédrot | |
| 2018-11-16 | put protocol/ in ide/.merlin | Gaëtan Gilbert | |
| 2018-11-16 | No Projection.constant in projection <-> constant declaration | Gaëtan Gilbert | |
| Enabled by previous commit about Heads. | |||
| 2018-11-16 | Heads: simplify using that projections are always rigid | Gaëtan Gilbert | |
| This avoids using Projection.constant in kind_of_head, which then allows compute_head to not check whether the constant is a compatibility definition (as in that case its body is [fun ... => x.(p)]). Thus Heads stops caring about the compatibility projection system. | |||
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-16 | Merge PR #8888: Proof runcountable rebase | Hugo Herbelin | |
| 2018-11-15 | Merge PR #8991: coqide: use correct toplevel name in files | Emilio Jesus Gallego Arias | |
| 2018-11-15 | Move generating library dirpath to stm in compile mode. | Gaëtan Gilbert | |
| 2018-11-15 | coqide: use correct toplevel name in files | Gaë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-15 | Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p" | Vincent Laporte | |
| 2018-11-14 | Merge PR #8966: coq_makefile: Fix ocamldep ignoring mlg files | Emilio Jesus Gallego Arias | |
| 2018-11-14 | ssr: add another test for elim + TC | Enrico Tassi | |
| 2018-11-14 | ssr: rewrite: do resolve TC once and forall at the very end | Enrico Tassi | |
| 2018-11-14 | ssr: elim: do resolve TC once and forall at the very end | Enrico Tassi | |
| 2018-11-14 | ssrcommon: API to call resolve_tyclasses on a term | Enrico Tassi | |
| 2018-11-14 | ssrmatching: unify_HO does not resolve type classes | Enrico Tassi | |
| 2018-11-13 | Merge PR #8886: [VM] Fix compilation of int31 eliminators | Maxime Dénès | |
| 2018-11-13 | Merge PR #8906: [Goptions] More detailed error messages | Maxime Dénès | |
| 2018-11-13 | Merge PR #8760: Automatically generate names for universes. | Pierre-Marie Pédrot | |
| 2018-11-13 | coq_makefile: Fix ocamldep ignoring mlg files | Gaë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-13 | Merge PR #8976: CoqHammer CI | Gaëtan Gilbert | |
| 2018-11-13 | Merge PR #8957: Fix -top for univbinders output test. | Emilio Jesus Gallego Arias | |
| 2018-11-13 | Merge 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-13 | Merge PR #8978: nix helpers for debugging external projects from CI | Emilio Jesus Gallego Arias | |
| 2018-11-13 | Merge PR #8936: Fix #8908: incorrect refresh of algebraic universes. | Pierre-Marie Pédrot | |
| 2018-11-12 | Merge PR #8979: Skip submodules in HoTT CI script. | Emilio Jesus Gallego Arias | |
| 2018-11-12 | Merge PR #8960: [dune] Build `cmxs` files instead of `cmxa` in "quick" target. | Enrico Tassi | |
| 2018-11-12 | Skip submodules in HoTT CI script. | Gaëtan Gilbert | |
| Avoid downloading Coq. | |||
| 2018-11-12 | Automatically 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-12 | Do not qualify universe names by section path. | Gaëtan Gilbert | |
| 2018-11-12 | Fix incorrect coq-prog-args in unidecls | Gaëtan Gilbert | |
| 2018-11-12 | Don'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-12 | Only declare univ binders once for mutind | Gaëtan Gilbert | |
| 2018-11-12 | Merge PR #8962: [ci] Add paramcoq to CI. | Gaëtan Gilbert | |
| 2018-11-12 | Merge PR #8892: Fix part of #8224: grounding open term in fixpoints | Pierre-Marie Pédrot | |
| 2018-11-12 | Merge PR #8972: Fix #4771: Substitution of inline global reference in ↵ | Pierre-Marie Pédrot | |
| tactics is broken | |||
| 2018-11-12 | CoqHammer CI | Lukasz Czajka | |
| 2018-11-12 | Set codeowners for dev/ci/nix | Vincent Laporte | |
| 2018-11-12 | Helpers for debugging external projects from CI | Vincent Laporte | |
| 2018-11-12 | Merge PR #8938: [Plugins] Remove some dead code | Pierre-Marie Pédrot | |
| 2018-11-12 | Merge PR #8958: [clib] Remove unneeded `get_extension` function. | Pierre-Marie Pédrot | |
| 2018-11-12 | Test case for #4771: Substitution of inline global reference in tactics is ↵ | Maxime Dénès | |
| broken | |||
| 2018-11-12 | Fix #4771: Substitution of inline global reference in tactics is broken | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |