aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-31[prettyp] remove `mod_ops` and `indirect_accessor` parametersGaëtan Gilbert
`Prettyp` is now late enough in linking to refer to them.
2019-10-31restore red behaviour printingGaëtan Gilbert
2019-10-31changelog for #10985Gaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-31ppvernac: bidi hints use & not |Gaëtan Gilbert
2019-10-31Print argument info as an Arguments command in AboutGaëtan Gilbert
Close #10961
2019-10-31Move prettyp (Print implementation) to vernac/Gaëtan Gilbert
2019-10-31Doc: index command Arguments with assertGaëtan Gilbert
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert
2019-10-31Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: jfehrle
2019-10-31Merge PR #11009: Rename the 2 local type_cstr nonterminals to give them ↵Pierre-Marie Pédrot
unique names Reviewed-by: ppedrot
2019-10-31Merge PR #10995: add test for #4502 (fixed by unknown commit)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-31Merge PR #10933: Add clarification in make-changelog.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-10-30Merge PR #10953: [declare] Remove declare_scheme hook in DeclarePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-30Merge PR #11004: [test-suite] Test section-local mutual Fixpoint.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-30Rename the 2 local type_cstr nonterminals to give them unique namesJim Fehrle
2019-10-30Merge PR #10999: [refman] Give an example of contradiction when positivity ↵Clément Pit-Claudel
checking is disabled. Reviewed-by: cpitclaudel
2019-10-30[test-suite] Test section-local mutual Fixpoint.Emilio Jesus Gallego Arias
Noticed by coverage, test code by Gäetan Gilbert. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2019-10-30Use bullets and indentation (but the result rendering is weird).Théo Zimmermann
2019-10-30Use explicit match as suggested by Clément.Théo Zimmermann
2019-10-30[refman] Add a second example of contradiction when positivity checking is ↵Théo Zimmermann
disabled.
2019-10-30Make changelog script aware of trailing slashes.Arthur Azevedo de Amorim
2019-10-30[refman] Give an example of contradiction when positivity checking is disabled.Théo Zimmermann
2019-10-30[declare] Remove declare_scheme hook in DeclareEmilio Jesus Gallego Arias
We introduce a new module that registers the scheme information that side-effects need, thus removing the hook from `Declare`. As we may want to deprecate scheme side effects, there is no need to design a general mechanism for this kind of registration for now. Would we remove the scheme side-effects the scheme code could become self-contained again.
2019-10-30Merge PR #10960: Move inference_hook from vernacentries to lemmasEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-10-30Merge PR #10973: Remove dead code in save_remaining_recthmsEmilio Jesus Gallego Arias
Ack-by: JasonGross Reviewed-by: ejgallego
2019-10-30Merge PR #10981: [abstract] Remove un-unused reference to `evar_map`Pierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-10-30Merge PR #10303: Raise an anomaly when looking up unknown constant/inductivePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-30Merge PR #10949: [declare] Provide helper for private constant inlining.Pierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-10-30Merge PR #10681: [declare] Make `proof_entry` a private type.Pierre-Marie Pédrot
2019-10-30Move start_proof_com from lemmas to vernacentriesGaëtan Gilbert
This lets us remove the closure passing for the program inference_hook
2019-10-30add test for #4502 (fixed by unknown commit)Gaëtan Gilbert
Close #4502
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: herbelin
2019-10-29Merge PR #10966: `assert_succeeds`&`assert_fails`: multisuccess fixGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-10-29Show diffs in "Show Proof."Jim Fehrle
Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output
2019-10-29Use a less kludgy way of solving #9114Jason Gross
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
These tactics now work correctly with multisuccess tactics by wrapping the tactic argument in `once`. Fixes #10965
2019-10-29[abstract] Remove un-unused reference to `evar_map`Emilio Jesus Gallego Arias
We use an `evar_map ref` even tho the modification the `evar_map` is ignored. I'm not sure if this is a bug or not, so I am making thus preserving the behavior but making the what is going with the `evar_map` more explicit.
2019-10-29[declare] Use helper function for `fix_exn` instead of relying on internals.Emilio Jesus Gallego Arias
2019-10-29[declare] Make `proof_entry` a private type.Emilio Jesus Gallego Arias
Proof entries are low-level objects and should not be manipulated by users directly, in particular as we want to unify all the code around declaration of constants. This patch doesn't bring by itself a lot of improvement, other than setting the base where to extend the interface, however it already points out some points of interest, and in particular the manipulation of opacity done by `Derive` which can be quite problematic, and of course the handling of delayed proofs. So while this is a first step, IMHO it doesn't harm a lot having it in place, but a lot more work will be needed, in particular regarding the handling of delayed proofs. To make `proof_entry` a fully abstract type, the remaining work is focused on `abstract` and obligations, both of which do quite a few hackery that will have to be migrated to the `Declare` API.
2019-10-29Merge PR #10892: [engine] Remove UnivGen.global_of_constrPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-10-29Document the ability to bind notation arguments in Ltac2.Pierre-Marie Pédrot
2019-10-29Fix #10615: Notation substitution for Ltac2 terms.Pierre-Marie Pédrot
We implement a new type of "preterms" that represent untyped ASTs, corresponding to glob_expr in the ML implementations. Ltac2 quotations inside notations are provided with such preterms, and have to pretype them in order to do anything of relevance with them.
2019-10-29Merge PR #10942: Describe XML tags used for highlighting diff textThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-29Merge PR #10947: Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in ↵Enrico Tassi
`coq_makefile` Ack-by: SkySkimmer Reviewed-by: gares
2019-10-28Merge PR #10963: Possible simplification of parsing rules.Clément Pit-Claudel
Reviewed-by: ppedrot
2019-10-28Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the ↵Kazuhiko Sakaguchi
`coq_makefile` utility The `coq_makefile` utility and `Makefile`s generated by it generate and include some files: `<CoqMakefile>.conf`, `<CoqMakefile>.local`, and the dependency file `.coqdep.d`, where `<CoqMakefile>` is the name of the output file given by the `-o` option. Out of these, only the name of the dependency file `.coqdep.d` is fixed to a constant. This seems to be a potential pitfall when we place multiple `Makefile`s generated by `coq_makefile` in the same directory. This patch renames `.coqdeps.d` to `.<CoqMakefile>.d`.
2019-10-28[declare] Provide helper for private constant inlining.Emilio Jesus Gallego Arias
We factor some duplicate code, this is a step towards making the `proof_entry` type abstract.
2019-10-28Fix typos.Théo Zimmermann
Co-Authored-By: Clément Pit-Claudel <cpitclaudel@users.noreply.github.com>
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:17:57 +0000