| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Since TACTIC EXTEND relies on the usual tactic notation mechanism, the
interpretation of an ML tactic first goes through a TacAlias node. This
means that variables bound by the notation overwrite those of the current
environment. It turns out to be problematic for badly designed arguments
that close over variables of the environment, e.g. glob_constr, because
the variables used at interpretation time are now different from the ones
of parsing time.
Ideally, those arguments should return a closure made of the inner argument
together with the Ltac environment they were defined in. Unluckily, this would
need some important changes in their design. Most notably, most of ssreflect
ARGUMENT EXTEND actually create such closed arguments.
In order to emulate the old behaviour, we rather use a hack by prefixing
ML-bound variables by a character that is not accessible from user-side.
|
| | | | |
| | | |
| | | |
| | | | |
Now the casual Dyn user does not need to be a GADT guru
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Instead of rebuilding a whole set of evars just to make a typeclass filter,
we use the source evarmap.
|
| | | | | |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Amongst other things:
1. No more unsafe grammar extensions, except when going through the CAMLPX-based
Pcoq.Gram module. This is mostly safe because CAMLPX adds casts to ensure that
parsing rules are well-typed. In particular, constr notation is now based on
GADTs ensuring well-typedness.
2. Less reliance on unsafe coq inside Pcoq, and exposing a self-contained API.
The Entry module was also removed as it now results useless.
3. Purely functional API for synchronized grammar extension. This gets rid of
quite buggy code maintaining a table of empty entries to work around CAMLPX bugs.
The state modification is now explicit and grammar extensions synchronized with
the summary must provide the rules they want to perform instead of doing so
imperatively.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This made little sense, as all the uses of this function were actually
called from toplevel ML modules. This was at best useless, and at worst
a source of bugs when loading plugins and messing with backtracking.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Instead of leaving the responsibility of extending the grammar to the caller,
we ask for a list of extensions in the return value of the function.
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
This was probably wreaking havoc in tricky undo-redo scenarii.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This removes the last call to unsafe_grammar_extend, so that all handwritten
grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are
still using the unsafe interface, but as they insert explicit casts they are
deemed safe.
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| |/ / / / |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The "Classic" string is still hard coded here in there in the system, but
not in STM.
BTW, the use of an hard coded "Classic" value suggests nobody really uses
"Set Default Proof Mode" in .v files.
|
| | | | | |
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | | |
obligations".
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This patch also disables the -makecmd option and the corresponding test,
since the value is not stored for future use. This prevents gratuitously
failing to configure on FreeBSD.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
A "sentence" includes all the blank lines and all the comments that
precede a command. So its starting location might be far from any error it
contains. This patch changes error reporting so that it relies on the
location of errors rather than the location of erroneous sentences.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | |
| | | | | |
This allows a proper printing of tactic notations with special tokens
such as separators.
|
| | | | | | |
|
| | | | | | |
|
| |/ / / / |
|
| | | | | |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This brings the evaluation model of Ltac closer to those of usual languages, and
further allows the integration of static typing in the long run. More precisely,
toplevel constructed values such as lists and the like do not carry anymore the
type of the underlying data they contain.
This is mostly an API change, as it did not break any contrib outside of mathcomp.
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Although still working, it is now bad practice to use it, and it is not
widely spread anyway.
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
Hugo Herbelin
Pierre-Marie Pédrot
Enrico Tassi
Guillaume Melquiond
Pierre Letouzey