| 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.
|
|
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
|
|
|
|
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.
|
|
|
|
|
|
|
|
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.
|
