aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2019-05-14Adding missing newline in coqc usage.Hugo Herbelin
2019-05-14CoqIDE: Treat unknown arguments starting with dash as unknown options rather ↵Hugo Herbelin
than files.
2019-05-14Removing no more existing option -emacs-U.Hugo Herbelin
2019-05-14Usage: fixing indentation for set/unset options.Hugo Herbelin
2019-05-14Ensuring suffix of file to compile also for -vio2vo checking.Hugo Herbelin
We do it by consistently using variants of the "ensure_exists" policy in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and parallel vio checking (schedule-vio-checking). For instance, coqc -vio2vo dir/file.vio now works, while before, dir/file was expected. Incidentally, this avoids the non-recommended Loadpath.locate_file.
2019-05-14Option -check-vio-tasks: fail gracefully when not finding expected integers.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 11:11:31 +0000