| Age | Commit message (Collapse) | Author |
|---|
|
|
|
- Implicit arguments in the return clause and in the branches
of a match were not checked.
- Implicit arguments in each declaration of intern_context were not
restarted.
- Additionally, in intern_context, we take into account ids from the
env on top of which intern_context is called.
- A better approximation of the check for manual implicit in notations
improved (though not fully correct because the exact context of
interpretation of a binder in a notation with recursive binders is
not known).
We also rename impl_binder_index into binder_block_names in anticipation of
checking redundancies also for non-implicit arguments.
|
|
|
|
in goal context.
Note: printing of a declaration was previously done in the context
made of the preceding segment of hypotheses, while now it is made in
the full context of all hyps (those coming before and after the hyp
being printed). As a consequence, constants which could be confused
with a variable in the context are now always qualified even if the
conflicting variable name is coming later. But why not, that looks
somehow more uniform like this.
|
|
This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf.
Going back to the convention of naming bound variables in hypotheses
of the goal as in 8.4.
My arguments for the revert are:
- apply ... with (id:=...) would have to be changed too, then possibly
breaking the compatibility
- the naming became dependent of the order of variables as in
x:nat
H:forall x0, x0=0
=====
goal
but
H:forall x, x=0
x:nat
=====
goal
Accordingly, this is all a matter of convention, since the meaning of
bindings is anyway the same in both cases.
|
|
|
|
Removed one more bug in simplification of visibly_occur_id in r12549
+ improved CHANGES message
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12561 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- fixed misunderstanding of the role of nenv while simplifying code of
occur_id in namegen.ml,
- documented the possible incompatibilites in CHANGES
- fixed output/Naming.v test, and fixed the count of misc. tests in
test-suite/check.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12556 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- backtrack on incompatibility introduced in intro while trying to
simplify the condition about when to restart the subscript of a name
(the legacy says: find a new name from x0 if the name xN exists in
the context but find a new name from xN+1 if the name xN does not
exists in the context but is a global to avoid).
- made the names chosen by "intro" compliant with the ones printed in
the goal and used for "intros until" (possible source of rare
incompatibilities) [replaced the use of visibly_occur_id for
printing the goal into a call to next_name_away_in_goal]
- also made the names internal to T in "T -> U" printed the same in
the goal as they are while printing T after it is introducted in the
hypotheses [non contravariant propagation of boolean isgoal in
detype_binder]
- simplified a bit visibly_occur_id (the Rel and Var cases were useless as
soon as the avoid list contained the current env); still this function is
costly with polynomial time in the depth of binders
- see file output/Naming.v for examples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7
|
