| Age | Commit message (Collapse) | Author |
|---|
|
There seems to have been several bugs, when -prefix is given:
- Under win32: "" instead of "lib" (presumably introduced in ab442aed8, 2006)
- Under win32: datadir, mandir, docdir should presumably be in
"share", "man", "doc", as given in default
- Under non-win32: coqdoc files should be in latex subdir not emacs subdir
|
|
|
|
"libdir" to "COQLIBINSTALL" then "libdir", then "coqlib".
For the record, here is how installation options are named at the
current time in the different places they are used (if any):
Name in Name in Name in Name of option Name in Name of option
config/Makefile coqtop -config config/coq_config.ml in configure lib/envars.ml for coqtop/coqdep
--------------------------------------------------------------------------------------------------------
COQLIBINSTALL COQLIB coqlib -libdir coqlib -coqlib
DOCDIR DOCDIR docdir -docdir docdir
CONFIGDIR configdir -configdir
DATADIR datadir -datadir
BINDIR -bindir
MANDIR -mandir
EMACSLIB -emacslib
COQDOCDIR -coqdocdir
Note: in envars.ml, docdir and coqlib are recomputed
|
|
|
|
|
|
|
|
|
|
Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug.
|
|
|
|
|
|
Deprecations which can't be fixed in 4.02.3 are locally wrapped with
[@@@ocaml.warning "-3"]. The only ones encountered are
- capitalize to capitalize_ascii and variants. Changing to ascii would
break coqdoc -latin1 and maybe other things though.
- external "noalloc" to external [@@noalloc]
|
|
This fixes Théo's bug on eset.
|
|
|
|
|
|
|
|
|
|
|
|
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
|
|
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
|
|
Forwards/backwards reasoning thoughts come from
https://github.com/coq/coq/pull/385#discussion_r111008347
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The ' was originally denoting that we were taking in the projections and
applying the constructor in the conclusion, rather than taking in the
bundled versions and projecting them out (because the projections don't
exist for [ex] and [ex2]). But we don't have versions like this for
[sig] and [sigT] and [sigT2] and [sig2], so we might as well not add the
' to the [ex] and [ex2] versions.
|
|
As per Hugo's request.
|
|
|
|
|
|
As per Hugo's suggestion in
https://github.com/coq/coq/pull/384#issuecomment-264891011
|
|
This tactic does better than [inversion] at sigma types.
|
|
|
|
As per Hugo's request.
|
|
As per Hugo's request in
https://github.com/coq/coq/pull/384#issuecomment-264891011
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
As suggested by @gares, now the meaning becomes way clearer.
|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
This is a minor cleanup.
|
|
We move Coqlib to library in preparation for the late binding of
Gallina-level references. Placing `Coqlib` in `library/` is convenient
as some components such as pretyping need to depend on it.
By moving we lose the ability to locate references by syntactic
abbreviations, but IMHO it makes to require ML code to refer to
a true constant instead of an abbreviation/notation.
Unfortunately this change means that we break the `Coqlib`
API (providing a compatibility function is not possible), however we
do so for a good reason.
The main changes are:
- move `Coqlib` to `library/`.
- remove reference -> term from `Coqlib`. In particular, clients will
have different needs with regards to universes/evar_maps, so we
force them to call the (not very safe) `Universes.constr_of_global`
explicitly so the users are marked.
- move late binding of impossible case from `Termops` to
`pretying/Evarconv`. Remove hook.
- `Coqlib.find_reference` doesn't support syntactic abbreviations
anymore.
- remove duplication of `Coqlib` code in `Program`.
- remove duplication of `Coqlib` code in `Ltac.Rewrite`.
- A special note about bug 5066 and commit 6e87877 . This case
illustrates the danger of duplication in the code base; the solution
chosen there was to transform the not-found anomaly into an error
message, however the general policy was far from clear. The long
term solution is indeed make `find_reference` emit `Not_found` and
let the client handle the error maybe non-fatally. (so they can test
for constants.
|
|
We remove redundant functions `coq_constant`, `gen_reference`, and
`gen_constant`.
This is a first step towards a lazy binding of libraries references.
We have also chosen to untangle `constr` from `Coqlib`, as how to
instantiate the reference (in particular wrt universes) is a
client-side issue. (The client may want to provide an `evar_map` ?)
c.f. #186
|
