| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-23 | Overlay for private polymorphic universes | Gaëtan Gilbert | |
| 2018-11-23 | Fix printing of private universes. | Gaëtan Gilbert | |
| Set Printing Universes. Set Universe Polymorphism. Lemma foo : Type. Proof. exact (forall _ : Type, Type). Qed. Print foo. Before: (* foo@{Top.1} = Type@{Top.2} -> Type@{Top.3} : Type@{Top.1} (* Top.1 |= Prop < Set Set < Top.1 local: {Top.3 Top.2} |= Top.2 < Top.1 Top.3 < Top.1 *) foo is universe polymorphic *) Now: (* Public universes: Top.1 |= Set < Top.1 Private universes: {Top.3 Top.2} |= Top.2 < Top.1 Top.3 < Top.1 *) | |||
| 2018-11-23 | Doc for Private Polymorphic Universes. | Gaëtan Gilbert | |
| 2018-11-23 | change vernac_qed_type to have [VtKeep of vernac_keep_as] | Gaëtan Gilbert | |
| 2018-11-23 | Local universes for opaque polymorphic constants. | Gaëtan Gilbert | |
| 2018-11-23 | Merge PR #9021: merge-pr: Improve overlay check | Maxime Dénès | |
| 2018-11-23 | Fix #8937: inductive conversion in coqchk subtyping | Gaë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-23 | s/let _ =/let () =/ in some places (mostly goptions related) | Gaëtan Gilbert | |
| 2018-11-23 | Goptions.declare_* functions return unit instead of a write_function | Gaëtan Gilbert | |
| Returning a writer insinuates that it is not exactly the same as the writer which was passed as argument, but that is incorrect. | |||
| 2018-11-22 | The usual order of strings. | Yao Li | |
| 2018-11-22 | Merge PR #8920: Deprecate Typeclasses Axioms Are Instances | Pierre-Marie Pédrot | |
| 2018-11-22 | [dev] fix create_overlay wrt branch names containing / | Enrico Tassi | |
| 2018-11-22 | Merge PR #8924: Misc updates to codeowners | Maxime Dénès | |
| 2018-11-22 | Document code owner team creation. | Théo Zimmermann | |
| 2018-11-22 | New code owner team parsing-maintainers. | Théo Zimmermann | |
| 2018-11-22 | New code owner team ssreflect-maintainers. | Théo Zimmermann | |
| 2018-11-22 | It seems that Hugo is also willing to assume a maintainer role on CoqIDE. | Théo Zimmermann | |
| 2018-11-22 | All dune files are owned by dune code owners. | Théo Zimmermann | |
| 2018-11-22 | Disable deprecation warnings in compat files. | Gaëtan Gilbert | |
| 2018-11-22 | Deprecate Typeclasses Axioms Are Instances | Gaëtan Gilbert | |
| People should use Declare Instance instead. | |||
| 2018-11-22 | Merge PR #8967: Fix #8922 (uncaught pp_diff exception) | Hugo Herbelin | |
| 2018-11-22 | Merge PR #9049: [default.nix] Add graphviz for STM DAG printer | Vincent Laporte | |
| 2018-11-22 | [default.nix] Add graphviz for STM DAG printer | Maxime Dénès | |
| 2018-11-21 | Merge PR #8945: [camlp5] Remove dependency on camlp5. | Pierre-Marie Pédrot | |
| 2018-11-21 | Remove pidetop from CI | Maxime Dénès | |
| pidetop relies on some rather low level API from STM, which we'd like to change. It does not seem maintained much anymore, and still hasn't moved to github. | |||
| 2018-11-21 | Merge PR #9005: More informative error on vo validation failure | Pierre-Marie Pédrot | |
| 2018-11-21 | [camlp5] Remove dependency on camlp5. | Emilio Jesus Gallego Arias | |
| 2018-11-21 | Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlib | Enrico Tassi | |
| 2018-11-21 | Merge PR #8975: Minor update to micromega.rst | Théo Zimmermann | |
| 2018-11-21 | More informative error on vo validation failure | Gaëtan Gilbert | |
| Now that the checker shares code with the kernel using md5 cic.mli doesn't work. We could md5 declarations.ml but this would miss changes to constr (and cic.mli already missed changes to names, univs). Instead we just print a bit of information (the last seen type name/annotation) when validate fails. This should help debugging when forgetting to update values.ml without the full verbosity of -debug. As such there is no need to -debug in the makefile validate target (NB: CI has an independent implementation of the validate rule since the vos are installed there). | |||
| 2018-11-21 | Add overlay for solve-remaining-evars-initial-arg | Gaëtan Gilbert | |
| 2018-11-21 | Make initial evar map argument to check_evars_are_solved optional. | Gaëtan Gilbert | |
| (same for solve_remaining_evars) This is the standard way to use these functions, with 1 exception in Unification. | |||
| 2018-11-21 | Merge PR #8961: dune: link kernel in checker instead of copying files | Pierre-Marie Pédrot | |
| 2018-11-21 | Merge PR #8998: [legacy proof engine] Remove some cruft. | Pierre-Marie Pédrot | |
| 2018-11-21 | [sphinx] Progress towards closing #7602: remove most objects without a body. | Théo Zimmermann | |
| Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter. | |||
| 2018-11-21 | [legacy proof engine] Remove some cruft. | Emilio Jesus Gallego Arias | |
| We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps. | |||
| 2018-11-21 | [gramlib] [build] Switch make-based system to packed gramlib | Emilio Jesus Gallego Arias | |
| This makes the make-based build system stop linking to Camlp5's gramlib and instead links to our own gramlib. We use the style done in the packing of `Stdlib` in OCaml 4.07. As to introduce a minimal amount of noise in history we use an autogenerated `gramlib__pack` directory. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2018-11-20 | Merge PR #8948: [dune] Some tweaks to docs. | Théo Zimmermann | |
| 2018-11-20 | Merge PR #9035: [dune] Only build printers when the ltac plugin is available. | Théo Zimmermann | |
| 2018-11-20 | [dune] Only build printers when the ltac plugin is available. | Emilio Jesus Gallego Arias | |
| This fixes a problem reported by @Zimmi48 in #8948, IMHO we should be able to have a clean build of core Coq. | |||
| 2018-11-20 | Merge PR #8959: [dune] [ide] Install data files. | Enrico Tassi | |
| 2018-11-20 | Notations: 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-20 | Merge PR #9016: PRINT_LOGS=1 in appveyor test suite run | Enrico Tassi | |
| 2018-11-20 | Merge PR #9017: Remove SSR profiling | Enrico Tassi | |
| 2018-11-20 | Merge PR #9033: gitlab: Install stdlib doc in build:base | Emilio Jesus Gallego Arias | |
| 2018-11-20 | Add a check that the return stack of an FProd is indeed empty. | Pierre-Marie Pédrot | |
| 2018-11-20 | Use a closure for the domain argument of FProd. | Pierre-Marie Pédrot | |
| The use of a term is not needed for the fast typing algorithm of the application case, so this tweak brings the best of both worlds. | |||
| 2018-11-20 | More efficient implementation of type_of_apply. | Pierre-Marie Pédrot | |
| 2018-11-20 | Do not wrap FProd return types in a closure. | Pierre-Marie Pédrot | |
| There is little point to this as the type is dependent on an open value and is never computed further. | |||
| 2018-11-20 | gitlab: Install stdlib doc in build:base | Gaëtan Gilbert | |
| Looks like we forgot to adapt this when we split off the sphinx job and stopped using -with-doc yes. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |