| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Also trying to reformulate the message, distinguishing between a
variable/parameter and its name.
|
|
We want to avoid capture in "Inductive I {A} := C : forall A, I".
But in "Record I {A} := { C : forall A, A }.", non recursivity ensures
that no clash will occur.
This fixes previous commit, with which it could possibly be merged.
|
|
Was failing e.g. with
Inductive foo {A : Type} : Type := { Foo : foo }.
Note: the test-suite was using the bug in coindprim.v.
|
|
For instance, the following was failing to use the implicitness of n:
Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P.
|
|
|
|
We get rid of a complex function doing both an incremental comparison
and an effect on names (Notation_ops.compare_glob_constr).
For the effect on names, it was actually already done at the time of
turning glob_constr to notation_constr, so it could be skipped here.
For the comparison, we rely on a new incremental variant of
Glob_ops.glob_eq_constr (thanks to Gaëtan for getting rid of the
artificial recursivity in mk_glob_constr_eq).
Seizing the opportunity to get rid of catch-all clauses in
pattern-matching (as advocated by Maxime). Also make indentation
closer to the one of other functions.
|
|
This was preventing to work examples such as:
Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
|
|
There was a mistake in the conflict resolution of merge
6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 which wrongly undid the the
deletion of the file `ide/texmacspp.ml` in 6a412da , fixing here and
sorry for the problem.
|
|
|
|
make install does not install these *.cm(o|a) files either.
You could always do manually :
- make bytefiles : to build the bytecode *.cm(o|a) files
- make install-byte : to install these files
- make byte : to compile the whole development with the bytecode version
of Coq (this builds the *.cm(o|a) files, but also the .vo via coqc -byte).
Technically, the behavior of make is controlled by the OPT variable,
which could be -byte or -opt. For instance, 'make byte' corresponds to a
'make OPT:=-byte'
Note that coqdep is used with the new option "-dyndep var" : when seeing
a Declare ML Module "foo", "coqdep -dyndep var" does not decide whether to
depend on foo.cma or foo.cmxs, but rather use some Makefile variables such
as foo$(DYNLIB), whose content is later set according to $(OPT)
|
|
|
|
|
|
|
|
There was an extra trailing space in #680.
Now things display as, e.g.,
```
TEST bugs/opened/3754.v
TEST bugs/opened/4803.v (-compat 8.4)
```
instead of
```
TEST bugs/opened/3754.v ( )
TEST bugs/opened/4803.v (-compat 8.4 )
```
|
|
This allows to grant a wish by Hugo: to build coqtop.byte and prelude
with it, you could do:
make -j BEST=byte states
|
|
On a machine for which ocamlopt is available, the make world will now
perform bytecode compilation only in grammar/ (up to the syntax
extension grammar.cma), and then exclusively use ocamlopt.
In particular, make world do not build bin/coqtop.byte.
A separate rule 'make byte' does it, as well as bytecode plugins and
things like dev/printers.cma.
'make install' deals only with the part built by 'make', while a new
rule 'make install-byte' installs the part built by 'make byte'.
IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any
parallel mix of native and byte rules. These are known to crash sometimes,
see below. Instead, do rather 'make -j && make -j byte'.
Indeed, apart from marginal compilation speed-up for users not interested
in byte versions, the main reason for this commit is to discourage any
simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and
ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli,
and in case of parallel build this may happen at the very moment another
ocaml(c|opt) is accessing this .cmi. Until now, this issue has been
handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in
Makefile.build). But these hacks weren't obvious to extend to ocamlopt
-pack vs. ocamlopt -pack.
coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML
Module influences the .v.d dependency file. Possible values are:
-dyndep opt : regular situation now, depends only on .cmxs
-dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a)
-dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs
-dyndep none : interesting for coqtop with statically linked plugins
-dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d
instead of extensions .cm*, so that the choice is made in the rest of the
makefile (see a future commit about coq_makefile)
NB: two extra mli added to avoid building unecessary .cmo during 'make world',
without having to use the ocamldep -native option.
NB: we should state somewhere that coqmktop -top won't work unless
'make byte' was done first
|
|
|
|
We only want an absolute path, no need to follow symlinks.
|
|
This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).
Incidentally updating output of Show output test (evar numbers shifted).
|
|
|
|
Includes fixes and suggestions from Théo.
|
|
|
|
evars.
This is for consistency with the rest of the language. For instance,
"eremember" and "epose" are supposed to refer to terms occurring in
the goal, hence not leaving evars, hence in general pointless.
Eventually, I guess that "e" should be a modifier (see e.g. the
discussion at #3872), or the difference is removed.
|
|
a goal with unresolved evars.
|
|
upper-case
At the moment, when one tries to add an Ocaml module to Coq code-base
which is composed just from upper-cases letters,
the compilation fails with an error:
File "......ml", line 1:
Error: Error while linking ...
Reference to undefined global `FOO'
This commit removes the restriction.
|
|
|
|
more uniform
|
|
|
|
would write that code
|
|
|
|
|
|
|
|
|
|
Two issues in one:
- some focused_simpl were called on the wrong locations
- some focused_simpl were done on whole equations
In the two cases, this could be bad if "simpl" goes too far
with respect to what omega expects: later calls to "occurrence"
might fail. This may happen for instance if an atom isn't a variable,
but a let-in (b:=5:Z in the example).
|
|
|
|
|
|
|
|
|
|
|
|
others.
|
|
|
|
This allows to share the test for possible relocalisation done in envars.ml.
|
|
Also standardizing the choice of the default datadir (I don't see why
we should add by default both /usr/local/share/coq and /usr/share/coq
when we know that the installation is in only one of them).
Open question: test for possible relocation of the installed coq
should be done on raw dirname of the executable or on the
standardization of this name wrt symbolic links?
|
|
This allows to centralize in the configuration file the description of
the 3 possible installation layouts (dispatched over directories
shared by multiple application as in unix, self-contained style like
in windows, local non-installation as with option -local).
Also supporting relocalisation when -prefix or -libdir and co is given.
|
|
This goes towards an approach where a local layout can be seen as an
installed layout.
|
|
Constrintern.pf_global returns a global_reference, not a constr,
adapt plugins accordingly, properly registering universes where
necessary.
|
|
Consequence: docdir is always defined, no more "" in external
preferences for manual and stdlib when using coqide in -local mode.
|
|
They were not used for looking for coqide files in the situation when
the effective installation path happens to be exactly the installation
path proposed by default, while relevant files were however (possibly)
installed in these directories.
|
|
installation paths in unix or win32.
There are two layouts (self-contained or unix-like) and we build
absolute paths from them. Under unix, there is a fully relative layout
(when user gives a prefix) and a standard semi-relative layout (where
most file are under /usr/local with the absolute /etc/xdg/coq as an
exception).
I respected the existing semantics that under cygwin, the unix layout
is the default one when prefix is not given, but the self-contained
layout is the default one when a prefix is given.
|
