| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Originally, "VernacTime" and "VernacRedirect" were defined like this:
type vernac_expr =
...
| VernacTime of vernac_list
| VernacRedirect of string * vernac_list
...
where
type vernac_list = located_vernac_expr list
Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:
| VernacTime of located_vernac_expr
| VernacRedirect of string * located_vernac_expr
which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.
|
| | | | |
|
| | | |
| | |
| | |
| | | |
all cases of rewrite.
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
Marking it as experimental.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
based on a suggestion of Guillaume M. (done like this in ssreflect).
This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
|
| | | | |
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
The fix was actually elementary. The lexer comes with a function to
compare parsed tokens against tokens of the parsing rules. It is
enough to have this function considering an ident in a parsing rule to
be equal to the corresponding string parsed as a keyword.
|
| |\| | |
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
(Fix bug #3654)
|
| | | |
| | |
| | |
| | |
| | | |
Without this expansion, camlp4 fails to properly factor a user notation
starting with either "trivial" or "auto".
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Entries defined in the Pcoq AST of symbols must be marshallable, because they
are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as
they contain functional values. This is why the Pcoq module used a pair
[string * string] to describe entries. It is obviously type-unsafe, so
we define a new abstract type in its own module. There is a little issue
though, which is that our entries and CAMLP4/5 entries must be kept
synchronized through an association table. The Pcoq module tries to
maintain this invariant.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\| | |
|
| | | | |
|
| | | | |
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
| | | |
| | |
| | |
| | |
| | | |
There is no such thing as the OPTSEP macro in Camlp4 so I had
to expand it by hand.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | | |
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
This (at least technically) solves the issue #4113 (see also #4329).
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)). It is
useful to have function_scope for, e.g., function composition. This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.
Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax. (The scope type_scope
should not be special-cased; this change is coming up next.)
Also explicitly define [function_scope] in theories/Init/Notations.v.
This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]
We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.
|
| |\| |
|
| | |
| |
| |
| |
| | |
The file seems to have been reintroduced by error by commit 012fe1a96, but
it was not compiled anyway.
|
Matej Kosik
Hugo Herbelin
Pierre-Marie Pédrot
Guillaume Melquiond
Enrico Tassi
Matthieu Sozeau
Maxime Dénès
Jason Gross