| Age | Commit message (Collapse) | Author |
|---|
|
are composed from uppercase letters
|
|
section variables.
|
|
|
|
|
|
A priori considered to be a good programming style.
|
|
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
|
|
|
|
The new function is interp_glob_closure which is basically a renaming
and generalization of interp_uconstr.
Note a change of semantics that I could however not observe in
practice.
Formerly, interp_uconstr discarded ltac variables bound to names for
interning, but interp_constr did not. Now, both discard them.
We also export the new interp_glob_closure.
|
|
This simplifies the API as before, inference of instances of type
classes was iff a type constraint was given.
We then export these both versions of interp_open_constr.
|
|
This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.
Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.
Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
|
|
|
|
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).
|
|
|
|
|
|
|
|
|
|
|
