aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Merge PR #6903: [compat] Remove "Shrink Abstract"Gravatar Maxime Dénès2018-03-08
|\
* \ Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Maxime Dénès2018-03-08
|\ \
* \ \ Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Gravatar Maxime Dénès2018-03-07
|\ \ \
* \ \ \ Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\ \ \ \
* \ \ \ \ Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \
| | | | | * [compat] Remove "Shrink Abstract"Gravatar Emilio Jesus Gallego Arias2018-03-06
| |_|_|_|/ |/| | | | | | | | | | | | | | Following up on #6791, we the option "Shrink Abstract".
* | | | | Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | a record.
| | | | | * ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Enrico Tassi2018-03-06
| | | | | |
* | | | | | Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ | |_|_|_|_|_|/ |/| | | | | |
| | | | | * | CHANGES and tests for with Definition @{univs}Gravatar Gaëtan Gilbert2018-03-05
| | | | | | |
| | | | * | | Sanitize universe declaration in Context (stop using a ref...)Gravatar Gaëtan Gilbert2018-03-05
| | | | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When there is more than one variable to declare we stop trying to attach global universes (ie monomorphic or section polymorphic) to one of them.
* | | | | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \
| | | * | | | [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| | | | |/ / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
| | * / | | Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| | |/ / /
| | | | * ssr: add Prenex Implicits for Some_inj to use it as a viewGravatar Anton Trunov2018-03-04
| | | |/ | | |/|
* | | | Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \
* \ \ \ \ Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | size.
* \ \ \ \ \ Merge PR #915: Fix rewrite in * side conditionsGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
| | | | * | | Removing test for bug #2850.Gravatar Pierre-Marie Pédrot2018-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This test was actually checking that evar-containing terms were making the VM fail. Obviously this is not the case anymore, so the test is now invalid.
| | | | * | | Adding a test file for evar handling in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
| | | | | | |
| | | * | | | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | | | | | |
| | | * | | | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
| | | | | | |
| | | * | | | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
| | | |/ / / | | | | | | | | | | | | | | | | | | Fix new deprecation warnings in the standard library.
| | * / / / Fix #6878: univ undefined for [with Definition] bad instance size.Gravatar Gaëtan Gilbert2018-03-01
| | |/ / /
| * / / / Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| |/ / / | | | | | | | | | | | | Noticed by Sigurd Schneider.
* / / / [test-suite] Add a basic test-case for `Load`.Gravatar Emilio Jesus Gallego Arias2018-02-28
|/ / / | | | | | | | | | | | | | | | | | | We test the 3 possible scenarios. A more complete test would also involved fake_ide. c.f. #6793
* | | Merge PR #6756: Fix issue with spurious timing test failuresGravatar Maxime Dénès2018-02-28
|\ \ \
* \ \ \ Merge PR #6823: Fixes #6821 (bug in protecting notation printing from ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ | | | | | | | | | | | | | | | infinite eta-expansion)
| | | * | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |_|/ / |/| | |
| | * | [test-suite] Move sed scripts into bash arraysGravatar Jason Gross2018-02-24
| | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/6756/files#r168028764
* | | | Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\ \ \ \
* \ \ \ \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ \
| | | * | | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Gravatar Hugo Herbelin2018-02-23
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | More precisely when matching "f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z" do not allow expansion of f since otherwise, we recursively have to match "f t" with the same pattern.
* | | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \
* \ \ \ \ \ Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just ↵Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | the concl
* \ \ \ \ \ \ \ Merge PR #6740: Adding a sanity check on inductive variance subtyping.Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \
| | | | | * | | | Update SearchPattern.out for numeral notationsGravatar Jason Gross2018-02-20
| |_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There is more churn than there should be because SearchPattern uses a non-local sorting algorithm; the comparison function considers many constants equal in priority and leaves it up to the heap structure to break ties, which seems wrong. This has been reported as [bug #5573](https://coq.inria.fr/bugs/show_bug.cgi?id=5573).
| | | | | * | | Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Hugo Herbelin2018-02-20
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Computation of the sort of the inductive type was done before ensuring that the arguments of the inductive type had the correct types, possibly brutally failing with `NotArity` in case one of the types expected to be typed with an arity was not so.
| | | * | | | Adding a test for wish #5532.Gravatar Hugo Herbelin2018-02-20
| | | | | | |
| | | * | | | Trying a hack to support {'pat|P} without breaking compatibility.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Concretely, we bypass the following limitation: The notation "{ ' pat | P }" broke the parsing of expressions of the form "{ forall x, P } + { Q }". Indeed the latter works thanks to a tolerance of Camlp5 in parsing "forall x, P" at level 200 while the rule asks to actually parse the interior of "{ ... }" at level 99 (the reason for 99 is to be below the rule for "M : T" which is at level 100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke the tolerance for constr at level 200. We fix this by adding an ad hoc rule for "{ binder_constr }" in the native grammar (g_constr.ml4). Actually, this is inconsistent with having a rule for "{ constr at level 99 }" in Notations.v. We should have both rules in Notations.v or both rules hard-wired in the native grammar. But I still don't know what is the best decision to take, so leaving as it at the current time. Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in metasyntax.ml (no need to ensure that the rule exist). Disadvantages: if one wants a different initial state without the business needing the "{ }" for sumbool, sumor, sig, sigT, one still have the rules there. Advantages of having them in Notations.v: more modular, we can change the initial state. Disadvantages: one would need a new kind of modifier, something like "x at level 99 || binder_constr", with all the difficulty to find a nice, intuitive, name for "binder_constr", and the difficulty of understanding if there is a generality to this "||" disjunction operator, and whether it should be documented or not.
| | | * | | | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Gravatar Hugo Herbelin2018-02-20
| | | | | | |
| | | * | | | Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | For compatibility, the default is to parse as ident and not as pattern.
| | | * | | | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}.
| | | * | | | When printing a notation with "match", more flexibility in matching equations.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We reason up to order, and accept to match a final catch-all clauses with any other clause. This allows for instance to parse and print a notation of the form "if t is S n then p else q".
| | | * | | | Adding general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This now works not only for parsing of fun/forall (as in 8.6), but also for arbitraty notations with binders and for printing.
| | | * | | | Using an "as" clause when needed for printing irrefutable patterns.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Example which is now reprinted as parsed: fun '((x,y) as z) => (y,x)=z
| | | * | | | Refining the strategy for glueing let-ins to a sequence of binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To deal with existing notations starting with a "let" (see notation "for" in output/Notation2.v) we adopt the pragmatic approach of glueing only inner let by default. Ideally, it might be nicer to detect if there is an overlap of notation, and not to glue only in case of overlap. We could also decide that a notation starting with a "let" should always be protected by some constant, say "id", so as to avoid possible collisions, but this would require changes user side.
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-09 08:24:29 +0000