| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | |
| | | |
| | | | |
This way, it's not eaten by a section
|
| | |/ /
| | |
| | | |
This definition was removed by a4043608f704f026de7eb5167a109ca48e00c221 (This commit adds full universe polymorphism and fast projections to Coq), for reasons I do not know. This means that things like `unfold option_map` work only in 8.5, while `unfold <application of Facts>.option_map` works only in 8.4. This allows `unfold` to work correctly in both 8.4 and 8.5.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We don't actually need to, unless we want to support the (presumably
uncommon) use-case of someone using [Import VectorNotations] to override
their local notation for things in vector_scope.
Additionally, we now maintain the behavior that [Import VectorNotations]
opens vector_scope.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In coqtop, one could do for instance:
Require Import Top. (* Where Top contains a Definition b := true *)
Lemma bE : b = true. Proof. reflexivity. Qed.
Definition b := false.
Lemma bad : False. Proof. generalize bE; compute; discriminate. Qed.
That proof could however not be saved because of the circular dependency check.
Safe_typing now checks that we are not requiring (Safe_typing.import) a library
with the same logical name as the current one.
|
| | | |
| | |
| | |
| | | |
This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.
Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.
|
| | | |
| | |
| | |
| | |
| | | |
Coqc now expects physical names for input files, so fix coq_makefile
accordingly.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
changing
set (x := val)
into
let x := fresh "x" in
set (x := val)
|
| | | | |
|
| |\ \ \
| | | |
| | | |
| | | | |
Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
|
| | | |\ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
match.""
We apply this patch to trunk so that it is integrated in 8.6.
This reverts commit 0eb08b70f0c576e58912c1fc3ef74f387ad465be.
|
| |\ \ \ \ \
| | |/ / /
| |/| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This fixes the end of bug #4069, provoked by a use
of unshelve refine which introduces a cast.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
not in pl2.
|
| | | | | | |
|
| | | |/ /
| |/| |
| | | |
| | | |
| | | |
| | | | |
We apply this patch to trunk for integration in 8.6 instead.
This reverts commit 715f547816addf3e2e9dc288327fcbcee8c6d47f.
|
| | | | | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Was PR#228: fix coqide double module linking (error on OCaml 4.03)
Fixes #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings
triggered by CoqIDE
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This was implemented in anticipation of a part of PR#164 that we decided not to
merge.
|
| | | | | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#226: CErrors & CClosure
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
lib/cErrors.ml)
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |/ / / / / |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Was PR#231: Separate flags for fix/cofix/match reduction and clean reduction
function names, itself a revision of PR#117: Isolating flags for cofix/fix
reduction + adjusting names of reduction functions to what they do
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
whd_zeta now takes an evar_map and looks in evar instances. This changes
the behavior of whd_zeta e.g. on let x := ?t in x
|
| | | | | | | |
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is a reimplementation of Hugo's PR#117.
We are trying to address the problem that the name of some reduction functions
was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in
reduction). Like PR#117, we are careful that no function changed semantics
without changing the names. Porting existing ML code should be a matter of
renamings a few function calls.
Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX
collectively denominated iota.
We renamed the following functions:
Closure.betadeltaiota -> Closure.all
Closure.betadeltaiotanolet -> Closure.allnolet
Reductionops.beta -> Closure.beta
Reductionops.zeta -> Closure.zeta
Reductionops.betaiota -> Closure.betaiota
Reductionops.betaiotazeta -> Closure.betaiotazeta
Reductionops.delta -> Closure.delta
Reductionops.betalet -> Closure.betazeta
Reductionops.betadelta -> Closure.betadeltazeta
Reductionops.betadeltaiota -> Closure.all
Reductionops.betadeltaiotanolet -> Closure.allnolet
Closure.no_red -> Closure.nored
Reductionops.nored -> Closure.nored
Reductionops.nf_betadeltaiota -> Reductionops.nf_all
Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
Reductionops.whd_betadeltaiota -> Reductionops.whd_all
Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
Reductionops.whd_eta -> Reductionops.shrink_eta
Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all
And removed the following ones:
Reductionops.whd_betaetalet
Reductionops.whd_betaetalet_stack
Reductionops.whd_betaetalet_state
Reductionops.whd_betadeltaeta_stack
Reductionops.whd_betadeltaeta_state
Reductionops.whd_betadeltaeta
Reductionops.whd_betadeltaiotaeta_stack
Reductionops.whd_betadeltaiotaeta_state
Reductionops.whd_betadeltaiotaeta
They were unused and having some reduction functions perform eta is confusing
as whd_all and nf_all don't do it.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
But there are still bugs with Declare Implicit Tactic, which should
probably rather be reimplemented with ltac:(tac).
Indeed, it does support evars in the type of the term, and
solve_by_implicit_tactic should transfer universe constraints to the
main goal. E.g., the following still fails, at Qed time.
Definition Foo {T}{a : T} : T := a.
Declare Implicit Tactic eassumption.
Goal forall A (x : A), A.
intros.
apply Foo.
Qed.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This allows to grant a wish by Hugo: to build coqtop.byte and prelude
with it, you could do:
make -j BEST=byte states
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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)
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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 next commit about coq_makedile)
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
|
| | | | |
| | | |
| | | |
| | | | |
See 4865.v for details.
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
Jason Gross
Jason Gross
Maxime Dénès
Matthieu Sozeau
Guillaume Melquiond
thery
Matej Kosik
Matthieu Sozeau
Pierre Letouzey
Hugo Herbelin