aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-21Merge PR #10587: [coqdoc] Nest <a> into <h2> instead of the other way aroundEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
Ack-by: Zimmi48
2019-11-21Merge PR #11010: [coq] Untabify the whole ML codebase.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ```
2019-11-21Merge PR #11103: Grammars: unification fix/cofix between constr/vernac + ↵Emilio Jesus Gallego Arias
cleaning Reviewed-by: ejgallego
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
Reviewed-by: gares Reviewed-by: silene
2019-11-20Merge PR #11144: Fix broken linksThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-20Fix broken linksNikita Eshkeev
This patch fixes broken links in the CONTRIBUTING.md document
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
2019-11-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing ↵charguer
(fixing bug #11057). With this new behavior, it is not needed to .vos files in user contribs. Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
2019-11-20Merge PR #11068: coq_makefile: support COQBIN with no ending /Enrico Tassi
Reviewed-by: gares
2019-11-20Merge PR #11074: coqdep: only output vos when passed -vosEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2019-11-19G_constr: Renaming record_fields_instance -> fields_def.Hugo Herbelin
This is in accordance with PR #10614 and to avoid a confusion with the fields of a record type in g_vernac.ml. Removing a useless line at the same time in G_vernac.
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:36:40 +0000