| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We clean the hack bypassing the interpretation of "'pat" in binders
and move it to comDefinition.ml. In particular, we fix the exact
subterm to which Eval has to apply in the hack, and remove the
artificial cast we had introduced.
|
|
"similar" means sharing a scope or implicit status.
|
|
|
|
[About] still says it.
Close #9056.
|
|
You can tell which it is from the `@{}` if you really care, and seeing
`Monomorphic List (A:Type)` with no indication that `Monomorphic` is
about universes can confuse people.
|
|
|
|
This works for contexts in Definition and co, but not yet for "fun" and co.
|
|
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.
|
|
|
|
- typo in notation_ops.ml
- factorization of patterns in ppconstr.ml
- update of test-suite
- printing of cast of a binding pattern if in mode "printing all"
The question of whether or not to print the type of a binding pattern
by default seems open to me.
|
|
Supporting accordingly printing of sequences of binders including binding
patterns.
|
|
(In agreement with Daniel.)
|
|
|
