aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: erikmd
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-27Merge PR #11848: Nicer printing for decimal constantsHugo Herbelin
Reviewed-by: herbelin
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-26Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlibHugo Herbelin
Reviewed-by: herbelin
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
2020-03-25Nicer printing for decimal constants in QPierre Roux
Print 1.5 as 1.5 and not 15e-1. We choose the shortest representation with tie break to the dot notation (0.01 rather than 1e-3). The printing remains injective, i.e. 12/10 is not mixed with 120/100, the first being printed as 1.2 and the last as 1.20.
2020-03-25Nicer printing for decimal constants in RPierre Roux
Print 1.5 as 1.5 and not 15e-1. We choose the shortest representation with tie break to the dot notation (0.01 rather than 1e-3). The printing remains injective, i.e. 12*10^2 is printed 12e2 in order not to mix it with 1200 and 12/10^1 is not mixed with 120/10^2, the first being printed as 1.2 and the last as 1.20.
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
They were defined at level 70, no associativity in all but three places, where they were instead declared at level 35. Fixes #11890
2020-03-22Testing notations which are specific numerals.Hugo Herbelin
2020-03-22Adding a test for printing single characters.Hugo Herbelin
Originally from bedrock2.
2020-03-22Test-suite: Assume coqtop output is text even with non-printable characters.Hugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares
2020-03-20Merge PR #11847: Properly thread let-bindings in Funind principle construction.Pierre Courtieu
Reviewed-by: Matafou
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
Unfortunately, we cannot go further and parse Export as a legacy attribute because this syntax conflicts with the Export command.
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
Ack-by: herbelin
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: ppedrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Adding a round-trip test for binders.Pierre-Marie Pédrot
2020-03-18Actually use the binder type for Ltac2 that should be used in the kernel.Pierre-Marie Pédrot
That is, it contains the type of the binder so as not to rely on the relevance explicitly.
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Export the user-facing attribute for hint locality.Pierre-Marie Pédrot
2020-03-18Change some ouput tests due to the printing of implicitsSimonBoulier
2020-03-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
Fixes #11846: Funind fails to generate principles for terms with let bindings.
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-17Add test for PR11811 (disable a positivity check)SimonBoulier
2020-03-16Document coq_makefile behavior wrt -native-compiler yesPierre Roux
2020-03-16Fix coq-makefile/native1 testPierre Roux
This was accidentaly disabled by #6264 when no_native_compiler was renamed to native_compiler. Moreover, the (then unactivated test) was broken by commit 48ae6ce (part of #9088).
2020-03-14Fixes #11692 (clear dependent knows about let-in).Hugo Herbelin
2020-03-14Merge PR #10858: Implementing postponed constraints in TC resolutionGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
A constraint can be stuck if it does not match any of the declared modes for its head (if there are any). In that case, the subgoal is postponed and the next ones are tried. We do a fixed point computation until there are no stuck subgoals or the set does not change (it is impossible to make it grow, as asserted in the code, because it is always a subset of the initial goals) This allows constraints on classes with modes to be treated as if they were in any order (yay for stability of solutions!). Also, ultimately it should free us to launch resolutions more agressively (avoiding issues like the ones seen in PR #10762). Add more examples of the semantics of TC resolution with apply in test-suite Properly catch ModeMatchFailure on calls to map_e* Add fixed bug 9058 to the test-suite Close #9058 Add documentation Fixes after Gaëtan's review. Main change is to not use exceptions for control-flow Update tactics/class_tactics.ml Clearer and more efficient mode mismatch dispatch Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> Remove exninfo argument
2020-03-12Merge PR #11798: Tests make bytecodeEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-03-11Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constantsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-11Merge PR #11786: Fix #11730: Mangle Names vs InfixPierre-Marie Pédrot
Reviewed-by: herbelin Reviewed-by: ppedrot
2020-03-10test coq-makefile/findlib-package-unpacked: only try to invoke 'make' whenRalf Treinen
there is an ocamlopt compiler.
2020-03-10test coq-makefile/camldep: try to build a cmx only when there is an ocamloptRalf Treinen
compiler. In any case, try to build a cmo file.
2020-03-10Fixing little bug in parsing decimal numbers in R.Hugo Herbelin
2020-03-09Fix #11730: Mangle Names vs InfixGaëtan Gilbert
2020-03-09Fix #9930: "change" replaces 0-param projections by constantsGaëtan Gilbert
2020-03-08Merge PR #11740: Ltac2: Add notation for enough and eenoughPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-06Merge PR #11698: Fix #11592: Side effect safety may be broken by universe ↵Gaëtan Gilbert
effects Reviewed-by: SkySkimmer
2020-03-06Merge PR #11723: Fix mishandling of sigma in guess_elim (regression from 8.11)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-06Adding a test to the test-suite.Pierre-Marie Pédrot
We take inspiration and code from the Evil plugin.
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ↵Pierre-Marie Pédrot
following the model of `pose (x:=t)`. Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-03-05Merge PR #11602: Adding support for an "only parsing" modifier in ↵Pierre-Marie Pédrot
"where"-based notation Reviewed-by: Zimmi48 Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-03-04Merge PR #11715: Be robust in calculating visible ids for non-registered ↵Hugo Herbelin
constants. Reviewed-by: herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 01:42:23 +0000