aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-07-08Make local nonterminal definitions unique when necessaryJim Fehrle
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive ↵Enrico Tassi
projection Reviewed-by: ejgallego Ack-by: gares
2020-07-08Merge PR #12612: docs(README.md): Update badge and linksEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-08Merge PR #12654: Reindent ppvernac.mlEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-08Merge PR #12645: Cleanup Evarutil APIEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-07-08Merge PR #12652: Fix erroneous implicits-in-term warningEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_from_context from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_pure_evar_full from the API.Pierre-Marie Pédrot
2020-07-08Small code simplification in Evarutil.new_evar.Pierre-Marie Pédrot
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-07Reindent ppvernac.mlGaëtan Gilbert
It used to be a big functor but changed in 8c5adfd5acb883a3bc2850b6fc8c29d352a421f8 The functor indent is now incorrect.
2020-07-07Fix erroneous implicits-in-term warningGaëtan Gilbert
Fix #12651
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: proux01 Ack-by: silene
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-06Merge PR #12622: Use goal cycling instead of manual evar generation order in ↵Gaëtan Gilbert
internal_cut_rev Reviewed-by: SkySkimmer
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
Perhaps we should thread an evar map with the Var universes added through to cs_pattern_of_constr but that would be significantly more invasive. Fix #12528
2020-07-05Merge PR #12641: Windows build: use architecture dependent version of windresEnrico Tassi
Reviewed-by: gares
2020-07-05Merge PR #12594: Fix ltac2 type parametersMichael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: gares
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-04Windows build: remove patch for windres architectureMichael Soegtrop
2020-07-04Windows build: use architecture dependent version of windresMichael Soegtrop
2020-07-03Merge PR #12523: Fix #11121: Simultaneous definition of term and notation in ↵Gaëtan Gilbert
custom gr… Reviewed-by: SkySkimmer Ack-by: ejgallego Ack-by: herbelin
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
2020-07-02Merge PR #12628: Fix debug printer for auctx in presence of AnonymousEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-02Merge PR #12614: Cleanup mentions of -as in coqdep usage messageEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-02Fix debug printer for auctx in presence of AnonymousGaëtan Gilbert
2020-07-02Fix Context with nonmaximplicit.Gaëtan Gilbert
Fix #12551
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet ↵Gaëtan Gilbert
patterns. Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2020-07-02Merge PR #12620: [state] Consolidate state handling into VernacstateGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-07-02Merge PR #12618: Use weak ref to memoize Evarutil.is_ground_envPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-01Use goal cycling instead of manual evar generation order in internal_cut_rev.Pierre-Marie Pédrot
This reduces the combinatorial complexity of the function, and the code size as well.
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
After #12504 , we can encapsulate and consolidate low-level state logic in `Vernacstate`, removing `States` which is now a stub. There is hope to clean up some stuff regarding the handling of low-level proof state, by moving both `Evarutil.meta_counter` and `Evd.evar_counter_summary` into the proof state itself [obligations state is taken care in #11836] , but this will take some time.
2020-07-01Add a changelog.Pierre-Marie Pédrot
2020-07-01Add a test for Ltac2 parsing of parameterized types.Pierre-Marie Pédrot
2020-07-01Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t.Pierre-Marie Pédrot
It seems that nobody tried to write a parameterized type with more than one parameter since this was causing a syntax error. LL(1) being great, we work around the issue by factorizing the syntax with the generic parentheses and decide the validity after parsing.
2020-07-01Overlays for UIP in SPropGaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12504: [states] Move States to vernacGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: maximedenes
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
2020-07-01Merge PR #12605: [test-suite] async-proofs off in tests with Fail TimeoutGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-01Merge PR #12615: [ci] [performance-tests] Use a lighter target.Gaëtan Gilbert
Reviewed-by: JasonGross Reviewed-by: SkySkimmer
2020-07-01Use weak ref to memoize Evarutil.is_ground_envGaëtan Gilbert
2020-07-01Merge PR #12616: [ci] Disable the OCaml 4.12 targetGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-01Merge PR #12596: Credit Erik Martin-Dorel for work on Docker.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-01[ci] Disable the OCaml 4.12 targetEmilio Jesus Gallego Arias
Recent changes in Coqbot plus the unfortunate breakage OCaml upstream has make this too noisy. We will re-enable once https://github.com/ocaml/dune/pull/3585 is accepted upstream.
2020-06-30Cleanup mentions of -as in coqdep usage messageGaëtan Gilbert
2020-06-30[ci] [performance-tests] Use a lighter target.Emilio Jesus Gallego Arias
The current `perf` CI target is quite heavy, failing from out of memory sometimes. We use the target suggested by Jason Gross (<- thanks) in https://github.com/coq/coq/pull/12577#issuecomment-651970064
2020-06-30docs(README.md): Update badge and linksErik Martin-Dorel
* Coq images are not built anymore from a Docker Hub automated build, they are now built from this GitLab CI project: https://gitlab.com/coq-community/docker-coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:18:13 +0000