aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2020-11-04Do not try to be clever for term-as-hint interpretation.Pierre-Marie Pédrot
The prepare_hint function was trying to requantify over all undefined evars, but actually this should not happen when defining generic terms as hints through some Hint vernacular command.
2020-11-04Opacify the Hints.hint_term type.Pierre-Marie Pédrot
2020-11-04Encapsulate the last use of IsConstr in the Hints API.Pierre-Marie Pédrot
2020-11-04Further API cleanup after the removal of forward hints.Pierre-Marie Pédrot
We know statically that only global references are passed to make_resolves.
2020-11-04Remove warning on SSR Search having moved.Théo Zimmermann
2020-11-03Merge PR #13293: Doc: added "Arguments" removing implicit argumentscoqbot-app[bot]
Reviewed-by: jfehrle Reviewed-by: Zimmi48
2020-11-03Merge PR #13132: Understand Mangle Names in implicit generalizationcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13179: Fix printing for empty primitive arrayscoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13256: Remove test-suite/bugs/opened/bug_3395.v: not a bugcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding ↵coqbot-app[bot]
notations in patterns Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: LasseBlaauwbroek
2020-11-03improved documentation of arguments commandFabian Kunze
2020-11-03Eagerly reduce rigid/flex conversion problems.Pierre-Marie Pédrot
2020-11-03Add a fast path in CClosure stack zipping.Pierre-Marie Pédrot
No need to zip the stack if the machine has made no progress.
2020-11-03Fix test-suite in async mode.Théo Zimmermann
(By closing unfinished proofs.)
2020-11-02Nicer spacing when printing array literalsGaëtan Gilbert
From [|x; y; z | def : ty |] to [| x; y; z | def : ty |]
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 12:20:44 +0000