| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
compare bodies
of convertible types! Bug found by B. Ziliani.
|
| |
|
|
|
| |
This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses
don't respect Barendregt convention".
|
| | |
|
| |
|
|
|
|
| |
ML tactics that may be used as simple identifiers are now declared as
a true Ltac entry pertaining to the module that contains the Declare ML
Module statement.
|
| |
|
|
|
| |
This allows to directly register globtactics in the Tacenv API, without
having to resort to any internalization function.
|
| |
|
|
|
|
|
|
|
|
|
| |
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
|
| | |
|
| |
|
|
|
| |
Instead of having a version of unpackers for each level, we use a dummy argument
to force unification of types.
|
| |
|
|
|
|
| |
at least remove the successes obtained by trivial unification of a
meta with the goal, so as to avoid surprising results. We generalize
this to variables which will only eventually be replaced by metas.
|
| |
|
|
|
| |
Indeed, generalized binders are unnamed, because their name is generated on the
fly.
|
| |
|
|
| |
eta-expanded version of a projection as before.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
|
| |
|
|
|
|
|
| |
The unification oracle now prefers unfolding the eta-expanded form of a
projection over the primitive projection, and allows first-order
unification on applications of constructors of primitive records,
in case eta-conversion fails (disabled by previous patch on eta).
|
| |
|
|
|
|
|
| |
pruning),
hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but
backtrack to eqappr on OccurCheck failures (problem found in Ssreflect).
|
| |
|
|
| |
presence of let-ins.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
All superscript numbers are now symbols instead of parts of identifiers.
This disallows some identifiers, but hopefully not a lot of people were
using superscripts as part of identifiers, weren't they?
|
| |
|
|
|
|
|
|
| |
behavior of evar_conv_x,
getting more common after patch on evars and eta. The main problem is that ?X = C[?X] problems get
postponed now, when they failed earlier before (rendering the algorithm incomplete, e.g. on ?X = \y. ?X y).
A notion of "rigid/strongly rigid" occurrences would give a better fix.
|
| |
|
|
|
|
| |
Indeed [tclWITHHOLES false tac sigma x] is equivalent to [tclEVARS sigma <*> tac x]
and we should try to reduce the use of this tactical, because it is mostly
a legacy tactic.
|
| |
|
|
| |
Coq now accepts the [Universes u1 ... un] syntax.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
For consistency with ChoiceFacts
|
| |
|
|
|
|
|
|
| |
The generalized versions are names *_one_var. We preserve backwards
compatibility by defining the old versions in terms of the generalized
ones.
This closes the rest of Bug 3019, and closes pull request #6.
|
| |
|
|
| |
stm test-suite files.
|
| |
|
|
| |
of metas/evars
|
| | |
|
| |
|
|
|
| |
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
cases pattern variables than for naming forall/fun binders (but still
avoiding constructor names).
Note in passing: such as it is implemented, the general strategy is in
O(n²) in the number of nested binders, because, when computing the
name for each 'fun x => c" (or forall, or a pattern name), the names
from the outside c and visibly occurring in c are computed.
|
| |
|
|
|
|
| |
Should we also add is_* tactics for other things? is_rel, is_meta,
is_sort, is_cast, is_prod, is_lambda, is_letin, is_app, is_const,
is_ind, is_constructor, is_case, is_proj?
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
| | |
|
| |
|
|
| |
Based on suggestion by @gasche.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
I'm not quite sure why, but I'm pretty sure it's not. Rather, in
"allowing for foo" and "allowing to foo", "foo" modifies the sense in
which someting is allowed, rather than it being "foo" that's allowed.
"Allowing fooing" generally works, though it can sound a bit awkward.
"Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always
acceptable, in-as-much as it's ok to use "one".
I haven't touched the older instances of it in the CHANGES file.
|
| | |
|
| |
|
|
|
| |
Conflicts:
tools/coqdep_lexer.mll
|
| | |
|
| | |
|
| |
|
|
|
| |
- The state machine gets kind of complex
maybe it should become a parser at some point?
|
Matthieu Sozeau
Pierre Boutillier
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Jason Gross
Pierre Boutillier
Jason Gross
Gregory Malecha