aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-12Lowercase variables in git_downloadGaëtan Gilbert
2020-10-12elpi 1.11.4Enrico Tassi
2020-10-11Modify ZArith/Znumtheory.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zdiv.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zcomplements.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZifyInst.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZifyClasses.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Ztac.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZCoeff.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zpow_def.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Wf_Z.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zabs.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Znat.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/RingMicromega.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Tauto.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Refl.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/EnvRing.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify NArith/Ndigits.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Strings/String.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Strings/Ascii.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/VectorEq.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/VectorSpec.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/VectorDef.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/Fin.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/OrderedRing.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Arith/Euclid.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Arith/Div2.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Arith/Even.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify setoid_ring/Ring.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify setoid_ring/InitialRing.v to compile with -mangle-namesJasper Hugunin
2020-10-11Similarly remove the explicit graph argument in the ~evar conversion API.Pierre-Marie Pédrot
2020-10-11Pick the universe graph out of the environment in conversion API.Pierre-Marie Pédrot
2020-10-11Remove the compare_graph field from the conversion API.Pierre-Marie Pédrot
We know statically that the first thing the conversion algorithm is going to do is to get it from the provided function, so we simply explicitly pass it around.
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
We simply use evars instance in the right order while reading back VM values.
2020-10-10Adding change log for #12950.Hugo Herbelin
2020-10-10Documenting the new only-parsing only-printing model.Hugo Herbelin
2020-10-10New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.Hugo Herbelin
2020-10-10Adding a warning in case a notation is used neither for parsing nor printing.Hugo Herbelin
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
The (old) original model for notations was to associated both a parsing and a printing rule to a notation. Progressively, it become more and more common to have only parsing notations or even multiple expressions printed with the same notation. The new model is to attach to a given scope, string and entry at most one either only-parsing or mixed-parsing-printing rules + an arbitrarily many unrelated only-printing rules. Additionally, we anticipate the ability to selectively activate/deactivate each of those. This allows to fix in particular #9682 but also to have more-to-the-point warnings in case a notation overrides or partially overrides another one. Rules for importing are not changed (see forthcoming #12984 though). We also improve the output of "Print Scopes" so that it adds when a notation is only-parsing, only-printing, or deactivated, or a combination of those. Fixes #4738 Fixes #9682 Fixes part 2 of #12908 Fixes #13112
2020-10-10Splitting ssrbool's multi-printing notations into parsing and printing.Hugo Herbelin
This is in anticipation of a model with an explicit difference between a parsing-printing notation and the pair of only-parsing notation + only-printing notation.
2020-10-10Notation.ml: Move interpretation_eq earlier for future use.Hugo Herbelin
Also add optimisation of interpretation_eq.
2020-10-10Print Scope & cie: Add parentheses around notation interpretation.Hugo Herbelin
This is to be consistent with the use of parentheses in the syntax of Notation and to support a list of attribute afterwards.
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵Hugo Herbelin
deprecated.
2020-10-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-10-10Adding and using locations on identifiers in constr_expr where they were ↵Hugo Herbelin
missing.
2020-10-10Closes #13142 (more standardized pretty-printing of records).Hugo Herbelin
2020-10-10Merge PR #13164: [bench] Dump the vo size difference.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
Add menu item that uses this
2020-10-09Modify ZArith/ZArith_dec.v to compile with -mangle-namesJasper Hugunin
2020-10-09Modify Bool/Sumbool.v to compile with -mangle-namesJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 01:21:36 +0000