aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-10Merge PR #13922: Mention overlays in PR templatecoqbot-app[bot]
Reviewed-by: Zimmi48
2021-03-10Mention overlays in PR templateGaëtan Gilbert
2021-03-10Merge PR #13901: Fix list contributorscoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: jfehrle
2021-03-10Adding output tests.Pierre-Marie Pédrot
2021-03-10Add documentation.Pierre-Marie Pédrot
2021-03-10Allow to register deprecation status in Ltac2 term and notation declarations.Pierre-Marie Pédrot
2021-03-10Regenerate the Ltac2 syntax for documentation.Pierre-Marie Pédrot
2021-03-10Adding documentation of the changes.Pierre-Marie Pédrot
2021-03-10Adding a parsing test.Pierre-Marie Pédrot
2021-03-10Allow the presence of type casts for return values in Ltac2.Pierre-Marie Pédrot
2021-03-10Merge PR #13912: Refactor coercionopscoqbot-app[bot]
Reviewed-by: gares
2021-03-10Merge PR #13919: Fix a hyperlink in CONTRIBUTING.mdcoqbot-app[bot]
Reviewed-by: Zimmi48
2021-03-10Fix a hyperlink in CONTRIBUTING.mdKazuhiko Sakaguchi
2021-03-09Add changelogKazuhiko Sakaguchi
2021-03-09Add overlayKazuhiko Sakaguchi
2021-03-09Add the source and target classes to the coercion tableKazuhiko Sakaguchi
`coe_source` and `coe_target` fields of type `cl_typ` have been added to `coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a coercion. The `coercion` record has also been replaced with `coe_info_typ`.
2021-03-09Replace cl_index with cl_typ in coercionops.mlKazuhiko Sakaguchi
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been replaced with `cl_typ` and `ClTypMap` respectively.
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-07Merge PR #13910: Attempt to fix the bench after coq-core splitPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-07Attempt to fix the bench after coq-core splitGaëtan Gilbert
2021-03-06[vernac] Improve alpha-renaming in record projection typesLi-yao Xia
2021-03-06Inline the refold and tactic_mode flags for the cbn tactic.Pierre-Marie Pédrot
They were unconditionally set to true, leading to a lot of dead branches.
2021-03-06Merge PR #13586: Support nested timeoutsPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-06Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoidsPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
Reviewed-by: JasonGross Reviewed-by: MSoegtropIMC
2021-03-06Merge PR #13902: [coercion] expose coercion_infoPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-06Merge PR #13899: Add noncritical constraint to exception catching in ↵Pierre-Marie Pédrot
solve_constraints Reviewed-by: ppedrot
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-03-05[coercipn] expose coercion_infoEnrico Tassi
2021-03-05Update nixpkgs.Théo Zimmermann
To get the right version of git to use the list-contributors.sh script.
2021-03-05Fix the .mailmap.Théo Zimmermann
2021-03-05Document the relation of the list-contributors.sh script to .mailmap.Théo Zimmermann
2021-03-05Fix list-constributors.sh script.Théo Zimmermann
2021-03-05Merge PR #13900: doc: don't count a contributor twice in the changelogcoqbot-app[bot]
Reviewed-by: Zimmi48
2021-03-04Correctly sort the glossaryJim Fehrle
2021-03-04doc: don't count a contributor twice in the changelogLi-yao Xia
2021-03-04Merge PR #13897: Cleanup internal hint locality handlingcoqbot-app[bot]
Reviewed-by: ppedrot Reviewed-by: ejgallego
2021-03-04Add noncritical constraint to exception catching in solve_constraintsLasse Blaauwbroek
2021-03-04Properly support nested timeoutsLasse Blaauwbroek
2021-03-04Cleanup internal hint locality handlingGaëtan Gilbert
By separating the libobject for create db and other hints we can unify handling of local/superglobal.
2021-03-04[test-suite] test for primitive tokens in patternsEnrico Tassi
2021-03-04[doc] changelog entryEnrico Tassi
2021-03-04[doc] Set/Unset Printing Raw LiteralsEnrico Tassi
2021-03-04[notation] option to fine tune printing of literalsEnrico Tassi
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
ssreflect asks setoid rewrite to rewrite in goal "forall_special_name_ : T, _other_name_" Since this is a non dependent product, setoid rewrite converts that to "impl T _other_name_" and must be taught to restore the special name when unfolding impl.
2021-03-03Merge PR #12567: [build] Split stdlib to it's own package.coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: gares Ack-by: LasseBlaauwbroek Ack-by: silene Ack-by: vbgl
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
2021-03-02Merge PR #13889: Dead code elimination: not reducible error message is never ↵coqbot-app[bot]
raised. Reviewed-by: jfehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 06:44:04 +0000