| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The evar counter has been moved from Evarutil to Evd, and all functions in
Evarutil now go through a dedicated primitive to create a fresh evar from
an evarmap.
|
|
A term was reduced in an improper environment.
|
|
|
|
The `search_guard` function is called to infer the recursive argument of fixpoints. For each potential argument, it tests whether it is called structurally, calling the kernel test. When a single argument is available either because `{struct x}` was specified, or because there is a single inductive argument, the kernel test is performed, despite the fact that the kernel will do it later, and the kernel error reraised. It is unnecessary.
|
|
(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.
|
|
This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)). It is
useful to have function_scope for, e.g., function composition. This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.
Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax. (The scope type_scope
should not be special-cased; this change is coming up next.)
Also explicitly define [function_scope] in theories/Init/Notations.v.
This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]
We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.
|
|
|
|
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.
|
|
|
|
|
|
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
|
Evars already had their own extensible state, but adding it globally allows
to write out extensible state-passing code in e.g. plugins. The additional
data is hopefully transparently preserved by the code out there. Trespassers
ought to be prosecuted.
|
|
It enhances bug #3527, as instead of raising an anomaly "Uncaught
exception Coercion.NoCoercion(_)", it now fails with a typing error.
|
|
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
