| Age | Commit message (Collapse) | Author |
|---|
|
function
|
|
function
|
|
|
|
|
|
|
|
This historical Makefile was used during the development of coqcheck,
but was unused since then : the checker is built via Coq's main Makefile.
So let's remove this one to avoid any risk of confusion.
|
|
This file was only used during ocamldebug sessions (in the dev/db
script). It was containing a large subset of the core cma files,
up to the printing functions. There were a few notable exceptions,
for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
But printers.cma was troublesome to maintain : almost each time an ML file
was added/removed/renamed in the core of Coq, dev/printers.mllib
had to be edited, in addition to the directory-specific .mllib
(kernel/kernel.mllib and co). So I propose here to kill this file,
and put instead in dev/db several "load_printer" of the core cma files.
For that to work, we need to compile kernel/kernel.cma with the right
-dllib and -dllpath options, but that shouldn't hurt (on the contrary).
We also source now the camlpX cma in dev/db, via a new generated file
dev/camlp4.dbg containing a load_printer of either gramlib.cma or
camp4lib.cma.
If one doesn't want to perform the whole "source db" at the start
of an ocamldebug session, then the former "load_printer printers.cma"
could be replaced by:
source core.dbg
load_printer top_printers.cmo
See for instance the minimal dev/base_db.
|
|
|
|
|
|
Apparently, in camlp4 (unlike camlp5) :
- Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]"
produces a kwd of type token instead of string (which sounds reasonable ?).
For now, I've replaced kwd by the explicit strings. Not so nice, but works
with both camlp4 and camlp5
- A quotation of the form "let obj = ... in bar; baz" is not
interpreted in the usual OCaml way, but rather as
"(let obj = ... in bar); baz".
Let's use instead "let obj = ... in let () = bar in baz", which works fine.
|
|
|
|
|
|
|
|
|
|
It should use evar instantiations eagerly during unification of
the lhs of the lemma, as in 8.4.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- 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.)
|
|
|
|
The same variable name was used to collect the binders and the
successive steps of matching one binder, resulting in unexpected
attempts for merging in the presence of multiple occurrence of the
same recursive pattern.
An amusing side-effect: when eta-expanding for a notation with
recursive binders, it is the second variable of the "x .. y" which is
used to invent a name rather than the first one.
|
|
|
|
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
|
|
Was triggering a deprecation warning.
|
|
It was anyway unusable due to a parsing conflict with the swap operator on
goals. Was triggering a warning when compiling the prelude.
|
|
|
|
|
|
|
|
|
|
Further work would include:
- Identify binders up to alpha-conversion (see #4932 with a list of
binders of length at least 2, or #4592 on printing notations such as
ex2).
A cool example that one could also consider supporting:
- Notation "[[ a , .. , b | .. | a , .. , b ]]" :=
(cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
|
|
immediately in the scope of another recursive pattern.
|
|
|
|
|
|
In particular, it becomes possible to have recursive patterns used
shared by binders and terms.
Currently limited by alpha-conversion issues (e.g. test2 from 4932.v
is not reprinted).
|
|
This application was actually not anticipated. It is nice and was not
too difficult to support.
Design for pattern binders maybe to clarify. When seing pat(x1,..,xn)
as a term, I just reused pat(x1,..,xn), but maybe it is worth using
the variable aliasing the pattern, for more a concise notation. But at
the same time, this means exposing the internal name of the alias
which is not so elegant.
|
|
This happens when recursive notations are used to define recursive
notations.
|
|
|
|
|
|
|
|
|
|
|
|
|
