aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-31[classes] Remove a couple of unneeded option typesEmilio Jesus Gallego Arias
Suggested by Gaëtan Gilbert.
2019-10-31[classes] Untabify in preparation for next commit.Emilio Jesus Gallego Arias
2019-10-31[classes] Some refactoring on proof save preparation.Emilio Jesus Gallego Arias
Note the ugly problem that we have on close_proof: ``` proof_global.ml:278 let entry_fn p (_, t) = let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in ``` arguments of start_proof should be pre-normalized. I think this will require a lot of refactoring to be fixed properly.
2019-10-31Fix #8459: anomaly not enough abstractions in fix bodyGaëtan Gilbert
We reach the anomaly because we call check_fix on a surrounding fixpoint from the pretyper, and the inner fix hasn't been checked. Using whd_all isn't useful in the specific reported case but a case where it's necessary can probably be crafted. See also #11013
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-31[Nix] Update reference to nixpkgsVincent Laporte
This version of nixpkgs includes: - Dune 1.11.4 - GTK3 3.24.12 - menhir 20190626
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-30Implement the unsupported attribute error using the warning systemGaëtan Gilbert
This means we can disable it to ignore unsupported attributes. For instance this would be useful if we change some behaviour of `Cmd` and add an attribute `att` to restore the old behaviour, then `#[att] Cmd` is backwards compatible if the warning is disabled.
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-30make: guard cp calls with rm -f on executablesGaëtan Gilbert
Fix #10728
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-30Numbers.Cyclic: use “lia” rather than “omega”Vincent Laporte
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 15:12:35 +0000