aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
We restrict #8890 so that it looks for a notation only for the fully applied coercion.
2019-11-20Merge PR #11074: coqdep: only output vos when passed -vosEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2019-11-19Merge PR #11106: Printing name of change log file in changelog scriptGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-11-18Merge PR #11115: [dune] Update .gitignore after #11092Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-11-16Merge PR #10998: Add missing zify class instancesFrédéric Besson
Ack-by: Zimmi48
2019-11-16Merge PR #11095: Do not export the internals of the prepare_hint function.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-11-15Merge PR #11079: Rename non-unique local nonterminalsHugo Herbelin
Ack-by: Zimmi48 Ack-by: herbelin
2019-11-15Update doc/changelog/04-tactics/10998-zify-complements.rstKazuhiko Sakaguchi
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-11-15Add missing zify class instancesKazuhiko Sakaguchi
Add missing zify class instances for `Pos.pred_double`, `Pos.pred_N`, `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`, `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, `Z.quot2`, `isZero`, and `isLeZero`. Instances for `isZero` and `isLeZero` are useful to provide new zify instances by using Micromega tactics.
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-14Merge PR #10979: Fix doc for universes(foo) attributesThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
Fix #10570
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2019-11-14doc fixesAntonio Nikishaev
2019-11-13cleanup unused argument for Classes.do_instance_resolve_TCGaëtan Gilbert
not sure what that's about
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
We can now do `#[refine] Instance : Bla := bli.` to enter proof mode with `bli` as a starting refinement. If `bli` is enough to define the instance we still enter proof mode, keeping things nicely predictable for the stm.
2019-11-13don't double parse program attribute for vernacinstanceGaëtan Gilbert
2019-11-13Update .gitignore after #11092Pierre Roux
2019-11-13Merge PR #11094: Miscellaneous micro-improvements of the syntax of recordsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-13Merge PR #11070: Do not rely on the user settings but on the actual window ↵Pierre-Marie Pédrot
size. (Fixes #10956) Reviewed-by: ppedrot
2019-11-12Printing name of change log file in changelog script.Hugo Herbelin
2019-11-12Merge PR #11067: Expand documentation about generating a Docker image.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: vbgl
2019-11-12Expand documentation about generating a Docker image.Pierre-Marie Pédrot
2019-11-12Merge PR #11092: [dune] Have only one rule calling configureEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-11-12Merge PR #11045: Forbid Include inside sectionsPierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: gares Reviewed-by: ppedrot
2019-11-11Have only one dune rule calling configurePierre Roux
2019-11-11Do not export the internals of the prepare_hint function.Pierre-Marie Pédrot
This statically ensures more invariants and moves a global declaration out of this function.
2019-11-11Merge PR #11032: Run update-compat script with --release option.Pierre-Marie Pédrot
Reviewed-by: JasonGross Ack-by: ppedrot
2019-11-11Run update-compat script with --release option.Théo Zimmermann
This should ideally have been done before the 8.11 branching.
2019-11-11Merge PR #11052: Fix #11048: uncaught destKO in inductive typePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
- only one space instead of two when printing "{| |}" - removing a redundant clause in the grammar of record_patterns
2019-11-10Merge PR #10980: Fix #10903: type-in-type allows fixpoints on sprop inductivesPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-09Merge PR #11017: Make [Proof_global.closed_proof_output] opaquePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
This means return_proof is the only place where it can be produced. We need to change the stm a bit as it keeps a pointer to a [closed_proof_output] to join and to check if it failed, and it needs a way to create a dummy in 1 case. I'm not sure if this works correctly though, how to test? We also inline the used bits of [return_proof ~allow_partial:true] in [save_lemma_admitted] to get [Proof using] info. We could alternatively expose the [closed_proof_output -> constr list] projection. I think the code is easier to understand this way though, as we don't have to read [return_proof] and figure out that the side effect manipulation is ignored etc. Note that the "this will warn" comment was outdated since 73daf37ccc7a44cd29c9b67405111756c75cb26a
2019-11-08Merge PR #11014: Fix #8459: anomaly not enough abstractions in fix bodyPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-08Merge PR #11069: Do not include final stops in queries. (Fixes #11058)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-08coqdep: only output vos when passed -vosGaëtan Gilbert
This fixes dune. TBH the problem is that dune is too strict, but we can't go back in time to change it.
2019-11-08Merge PR #11050: Replace "option" in doc when it refers to a flagThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-08Merge PR #11042: The "univ poly can capture global univs" checker side bug ↵Théo Zimmermann
is fixed Reviewed-by: Zimmi48
2019-11-07Do not rely on the user settings but on the actual window size. (Fixes #10956)Guillaume Melquiond
This should fix the issue when creating new session panes. The initial session panes, however, might still be wrongly sized, as we do not yet know, at the time they are created, if the window manager will respect the user settings fixing the window size.
2019-11-07Do not include final stops in queries. (Fixes #11058)Guillaume Melquiond
The bug was introduced by #10063, which eagerly added dots to identifier without considering whether they are related to the identifier. Along the way, this commit also prevents primes and digits from being added as initial characters of identifiers. This works for both word selection and queries. Note that there is still a small issue with word selection, when the current word starts with a digit. Indeed, when double-clicking, GTK will already have extended the selection to it, so we have no way of preventing the digit from being part of the selection. This commit also fixes the unusual calling convention of Gtk_parsing.end_words.
2019-11-07The "univ poly can capture global univs" checker side bug is fixedGaëtan Gilbert
(by the checker refactor AFAICT) + fix commit for the coqtop side fix (it got rebased at some point) Close #10705
2019-11-07Merge PR #11049: Prevent redefinition of Ltac2 types and constructors inside ↵Pierre-Marie Pédrot
a module Reviewed-by: ppedrot
2019-11-07Merge PR #11059: Swap parsing precedence of `::` and `,` ; Fix #10116Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-06Merge PR #11038: fix(*.opam): Add missing version "dev"Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48
2019-11-06Swap parsing precedence of `::` and `,` ; Fix #10116Kenji Maillard
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-06Merge PR #11041: Cite POPL19 SProp paperThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-06Merge PR #11051: elpi 1.8Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 13:53:06 +0000