| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
The parsing rules were broken and disallowed tactic replacement of the form
Ltac ident ::= expr.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.
The original definition allowed us to represent non-sensical value such as:
VernacDeclareTacticDefinition(Qualid ..., false, ...)
The new definition prevents that.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
Pierre-Marie Pédrot
Matej Kosik
Hugo Herbelin
Guillaume Melquiond
Enrico Tassi
Matthieu Sozeau
Maxime Dénès