aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-20Do not perform the section variable check on global recipes.Pierre-Marie Pédrot
By construction, we know that Cooking is returning the right set of used variables. This set has been checked already once at the time when the definition was performed inside the section.
2019-05-20Ensure statically that declarations built by Term_typing are direct.Pierre-Marie Pédrot
This removes a lot of cruft breaking the opaque proof abstraction in Safe_typing and similar.
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-05-19Make the type of constant bodies parametric on opaque proofs.Pierre-Marie Pédrot
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-19Inverting the responsibility to define logically a constant in Declare.Pierre-Marie Pédrot
The code was intricate due to the special handling of side-effects, while it was sufficient to extrude the logical definition to make it clearer. We thus declare a constant in two parts, first purely kernel-related, then purely libobject-related.
2019-05-15Merge PR #10150: Handle tags shorter than "diff." without an exceptionGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-15Merge PR #10151: Clean up the API for side-effectsGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: gares
2019-05-15Merge PR #9905: [vm] x86_64 registersMaxime Dénès
Reviewed-by: maximedenes
2019-05-15Simplify the private constant API.Pierre-Marie Pédrot
We ungroup the rewrite scheme-defined constants, while only exporting a function to turn the last added constant into a private constant.
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: herbelin Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-05-14Merge PR #10136: [ltac2] Add primitive integersPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-05-14Merge PR #10164: Add aucontext debug printerPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
Ack-by: ejgallego Ack-by: maximedenes Reviewed-by: ppedrot
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-05-14Reduce the attack surface of Opaqueproof.Pierre-Marie Pédrot
2019-05-14Merge PR #10145: Code cleanups in tacticsHugo Herbelin
Reviewed-by: herbelin
2019-05-14Remove the sidecond_first flag of apply-related tactics.Pierre-Marie Pédrot
This was dead code.
2019-05-14Remove the elimrename field from Tactics.eliminator.Pierre-Marie Pédrot
This is actually dead code, we never observe it.
2019-05-14Code factorization in elim tactics.Pierre-Marie Pédrot
This is just moving code around, so it should not change the semantics.
2019-05-14Overlay for value-returning run_tacticGaëtan Gilbert
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-14Add aucontext debug printerGaëtan Gilbert
2019-05-14Merge PR #10152: Move last changelog entries for 8.10+beta1.Vincent Laporte
Reviewed-by: vbgl
2019-05-13Handle tags shorter than "diff." without an exceptionJim Fehrle
2019-05-13Adding overlay for Equations.Hugo Herbelin
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-13Moving Evd.evars_of_term from constr to econstr + consequences.Hugo Herbelin
This impacts a lot of code, apparently in the good, removing several conversions back and forth constr.
2019-05-13Missing change entry for #9854.Théo Zimmermann
2019-05-13Move last changelog entries for 8.10+beta1.Théo Zimmermann
2019-05-13Merge PR #10085: Do not include unreleased changelog in released versions.Vincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: jfehrle Reviewed-by: vbgl
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵Enrico Tassi
prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-13Add overlay for UnicoqMaxime Dénès
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
I don't think there's a reason to treat such variables more severely than unbound variables. This anomaly is often raised by debug printers (e.g. when studying complex scenarios using `Set Unification Debug`), and so makes debugging less convenient. Fixes #3754, fixes #10026.
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: jashug
2019-05-13Merge PR #10079: [refman] Move Ltac examples to Ltac chapter.Vincent Laporte
Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2019-05-12Merge PR #10083: Avoid trivial (u=u) constraints in AcyclicGraph.constraints_forEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-05-11Merge PR #10006: NanoPG: a general fix + fixing Meta-based bindings on MacOS ↵Pierre-Marie Pédrot
+ adding a go-to-end binding + improving documentation Reviewed-by: gares Ack-by: herbelin Reviewed-by: ppedrot
2019-05-11Remove the sidecond_first flag of apply-related tactics.Pierre-Marie Pédrot
This was dead code.
2019-05-11Remove the elimrename field from Tactics.eliminator.Pierre-Marie Pédrot
This is actually dead code, we never observe it.
2019-05-11Code factorization in elim tactics.Pierre-Marie Pédrot
This is just moving code around, so it should not change the semantics.
2019-05-11Merge PR #10052: Cleanup the hypothesis conversion functionHugo Herbelin
Reviewed-by: herbelin
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10[refman] Mention the `#[canonical(false)]` attributeVincent Laporte
2019-05-10[Attributes] Allow explicit value for two-valued attributesVincent Laporte
Attributes that enable/disable a feature can have an explicit value (default is enable when the attribute is present). Three-valued boolean attributes do not support this: what would `#[local(false)]` mean?
2019-05-10Add overlay for elpiVincent Laporte
2019-05-10Changelog for PR #10076Vincent Laporte
2019-05-10[User manual] Fix two warnings related to canonical structuresVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:02:33 +0000