| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-17 | Merge PR #8712: [stm] avoid unshare safe env to detect correctly env ↵ | Maxime Dénès | |
| changing tactics | |||
| 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 | Make set_typing_flags "smart" | Gaëtan Gilbert | |
| Fix #8609 gares said: I believe it was introduced in de20a45 where the option (part of the summary) is moved to the save env. By setting the summary, you unshare the safe env. Now we do that only if needed. The stm uses `==` on the safe env to detect tactics that alter the env, eg abstract. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |