| Age | Commit message (Collapse) | Author |
|---|
|
etc. (source of incompatibility).
|
|
|
|
|
|
More results on set_remove, in particular explicit the NoDup
pre-condition. Show that NoDup is preserved by other operations.
|
|
|
|
|
|
This reverts commit 5f49780b395686cdfce7126438c6dd69712d5c70.
|
|
Conflicts:
tools/coq_makefile.ml
|
|
|
|
Solves an efficiency problem in Makefiles generated by coq_makefile.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In particular document the "once" behaviour.
|
|
In particular try to avoid the use of the word "backtracking" which refers to too many things.
|
|
|
|
- gfail
- multimatch
- tryif/then/else
|
|
|
|
|
|
|
|
In particular document the "once" behaviour.
|
|
In particular try to avoid the use of the word "backtracking" which refers to too many things.
|
|
|
|
- gfail
- multimatch
- tryif/then/else
|
|
|
|
So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed)
|
|
|
|
|
|
This is a follow-up on Pierre's 5d80a385.
|
|
|
|
|
|
|
|
|
