| Age | Commit message (Collapse) | Author |
|---|
|
Renouncing to bypass the library path given by "camlp5o -where" what
we assume to be the default library location, considering that
-usecamlp5dir is here to deal with the non-standard installation
layout.
Renouncing to find camlp5 libraries in a subdirectory of the ocaml
library directory since we now know that camlp5o is found and that we
have a priori to trust option -where of camlp5o.
Additionally falling back on looking for camlp4 if a camlp5 library is
found but no camlp5 binary. Also using camlp5o as a reference since
after all this is camlp5o that we need.
In particular, this fixes situations where -usecamlp5dir is given but
"camlp5o -where" contradicts it.
If something has to be checked on windows, please tell.
|
|
Now, type_scope is consistently used whether it is an hypothesis or
the conclusion, and consistently not used when in "context".
The question of a compatibility support, e.g., as suggested by Jason,
using a scope is still open though.
See reports #3050 and #4398.
|
|
on the contrary of message given in 23041481f, while it introduces a
square time complexity of the size of the goal in subterm finding.
|
|
The error message was not only causing coqtop to exit, but also coqide to
crash, which led to a rather poor user experience. Since the code does not
actually care about the file extension, this commit just removes the test.
|
|
We delay the externalization of application arguments in Constrextern,
so that they only get computed when they are actually explicitly displayed.
|
|
The COQLIBS variable contains some -Q and -I options, which are not
supported by the checker. So this commit introduces a COQCHKLIBS variable
that contains the proper options for coqchk. For the sake of homogeneity,
the COQDOCLIBS variable is also preprocessed in the same way. This means
that both variables have the same value, but they are kept separate in
case the user would like to override one and not the other.
This commit also removes some deprecated options from "coqchk --help".
They are not removed from coqchk itself to preserve backward compatibility
in the branch.
An open question is whether coqchk should support dummy options such as -Q
(interpreted as -R) or -I (ignored).
|
|
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
g I. (* Was printing Top.Top#<>#1 *)
idtac; f I. (* Was not properly locating error *)
This is a "a minima" fix.
This a different fix than in trunk, so the merge will have to take the
trunk version.
|
|
Since d09def34, only the summary of libraries was included in the checksum, not
the actual content of the library. This quick fix performs the checking of the
checksum immediately, even if the loading is delayed.
|
|
|
|
#4770).
This also fixes comments not being properly skipped when looking for eol.
|
|
As a side effect, there should be a small speedup when ignoring comments.
This commit also fixes two bugs related to handling "$$" and "#" in
comments.
|
|
|
|
This brings a 10x speedup for going at the end of large .v files.
|
|
If the second allocation causes a collection of the minor heap, the first
allocation will be freed, thus causing a memory corruption.
Note: it only happens when computing the native projection of an opaque
value while the minor heap is almost full.
|
|
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
|
|
|
|
Some dubious evarmap manipulation is going on in destruct because of the
use of clenv primitives. Here, building a clenv was introducing new evars
that were not taken into account in the remainder of the tactic. We plug
them back using a local workaround.
Eventually, this code should be replaced by an evar-based one, but meanwhile,
we rely on what is probably a hack.
|
|
Command line options to be dropped got outdated after vi -> vio renaming.
This made the par: goal selector do not work in conjunction with -quick.
|
|
Return the most appropriate evar_map for commands that can run on
non-focused proofs (like Check, Show and debug printers) so that
universes and existentials are printed correctly (they are global
to the proof). The API is backwards compatible.
|
|
|
|
Use the compatibility match construction to extract the compatibility
constant associated to a primitive projection.
|
|
Fix handling of non-polymorphic hints built from polymorphic values, or
simply producing new universes. We have to record the side effects of
global hints built from constrs which are not polymorphic when they
declare global universes, which might need to be discharged at the end
of sections too. Also issue a warning when a Hint is declared for a
polymorphic reference but the Hint isn't polymorphic itself (this used
to produce an anomaly). For [using] hints, treat all lemmas as
polymorphic, refreshing their universes at each use, as is done for
their existentials (also used to produce an anomaly).
|
|
Anomaly: Uncaught exception Unix.Unix_error(Unix.EACCES, "open", "lia.cache").
Please report.
|
|
|
|
|
|
|
|
A non-ASCII char is now converted to _UUxxxx_ with xxxx being its unicode index
in hexa. And any preexisting _UU substring in the ident is converted to _UUU.
The switch from __Uxxxx_ to _UUxxxx_ is cosmetic, it just helps the extraction
(less __ in names). But the other part of the patch (detection of preexisting
_UU substrings) is critical to make ascii_of_ident truly injective and avoid
the following kind of proof of False via native_compute :
Definition α := 1.
Definition __U03b1_ := 2.
Lemma oups : False.
Proof.
assert (α = __U03b1_). { native_compute. reflexivity. }
discriminate.
Qed.
Conflicts:
lib/unicode.mli
|
|
|
|
there is actually no change in default subst between 8.4 and 8.5.
|
|
|
|
Instead of rebuilding a whole set of evars just to make a typeclass filter,
we use the source evarmap.
|
|
|
|
obligations".
|
|
|
|
|
|
This patch also disables the -makecmd option and the corresponding test,
since the value is not stored for future use. This prevents gratuitously
failing to configure on FreeBSD.
|
|
A "sentence" includes all the blank lines and all the comments that
precede a command. So its starting location might be far from any error it
contains. This patch changes error reporting so that it relies on the
location of errors rather than the location of erroneous sentences.
|
|
|
|
|
|
|
|
|
|
into v8.5
|
|
|
|
The Haskell extraction code would allow line-wrapping of the Haskell
type definition, which would lead to unparseable Haskell code when the
linebreak occured just before the type name. In particular, with a term
name of 46 characters or more, the following Coq code:
Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt.
Extraction Language Haskell.
Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.
would produce:
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx ::
Unit
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx =
Tt
which failed to compile with GHC (according to Haskell's indentation
rules, the "Unit" line must be indented to be treated as a continuation
of the previous line).
This patch always forces the type onto a separate line, and ensures that
it is always indented by 2 spaces (just like the body of each definition).
|
|
Note that extracting terms containing primitive projections is still
utterly broken, so don't use them.
|
|
Patch by Matthieu, Enrico and myself.
|
|
A single terminal character can take up to 5 bytes, e.g. "''^A'".
|
|
preserved, which is a source of incompatibilities w.r.t. released 8.5
but which looks to me to be the only possible canonical behavior.
This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.
So, I consider this to be a fix to the "Regular Subst Tactic" mode.
Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
|
|
We only retype hypotheses and conclusion when they do depend on the cleared
identifier. This saves a lot of time.
|
|
rejected.
|
