aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-24Merge pull request coq/ltac2#87 from ppedrot/camlp5-safe-api-strikes-backPierre-Marie Pédrot
Fix w.r.t. coq/coq#9051.
2018-11-24Merge PR #9022: [ci] [doc] Split user/developer README, add info about ↵Théo Zimmermann
Nix/Docker CI
2018-11-24Apply suggestions from code review Théo Zimmermann
Thanks to @Zimmi48 as always for the careful review. Co-Authored-By: ejgallego <e+git@x80.org>
2018-11-24[ci] [doc] Note about `overlay-maintainers` team.Emilio Jesus Gallego Arias
2018-11-24[ci] [doc] Note about `create-overlays.sh`Emilio Jesus Gallego Arias
2018-11-24[ci] [doc] Split user/developer README, add info about Nix/Docker CIEmilio Jesus Gallego Arias
2018-11-23Merge PR #8890: Looking for notation both before or after removal of top ↵Emilio Jesus Gallego Arias
coercion
2018-11-23Merge PR #9055: [dev] fix create_overlay wrt branch names containing /Emilio Jesus Gallego Arias
2018-11-23Merge PR #9044: Remove pidetop from CIEmilio Jesus Gallego Arias
2018-11-23Merge PR #9051: Camlp5 safe API strikes backEmilio Jesus Gallego Arias
2018-11-23Merge PR #8995: Don't redeclare constraints of fields in IncludeMaxime Dénès
2018-11-23Fix w.r.t. coq/coq#9051.Pierre-Marie Pédrot
2018-11-23Adding overlay.Pierre-Marie Pédrot
2018-11-23Remove the unsafe API from gramlib.Pierre-Marie Pédrot
2018-11-23Remove the unsafe camlp5 API from the Coq codebase.Pierre-Marie Pédrot
2018-11-23Only use Coq API in coqpp.Pierre-Marie Pédrot
2018-11-23Port Pcoq to safe camlp5 API.Pierre-Marie Pédrot
Revival of the cleaning part of #8923.
2018-11-23Overlay for private polymorphic universesGaëtan Gilbert
2018-11-23Fix 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-23Doc for Private Polymorphic Universes.Gaëtan Gilbert
2018-11-23change vernac_qed_type to have [VtKeep of vernac_keep_as]Gaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23Merge PR #9021: merge-pr: Improve overlay checkMaxime Dénès
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-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-23Goptions.declare_* functions return unit instead of a write_functionGaë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-22The usual order of strings.Yao Li
2018-11-22Merge PR #8920: Deprecate Typeclasses Axioms Are InstancesPierre-Marie Pédrot
2018-11-22[dev] fix create_overlay wrt branch names containing /Enrico Tassi
2018-11-22Merge PR #8924: Misc updates to codeownersMaxime Dénès
2018-11-22Document code owner team creation.Théo Zimmermann
2018-11-22New code owner team parsing-maintainers.Théo Zimmermann
2018-11-22New code owner team ssreflect-maintainers.Théo Zimmermann
2018-11-22It seems that Hugo is also willing to assume a maintainer role on CoqIDE.Théo Zimmermann
2018-11-22All dune files are owned by dune code owners.Théo Zimmermann
2018-11-22Disable deprecation warnings in compat files.Gaëtan Gilbert
2018-11-22Deprecate Typeclasses Axioms Are InstancesGaëtan Gilbert
People should use Declare Instance instead.
2018-11-22Merge PR #8967: Fix #8922 (uncaught pp_diff exception)Hugo Herbelin
2018-11-22Merge PR #9049: [default.nix] Add graphviz for STM DAG printerVincent Laporte
2018-11-22[default.nix] Add graphviz for STM DAG printerMaxime Dénès
2018-11-21Merge PR #8945: [camlp5] Remove dependency on camlp5.Pierre-Marie Pédrot
2018-11-21Remove pidetop from CIMaxime 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-21Merge PR #9005: More informative error on vo validation failurePierre-Marie Pédrot
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-21Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlibEnrico Tassi
2018-11-21Merge PR #8975: Minor update to micromega.rstThéo Zimmermann
2018-11-21More informative error on vo validation failureGaë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-21Add overlay for solve-remaining-evars-initial-argGaëtan Gilbert
2018-11-21Make 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-21Merge PR #8961: dune: link kernel in checker instead of copying filesPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-25 19:52:57 +0000