| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Commit dc438047 was a bit overlooked as it introduced a wrong comparison function
on term patterns in dnets. Strangely enough, it seems not to have wreaked havoc
that much compared to the severity of the error.
|
|
File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.
There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
|
|
|
|
|
|
When set, search results only display symbol names, instead of
displaying full terms with types. This is useful when the list of
symbols is needed by an external program, in particular for doing
completion in IDEs.
|
|
abbreviation not bound to an applied constructor as itself but rather
as a binding variable as it was the case for non-applied
constructor). This was broken by e5c02503 while fixed #3483 (Not_found
uncaught with a notation to a non-constructor).
|
|
|
|
This should actually probably be an anomaly, but I'm unsure the code
for decidability schemes is robust enough to dare it.
|
|
decidability scheme).
Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:
Set Decidable Equality Schemes.
Inductive a := A with b := B.
which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
|
|
|
|
|
|
|
|
"Print Module command shows module type expression incorrectly".
|
|
This patch implements the traversal of inductive definitions in the
traverse function of toplevel/assumptions.ml which recursively
collects references in terms. In my opinion, this fixes a bug (but it
could be argued that inductive definitions were not traversed on
purpose). I think that is not possible to use this bug to hide a
meaningful use of an axiom.
You can try the patch with the following coq script:
Axiom n1 : nat.
Axiom n2 : nat.
Axiom n3 : nat.
Inductive I1 (p := n1) : Type := c1.
Inductive I2 : let p := n2 in Type := c2.
Inductive I3 : Type := c3 : let p := n3 in I3.
Inductive J : I1 -> I2 -> I3 -> Type :=
| cj : J c1 c2 c3.
Inductive K : I1 -> I2 -> I3 -> Type := .
Definition T := I1 -> I2 -> I3.
Definition C := c1.
Print Assumptions I1.
Print Assumptions I2.
Print Assumptions I3.
Print Assumptions J.
Print Assumptions K.
Print Assumptions T.
Print Assumptions C.
Print Assumptions c1.
Print Assumptions c2.
Print Assumptions c3.
Print Assumptions cj.
The patch is a bit more complicated that I would have liked due to
the feature introduced in commit 2defd4c. Since this commit,
Print Assumptions also displays the type proved when one destruct
an axiom inhabiting an empty type. This provides more information
about where the old implementation of the admit tactic is used.
I am not a big fan of this feature, especially since the change in
the admit tactic.
PS: In order to write some tests, I had to change the criteria for
picking which axiom destruction are printed. The original
criteria was :
| Case (_,oty,c,[||]) ->
(* non dependent match on an inductive with no constructor *)
begin match Constr.(kind oty, kind c) with
| Lambda(Anonymous,_,oty), Const (kn, _)
when Vars.noccurn 1 oty &&
not (Declareops.constant_has_body (lookup_constant kn)) ->
and I replaced Anonymous by _. Indeed, an Anonymous name here could
only be built using the "case" tactic and the pretyper seems to always
provide a name when compiling "match axiom as _ with end". And I
wanted to test what happened when this destruction occurs in
inductive definitions (which is of course weird in practice), for
instance:
Inductive I4 (X : Type) (p := match absurd return X with end)
: Type -> Type :=
c4 : forall (q := match absurd return X with end)
(Y : Type) (r := match absurd return Y with end), I4 X Y.
The ability of "triggering" the display of this information only when
using the "case" tactic (and not destruct or pattern matching written
by hand) could have been a feature. If so, please feel free to
change back the criteria to "Anonymous".
|
|
The .png was ugly (less than 400px wide) and did not match the content of
the .fig file (e.g. presence of '$'). To improve things a bit, text is now
rendered by latex.
|
|
|
|
The quadratic behaviour of list searching probably appears with small
enough samples. With the advent of usable libraries in Coq, and thus many
possible dependencies, better be safe than sorry.
|
|
|
|
On Fedora, `which 2>&1 >/dev/null` doesn't silence stderr, while `which >/dev/null 2>&1` does.
|
|
|
|
|
|
The file seems to have been reintroduced by error by commit 012fe1a96, but
it was not compiled anyway.
|
|
|
|
|
|
Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
|
|
I was not seeing the warning due to the 10 deprecation warnings before
it...
|
|
|
|
|
|
|
|
unification in tactics.
The relaxing of occur-check was ok but was leading trivial problems of
the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into
?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems
was not any more able to deal with.
Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way,
so that it behaves as if the occur-check had not been restricted.
|
|
using closer naming strategies for naming variables in make_all_name_different
and when contracting trivial letins.
Not sure what the best policy is. Maybe the contraction process should
not invent names at al and let make_all_name_different do the job.
Maybe pretyping should name all rels which it pushes to environment
(with cases.ml paying attention to avoid clash).
The problem shows for instance with a PretypeError (... env, ... ,
ActualTypeNotCoercible (NotClean (... env ...)) message with two
copies of env which we don't if they are the same but which have to
share same names for similar rendering of the rels!
This was revealed e.g. by the error message of #4177.
|
|
This is a bug in a pretty old code, showing also in 8.3 and 8.4.
|
|
|
|
former filter after 48509b61 and 3cd718c, because filtered let-ins
were not any longer preserved).
|
|
|
|
Patch by Matthieu Sozeau.
Fixes #3819: "Error: Unsatisfied constraints" due to canonical
structure inference
|
|
We were throwing away constraints from 'with Definition' in module
type ascriptions.
|
|
because of the name of a bound variable lost when unifying under a
binder in evarconv.
|
|
Indeed, the name of a bound variable was lost when unifying under a Prod in
evarconv.
The error message for "Unable to satisfy the following constraints" is
still to be improved though.
|
|
I was trying to be a bit too clever with not substituting the universe
instance everywhere: the constructor type/inductive arity has to be
instantiated before instantiate_params runs, which became true only
for constructor types since my last commit.
|
|
It showed up at the CoqCS.
|
|
Calling md5sum test earlier, at the time coqchk is built, rather than
at testing time, hopefully moving it closer to what it is supposed to
occur.
|
|
|
|
|
|
|
|
Commit df6e64fd28 let apply_coercion raise NoCoercion untrapped by inh_app_fun.
Commit 4944b5e72 caught NoCoercion but missed re-attempting inserting a
coercion after resolving instances of type classes.
This fixes MathClasses (while preserving fix of part of from 4944b5e72
and fixes of HoTT_coq_014.v from df6e64fd28).
|
|
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
|
|
|
|
|
