aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)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
2019-11-19Merge PR #11106: Printing name of change log file in changelog scriptGaëtan Gilbert
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
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-16Merge PR #10998: Add missing zify class instancesFrédéric Besson
2019-11-16Merge PR #11095: Do not export the internals of the prepare_hint function.Gaëtan Gilbert
2019-11-15Merge PR #11079: Rename non-unique local nonterminalsHugo Herbelin
2019-11-15Update doc/changelog/04-tactics/10998-zify-complements.rstKazuhiko Sakaguchi
2019-11-15Add missing zify class instancesKazuhiko Sakaguchi
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-14Merge PR #10979: Fix doc for universes(foo) attributesThéo Zimmermann
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
2019-11-14doc fixesAntonio Nikishaev
2019-11-14Restore documentation of `Typeclasses Axioms Are Instances`Maxime Dénès
2019-11-14Document recommended syntax for `firstorder`Maxime Dénès
2019-11-13cleanup unused argument for Classes.do_instance_resolve_TCGaëtan Gilbert
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
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
2019-11-13Merge PR #11070: Do not rely on the user settings but on the actual window si...Pierre-Marie Pédrot
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
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
2019-11-12Merge PR #11045: Forbid Include inside sectionsPierre-Marie Pédrot
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
2019-11-11Merge PR #11032: Run update-compat script with --release option.Pierre-Marie Pédrot
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-11Merge PR #11052: Fix #11048: uncaught destKO in inductive typePierre-Marie Pédrot
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
2019-11-10Merge PR #10980: Fix #10903: type-in-type allows fixpoints on sprop inductivesPierre-Marie Pédrot
2019-11-09Merge PR #11017: Make [Proof_global.closed_proof_output] opaquePierre-Marie Pédrot
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
2019-11-08Merge PR #11014: Fix #8459: anomaly not enough abstractions in fix bodyPierre-Marie Pédrot
2019-11-08Merge PR #11069: Do not include final stops in queries. (Fixes #11058)Pierre-Marie Pédrot
2019-11-08coqdep: only output vos when passed -vosGaëtan Gilbert
2019-11-08Merge PR #11050: Replace "option" in doc when it refers to a flagThéo Zimmermann