| Age | Commit message (Collapse) | Author |
|---|
|
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
|
|
|
|
Add a flag to disallow minimization to set
|
|
Retypecheck abstracted infered predicate to register the right
universe constraints.
|
|
Let merge_context_set be lenient when merging the context of side
effects of an entry from solve_by_tac.
|
|
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
|
universe graph
|
|
|
|
|
|
|
|
|
|
This allows pretyping and detyping to be inverses regarding universes,
and makes Function's detyping/pretyping manipulations bearable in
presence of global universes that must be declared (otherwise an evd
would need to be threaded there in many places as well).
|
|
- Fix union of universe contexts to keep declarations
- Fix side-effect handling to register new global universes
in the graph.
|
|
|
|
|
|
Rechecking applications built by evarconv's imitation.
|
|
|
|
|
|
A term was reduced in an improper environment.
|
|
(Fix bug #4348)
|
|
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
|
clause in pattern-matching or not.
|
|
of syntax in test file ltac.v.
|
|
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
|
|
|
|
|
of arguments of eta_constructor.
|
|
naming of arguments of eta.
|
|
|
|
|
|
|
|
capturing bound names unexpectingly).
We moved renaming to after finding bindings, i.e. in pretyping
"fun x y => x + y" in an ltac environment where y is ltac-bound to x,
we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1"
(which later on is displayed into "fun y y0 => y + y0").
We renounced to renaming in "match" patterns, which was anyway not
working well, as e.g. in
let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0).
which was producing
forall z : nat, match z with 0 => z | S y => y end = 0
because the names in default branches are treated specifically.
It would be easy to support renaming in match again, by putting the
ltac env in the Cases.pattern_matching_problem state and to rename the
names in "typs" (from build_branch), just before returning them at the
end of the function (and similarly in abstract_predicate for the names
occurring in the return predicate).
However, we rename binders in fix which were not interpreted.
There are some difficulties with evar because we want them defined in
the interpreted env (see comment to ltac_interp_name_env).
fix ltac name
|
|
|
|
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
|
|
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.
|
|
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?
|
|
Unfortunately, it seems that retyping can be called in ill-typed terms and/or in
the wrong environment. This was broken for projections by my commit
a51cce369b9c634a93120092d4c7685a242d55b1
|
|
Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
|
|
I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
|
|
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
|
In case we need to backtrack on universe inconsistencies when converting
two (incompatible) instances of the same constant and unfold them.
Bug reported by Amin Timany.
|
|
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
|
|
with other reduction machines.
|
|
|
