aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-19G_constr: Renaming instance -> univ_instance (more specific name).Hugo Herbelin
2019-11-19G_constr: Uniformization of indentation.Hugo Herbelin
2019-11-19Separating constr grammar for fix and cofix, for the purpose of documentation.Hugo Herbelin
2019-11-19Grammar: slight simplification of treatment of annot/binder overlapping.Hugo Herbelin
2019-11-19Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.Hugo Herbelin
2019-11-19Grammar of terms: mini-shortcut in the rules for fix and cofix.Hugo Herbelin
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-19coq_makefile: support COQBIN with no ending /Gaëtan Gilbert
Close #6460
2019-11-19Merge PR #11106: Printing name of change log file in changelog scriptGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-11-19added changelog entryCyril Cohen
2019-11-18Adding `inj_compr` lemma in ssrfun.Cyril Cohen
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-14Restore documentation of `Typeclasses Axioms Are Instances`Maxime Dénès
This documentation seems to have been lost after it was introduced by 0ad26633a4589d77de1f864733d1d953dab9ea91 We also document that this flag is deprecated.
2019-11-14Document recommended syntax for `firstorder`Maxime Dénès
Only the deprecated one was documentated, and the deprecation was not mentioned.
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-13Register proof_irrelevancePierre Roux
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 20:57:00 +0000