aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-20Remove VtUnknown classificationMaxime Dénès
This clean-up removes the dependency of the current proof mode (and hence the parsing state) on unification. The current proof mode can now be known simply by parsing and elaborating attributes. We give access to attributes from the classifier for this purpose. We remove the infamous `VtUnknown` code path in the STM which is known to be buggy. Fixes #3632 #3890 #4638.
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-20Merge PR #10149: [refman] Misc fixes (indentation, whitespace, notation syntax)Théo Zimmermann
Reviewed-by: Zimmi48
2019-05-19[refman] Document etransitivityClément Pit-Claudel
2019-05-19[refman] Fix up the grammar entry for field_defClément Pit-Claudel
2019-05-19[refman] Add a .. cmd:: header for Reserved Notation and Reserved InfixClément Pit-Claudel
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-05-19[refman] Fix up the documentation of Instance and Existing InstanceClément Pit-Claudel
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-19Merge PR #10184: A few nix-related updatesThéo Zimmermann
Reviewed-by: Zimmi48
2019-05-19Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ↵Théo Zimmermann
notations Reviewed-by: Zimmi48 Ack-by: jfehrle
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-19Merge PR #10190: Implicit Quantifiers recurse in continuation of let-inHugo Herbelin
Reviewed-by: herbelin
2019-05-19Implicit Quantifiers recurse in continuation of let-inJasper Hugunin
2019-05-18Merge PR #10134: Simplify impargsHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin Ack-by: jashug
2019-05-17Fail: don't catch critical errorsGaëtan Gilbert
Not sure why we didn't. Fail didn't catch anomalies almost by accident. It still makes sense to catch Timeout here imo
2019-05-17[CI/Azure/macOS] Target macOS version 10.11Vincent Laporte
2019-05-17Overlay for removing Generalized 1st argGaëtan Gilbert
2019-05-17[nix] Update reference to nixpkgsVincent Laporte
2019-05-17[Nix-ci] Update Unicoq patchVincent Laporte
2019-05-17[default.nix] Exclude the nix/ directory from sourcesVincent Laporte
2019-05-17[Nix-CI] Bignums no longer depends on camlp5Vincent Laporte
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
Closes GH-8482.
2019-05-16Fix #10176: shadowing vs automatic class based generalizationGaëtan Gilbert
2019-05-16binder_kind Generalized: remove 1st arg as it's always ImplicitGaëtan Gilbert
https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#implicit-generalization >The generalizing binders `{ } and `( ) work similarly to their >explicit counterparts, only binding the generalized variables >implicitly, as maximally-inserted arguments. I guess this was meant to provide a way to get "(A:_) {B:bla A}" from "`{B:bla A}" (where A is generalizable) but there's no syntax for it so let's drop the ml side until such a syntax exists.
2019-05-16Cleanup Implicit_quantifiers.implicit_applicationGaëtan Gilbert
- fix misleading indentation - simplify "let a, b = e in a, b" -> "e"
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-14Fix #10161: occur check when defining an algebraic universe.Gaëtan Gilbert
2019-05-14Coqc: Ensure that at most one file is given when -o is also given.Hugo Herbelin
2019-05-14Coqc: Ensure exclusiveness of options -quick and -vio2vo.Hugo Herbelin
2019-05-14Usage: Fixing wrong description of load_vernac_object and similar.Hugo Herbelin
We also preventively add quoted around Load to suggest that the file can have "/" in it. We also fix a too far indentation.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-17 21:23:06 +0000