aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-05Add new page to writing proof index.Théo Zimmermann
2020-11-05Remove everything before term rewriting and simplification.Théo Zimmermann
2020-11-05Remove everything after term rewriting and simplification.Théo Zimmermann
2020-11-05Move some content to a new page on term rewriting and simplification.Théo Zimmermann
2020-11-05Merge PR #13231: Remove warning on SSR Search having moved.coqbot-app[bot]
Reviewed-by: gares
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
Reviewed-by: gares
2020-11-04[stdlib] Decidable instance for negationYishuai Li
Added Changelog
2020-11-05Add overlaysPierre Roux
2020-11-05Add changelogPierre Roux
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
As noted by Hugo Herbelin, Dec is rather used for "decidable".
2020-11-05[refman] Add an example for number notationsPierre Roux
As suggested by Jim Fehrle while reviewing #12218
2020-11-05Allow multiple primitive notation on the same scope and triggersPierre Roux
Until now, declaring a number or string notation on some trigger removed all previous notations on the same scope. Bug discovered by Jason Gross while reviewing #12218.
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Add tests for implicit argumentsPierre Roux
2020-11-05[numeral notation] Handle implicit argumentsPierre Roux
2020-11-05[numeral notation] Allow to put/ignore holes during pre/postprocessingPierre Roux
This will enable to handle implicit arguments by ignoring them during preprocessing (before uninterpreting (i.e., printing)) and remplace them with holes `_` during postprocessing (after interpreting (i.e., parsing)).
2020-11-05[numeral notation] Prove RPierre Roux
2020-11-05[numeral notation] Specify RPierre Roux
2020-11-05[numeral notation] RPierre Roux
Previously real constants were parsed by an unproved OCaml code. The parser and printer are now implemented in Coq, which will enable a proof and hopefully make it easier to maintain / make evolve. Previously reals were all parsed as an integer, an integer multiplied by a power of ten or an integer divided by a power of ten. This means 1.02 and 102e-2 were both parsed as 102 / 100 and could not be tell apart when printing. So the printer had to choose between two representations : without exponent or without decimal dot. The choice was made heuristically toward a most compact representation. Now, decimal dot is parsed as a rational and exponents are parsed as a product or division by a power of ten. For instance, 1.02 is parsed as Q2R (102 # 100) whereas 102e-2 is parsed as IZR 102 / IZR (Z.pow_pos 10 2). 1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = Q2R (102 # 100) * 10 and 10.2 = Q2R (102 # 10) no longer are.
2020-11-05[numeral notation] Prove QPierre Roux
2020-11-05[numeral notation] Specify QPierre Roux
2020-11-05[numeral notation] QPierre Roux
Previously rationals were all parsed as a pair numerator, denominator. This means 1.02 and 102e-2 were both parsed as 102 # 100 and could not be tell apart when printing. So the printer had to choose between two representations : without exponent or without decimal dot. The choice was made heuristically toward a most compact representation. Now, decimal dot is still parsed as a power of ten denominator but exponents are parsed as a product or division by Z.pow_pos. For instance, 1.02 is parsed as 102 # 100 whereas 102e-2 is parsed as (102 # 1) / (Z.pow_pos 10 2 # 1). 1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = (102 # 100) * (10 # 1) = 1020 # 100 and 10.2 = 102 # 10 no longer are. A nice side effect is that exponents can no longer blow up during parsing. Previously 1e1_000_000 literally produced a numerator with a million digits, now it just yields (1 # 1) * (Z.pow_pos 10 1_000_000 # 1).
2020-11-05[numeral notation] Remove proofs for QPierre Roux
Just to get a cleaner log, this will be proved again in a few commits.
2020-11-05[numeral notation] Document the via ... using ... optionPierre Roux
2020-11-04[numeral notation] Add tests for the via ... using ... optionPierre Roux
2020-11-04Merge PR #13232: Adding an if-then-else syntax to Ltac2.Michael Soegtrop
Reviewed-by: MSoegtropIMC Ack-by: Zimmi48 Reviewed-by: jfehrle
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
This enables numeral notations for non inductive types by pre/postprocessing them to a given proxy inductive type. For instance, this should enable the use of numeral notations for R.
2020-11-04[numeral notation] Add a pre/postprocessingPierre Roux
This will enable to define numeral notation on non inductive by using an inductive type as proxy and those translations to translate to/from the actual type to the inductive type.
2020-11-04Add functions Smartlocate.global_{constant,constructor}Pierre Roux
2020-11-04Add kernel/float64.ml to gitignorePierre Roux
This is a generated file since #13147
2020-11-04Regenerate the grammar description file.Pierre-Marie Pédrot
2020-11-04Document the syntax addition.Pierre-Marie Pédrot
2020-11-04Adding an if-then-else syntax to Ltac2.Pierre-Marie Pédrot
This is a syntactic sugar that is compiled away to a simple case analysis.
2020-11-04Adding change log for #13255.Hugo Herbelin
2020-11-04Typing patterns and using type constraints in Search.Hugo Herbelin
We accept patterns that we failed to type as a fallback.
2020-11-04Adding a typed interpretation of patterns.Hugo Herbelin
2020-11-04Adding change log for #13301.Hugo Herbelin
2020-11-04Fixes #13298: primitive projections needs a correct typing environment.Hugo Herbelin
2020-11-04Merge PR #13193: [build] [native] Don't assume installed native libraries ↵coqbot-app[bot]
are in custom output path Reviewed-by: maximedenes Reviewed-by: herbelin
2020-11-04Documentation of the main entry points of uState.mli.Hugo Herbelin
2020-11-04Factorizing UState.make* through UState.from_env, to highlight the similarity.Hugo Herbelin
An alternative could also be to split the initialization of the environment and the declaration of initial "binders".
2020-11-04Moving interpretation of user-level universes in constrintern.ml.Hugo Herbelin
2020-11-04Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.Hugo Herbelin
Also some dead code. If no typo is introduced, there should be no semantic changes.
2020-11-04Merge PR #13258: Eagerly reduce rigid / flex conversion problemscoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-04Merge PR #13302: Fix test-suite in async mode.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-04Add overlays.Pierre-Marie Pédrot
2020-11-04Document the changes.Pierre-Marie Pédrot
2020-11-04Further code simplification in arbitrary hint interpretation.Pierre-Marie Pédrot
We reuse the standard code path for term interpretation instead of trying to mangle it.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 20:56:36 +0000