aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Collapse)AuthorAge
* Making explicit that errors happen in one of five executation phases.Gravatar Hugo Herbelin2018-05-02
| | | | | | | | | | The five phases are command line interpretation, initialization, prelude loading, rcfile loading, and sentence interpretation (only the two latters are located). We then parameterize the feedback handler with the given execution phase, so as to possibly annotate the message with information pertaining to the phase.
* Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while ↵Gravatar Emilio Jesus Gallego Arias2018-04-09
|\ | | | | | | looking for a notation for a nested pattern
* \ Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Gravatar Maxime Dénès2018-04-09
|\ \
* \ \ Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Gravatar Hugo Herbelin2018-04-04
|\ \ \
| | * | ssr: check cleared hyps do exist (fix #7050)Gravatar Enrico Tassi2018-04-04
| | | |
* | | | Fix #6404 - Print tactics called by ML tacticsGravatar Jason Gross2018-04-02
| |/ / |/| |
| * | Fix #6257: anomaly with Printing Projections and Context.Gravatar Gaëtan Gilbert2018-03-30
|/ / | | | | | | | | | | | | | | | | | | | | | | Constrextern.explicitize expected that if implicits were declared they would be declared at least up to the principal argument of the projection, but Context/discharge of implicits does not preserve this. Note the anomaly only happens with primitive projections DISABLED in recent Coqs (>=8.8). Implicit argument experts may consider whether ensuring enough implicits are declared would be better.
| * Fixes #7110 ("as" untested while looking for notation for nested patterns).Gravatar Hugo Herbelin2018-03-29
| |
* | Slightly refining some error messages about unresolvable evars.Gravatar Hugo Herbelin2018-03-24
|/ | | | For instance, error in "Goal forall a f, f a = 0" is now located.
* Revert "Merge PR #873: New strategy based on open scopes for deciding which ↵Gravatar Maxime Dénès2018-03-09
| | | | | | | notation to use among several of them" This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
* Merge PR #6895: [compat] Remove "Refolding Reduction" option.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6945: Fix error with univ binders on monomorphic records.Gravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsGravatar Maxime Dénès2018-03-08
|\ \ \
| | | * [compat] Remove "Refolding Reduction" option.Gravatar Emilio Jesus Gallego Arias2018-03-08
| |_|/ |/| | | | | | | | | | | | | | | | | Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895.
| | * Fix error with univ binders on monomorphic records.Gravatar Gaëtan Gilbert2018-03-08
| |/ |/| | | | | | | | | | | Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were declared twice for all records. Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an observable error for monomorphic records.
* | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \
| * | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | Fix new deprecation warnings in the standard library.
* | | [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 #6823: Fixes #6821 (bug in protecting notation printing from ↵Gravatar Maxime Dénès2018-02-28
|\ \ | | | | | | | | | infinite eta-expansion)
* \ \ 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.
| | * Adding mention of shelved/given-up status in "Show Existentials".Gravatar Hugo Herbelin2018-02-22
| |/ |/| | | | | | | | | Also changed the API of pr_subgoals now using labels. Also removed a trailing space in printing existentials.
| * 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).
* | 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.
* | A (significant) simplification in printing notations with recursive binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For historical reasons (this was one of the first examples of notations with binders), there was a special treatment for notations whose right-hand side had the form "forall x, P" or "fun x => P". Not only this is not necessary, but this prevents notations binding to expressions such as "forall x, x>0 -> P" to be used in printing. We let the general case absorb this particular case. We add the integration of "let x:=c in ..." in the middle of a notation with recursive binders as part of the binder list, reprinting it "(x:=c)" (this was formerly the case only for the above particular case). Note that integrating "let" in sequence of binders is stil not the case for the regular "forall"/"fun". Should we?
* | Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
| |
* | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms.
* | Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"...
* | In printing notations with "match", reasoning up to the order of clauses.Gravatar Hugo Herbelin2018-02-20
| |
* | Supporting recursive notations reversing the left-to-right order.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | Seizing this opportunity to generalize the possibility for different associativity into simply reversing the order or not. Also dropping some dead code. Example of recursive notation now working: Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A).
* | Allowing variables used in recursive notation to occur several times in pattern.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | This allows for instance to support recursive notations of the form: Notation "! x .. y # A #" := (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..) (at level 200, x binder).
* | Allows recursive patterns for binders to be associative on the left.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | This makes treatment of recursive binders closer to the one of recursive terms. It is unclear whether there are interesting notations liable to use this, but this shall make easier mixing recursive binders and recursive terms as in next commits. Example of (artificial) notation that this commit supports: Notation "! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder).
* | Fixing/improving notations with recursive patterns.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - The "terminator" of a recursive notation is now interpreted in the environment in which it occurs rather than the environment at the beginning of the recursive patterns. Note that due to a tolerance in checking unbound variables of notations, a variable unbound in the environment was still working ok as long as no user-given variable was shadowing a private variable of the notation - see the "exists_mixed" example in test-suite. Conversely, in a notation such as: Notation "!! x .. y # A #" := ((forall x, True), .. ((forall y, True), A) ..) (at level 200, x binder). Check !! a b # a=b #. The unbound "a" was detected only at pretyping and not as expected at internalizing time, due to "a=b" interpreted in context containing a and b. - Similarly, each binder is now interpreted in the environment in which it occurs rather than as if the sequence of binders was dependent from the left to the right (such a dependency was ok for "forall" or "exists" but not in general). For instance, in: Notation "!! x .. y # A #" := ((forall x, True), .. ((forall y, True), A) ..) (at level 200, x binder). Check !! (a:nat) (b:a=a) # True #. The illegal dependency of the type of b in a was detected only at pretyping time. - If a let-in occurs in the sequence of binders of a notation with a recursive pattern, it is now inserted in between the occurrences of the iterator rather than glued with the forall/fun of the iterator. For instance, in: Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). Check exists_true '(x,y) (u:=0), x=y. We now get exists '(x, y), True /\ (let u := 0 in True /\ x = y) while we had before the let-in breaking the repeated pattern: exists '(x, y), (let u := 0 in True /\ x = y) This is more compositional, and, in particular, the printer algorithm now recognizes the pattern which is otherwise broken.
* | Using name given by user to name a 'pat, if any.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | This works for contexts in Definition and co, but not yet for "fun" and co.
* | Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
* | Adding support for re-folding notation referring to isolated "forall '(x,y), t".Gravatar Hugo Herbelin2018-02-20
|/ | | | Was apparently forgotten in a67bd7f9.
* Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\
* \ Merge PR #6418: More detailed error messages for Canonical Structure, #6398Gravatar Maxime Dénès2018-02-12
|\ \
| * | More detailed error messages for Canonical Structure, #6398Gravatar Paul Steckler2018-02-06
| | |
* | | Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
|/ / | | | | | | | | | | | | | | | | | | | | | | | | There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems.
* | add optimize_heap tactic for #6488Gravatar Paul Steckler2018-01-03
| |
* | Merge PR #6234: Make the micromega extraction check a regular output test.Gravatar Maxime Dénès2017-12-20
|\ \
* | | Make [abstract] nodes show up in the Ltac profileGravatar Jason Gross2017-12-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This closes #5082 and closes #5778, but makes #6404 apply to `abstract` as well as `transparent_abstract`. This is unfortunate, but I think it is worth it to get `abstract` in the profile (and therefore not misassign the time spent sending the subproof to the kernel). Another alternative would have been to add a dedicated entry to `ltac_call_kind` for `TacAbstract`, but I think it's better to just deal with #6404 all at once. The "better" solution here would have been to move `abstract` out of the Ltac syntax tree and define it via `TACTIC EXTEND` like `transparent_abstract`. However, the STM relies on its ability to recognize `abstract` and `solve [ abstract ... ]` syntactically so that it can handle `par: abstract`. Note that had to add locations to `TacAbstract` nodes, as I could not figure out how to call `push_trace` otherwise.