aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-16Suggesting to use injection when an injection pattern is given to destruct.Hugo Herbelin
This hopefully clarifies the confusing role of destruct (see #13205).
2020-11-16[gc] Set GC policy as best-fit in OCaml >= 4.10.0Emilio Jesus Gallego Arias
Closes #11277 ; the `space_overhead` parameter has been selected for maximum speedup, in some cases it could also increase memory consumption. Please use `OCAMLRUNPARAM` to tune it and report back your experiments.
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named ↵coqbot-app[bot]
variables. Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: SkySkimmer
2020-11-16Merge PR #13337: Avoid exposing an internal name when "intros _ H" fails ↵coqbot-app[bot]
because of _ being dependent in H Reviewed-by: gares
2020-11-16Fix incorrect name refreshing when interning a generalized binderGaëtan Gilbert
Fix #13249
2020-11-16Add changelog for #13337.Hugo Herbelin
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context ↵coqbot-app[bot]
of the definition of the metas Reviewed-by: mattam82
2020-11-16Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` ↵Pierre-Marie Pédrot
commands Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part ↵coqbot-app[bot]
of unification Reviewed-by: mattam82
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: ppedrot
2020-11-16Merge PR #12685: Propagating scope information in indirect application to a ↵Pierre-Marie Pédrot
reference. Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-11-16Document the deprecation of the commands.Pierre-Marie Pédrot
2020-11-16Document the new warning.Pierre-Marie Pédrot
2020-11-16Tentative fix for the refman.Pierre-Marie Pédrot
2020-11-16Fix test-suite.Pierre-Marie Pédrot
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
By default Coq stdlib warnings raise an error, so this is really required.
2020-11-16Warning on hint commands that have no explicit locality.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
Reviewed-by: silene Reviewed-by: gares Reviewed-by: Zimmi48
2020-11-16Deprecate `Grab Existential Variables` and `Existential` commandsMaxime Dénès
2020-11-16Overlay for Coq-Equations.Hugo Herbelin
2020-11-16Checking type in unification imitation: avoid raising a non-located error.Hugo Herbelin
2020-11-16Fixing a (known) "bugged" part of imitation in unification.Hugo Herbelin
We ensure that when imitation stops to be possible, we postpone an equation of the type of the subterm (and not of the arbitrary type of an evar possibly depending on this subterm).
2020-11-16Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freecoqbot-app[bot]
Reviewed-by: anton-trunov Reviewed-by: Blaisorblade
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
It remains to accept resolving Type(u)<=Prop for u arbitrary sort variable.
2020-11-16Extend hack to use postponed constraints in retyping to template polyGaëtan Gilbert
See 742ef62fe8050a6865d06bd644e30cbec0e7eb02 Fix #13366 Fix #9809
2020-11-16Finish fixing setoid rewrite under anonymous lambdas (hopefully)Gaëtan Gilbert
Fix #13246 Not sure if this is the right thing to do, but it seems to work.
2020-11-16Only lower inductives to Prop if the type is syntactically an arity.Gaëtan Gilbert
Fix #13300
2020-11-16Small cleanup in ComInductiveGaëtan Gilbert
2020-11-16Update grammar in docJim Fehrle
2020-11-16Changelog for variance syntaxGaëtan Gilbert
2020-11-16Overlays for cumulative inductive syntaxGaëtan Gilbert
2020-11-16Doc for variance syntaxGaëtan Gilbert
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-16Infrastructure for cumulative inductive syntax (no grammar extension yet)Gaëtan Gilbert
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ↵coqbot-app[bot]
sort elimination constraints Reviewed-by: gares
2020-11-16Slight improvement to the changelog entry.Théo Zimmermann
2020-11-15Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"Jim Fehrle
2020-11-15Merge PR #12611: [record] Cleanup of data structure and functionscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: gares
2020-11-15Intern application arguments in left-to-right orderGaëtan Gilbert
This makes it so that we have an application `h a b` with both `a` and `b` unbound, `a` is the one that is reported (parent commit with my current compiler setup reports `b` first, and the code does not define which it should be). Ideally we would report both but that requires more code.
2020-11-15Ensuring the body of the notation in Locate is printed at level 0.Hugo Herbelin
This is consistent with the syntax of Notation and is (IMO) clearer.
2020-11-15Adding support for Locate "( x , y )".Hugo Herbelin
It finds "( x , y , .. , z )". Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-15Fixing Locate for recursive notations with names.Hugo Herbelin
E.g. Locate "(x , y , .. , z )" now works while only Locate "(_ , _ , .. , _ )" was working before. This also fixes a confusion between a variable and its anonymization into _, wrongly finding notations mentioning '_'. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-15Merge PR #13374: [dune] [opam] Generate opam files automatically using Dune.coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-15Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block ↵Li-yao Xia
verbatim from inline verbatim Reviewed-by: Lysxia
2020-11-15Moving the analysis of notation strings in notation.ml.Hugo Herbelin
This is a better abstraction barrier (no "symbol" type with uninterpreted ".." exported out of notation.ml). It also allows to "browse" notations mentioning a "..".
2020-11-15Indentation.Hugo Herbelin
2020-11-15Add changelog for #13387.Hugo Herbelin
2020-11-15Fixes #12348: long-standing de Bruijn indices bug in imitation ↵Hugo Herbelin
(solve_simple_eqn). The bug was that an assumption could be interpreted as a local definition and wrongly expanded. It triggered rarely because it involved mixing let-ins and local assumptions + imitation under binders.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 23:42:46 +0000