| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
is ongoing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12184 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
in the context to avoid it being abstracted over in potential evars
occuring in the codomain, which can prevent unifications.
Add [intro] to the typeclasses eauto and fix [make_resolve_hyp] to
properly normalize types w.r.t. evars before searching for a class in an
hypothesis.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12182 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
The comment just below makes me think this is just a typo...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
ensure the type and relation used in the subgoals stay syntactically the
same, for compatibility with [ring] which does not use conversion
to find the ring on a relation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
coming from the lemma in setoid_rewrite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12178 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
resolution of generated evars, not doing any backtracking yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12175 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
configurable through preferences.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12174 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12173 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
marks and no longer on old-fashioned reset to id.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12172 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- "*" implements Arthur Charguéraud's "introv"
- "**" works as "; intros" (see also "*" in ssreflect).
- Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui.
- Shy attempt to seize the opportunity to clean Zarith_dec but Coq's
library is really going anarchically (see a summary of the various
formulations of total order, dichotomy of order and decidability of
equality and in stdlib-project.tex in branch V8revised-theories).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
revisions 12063 and 12065).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12169 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
instead of the index required by the user; extended FixRule and
Cofix accordingly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12168 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12167 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12166 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
[copy of revision 12164 from branch v8.2]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12165 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
before calling it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12162 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
rewriting using eta.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12161 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12160 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
major changes in [w_unify] and the conversion functions used by it to
handle the sort constraints correctly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12158 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
## File(s) to commit:
## tactics/refine.ml
Try solving typeclasses before refining in Refine.refine (suggested by
S. Lescuyer).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12157 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
conversion when sort variables are involved and always call it
with an empty sort constraint set to avoid [whd_sort_variable] reducing
a universe variable to an algebraic universe.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12156 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
not set.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12155 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
lists.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12154 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
[base_sort_conv] and revert change in [unify_type].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12153 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12152 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
qui permet de changer la façon dont on imprime certains sous-termes sans
avoir à réécrire entièrement un printer de constr.
Dans le même esprit que les commits sur le parser et le lexer, je
cherche à donner une flexibilité aux plugins pour changer l'aspect de
Coq pour le plier à d'autres conventions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12151 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
definitions and variables (may increase the vo's size a bit), which in
turn fixes discharging with manual implicit args only.
Fix Context to correctly handle "kept" assumptions for typeclasses,
discharging a class variable when any variable bound in it is used.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12150 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
[set_eq_sort_variable] for cases where two universes should be equal,
fix [evars_reset_evd] to keep sort constraints and use [whd_sort_var]
directly in [whd_evar].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12149 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
as they are used.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12148 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
un plugin.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12147 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lheureusement,=20je=20ne
=20sais=20pas=20permettre=20que=20GDELETE=5FRULE=20soit=20appelable=20pendant=20une=20section
=20sans=20causer=20de=20potentiels=20soucis=20(bien=20que=20je=20trouve=20qu'il=20faille=20un
=20esprit=20sacr=C3=A9ment=20pervers=20pour=20faire=20Declare=20ML=20Module=20dans=20une=20section).?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Je suppose qu'on est dans le même esprit d'information trop partielle
que pour les notations aux niveaux 8, 99 et 200.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12146 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12145 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12144 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12143 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
de Bruijn-bound parameters (reported by W. Swierstra).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12142 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12141 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Solve meta type equations in the order they appeared during
unification: it's sensible because we do an [hnf_constr] on these
types, introducing a bit of delta even when it's not allowed by the
flags, and some code relies on it. A definite solution would involve an
nf variant of hnf_constr or allowing delta-reduction of closed terms
when unifying types.
- Do a bit of betaiota reduction on types in [check_types] while we
haven't got a sort-variable aware [is_trans_fconv] test.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12140 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
revised-theories branch. The V5.10 period at Lyon is still unclear.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12138 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
universes as usual, we add the new universes to the sort constraints and
do unification modulo those ([constr_unify_with_sorts]): this allows to
instanciate Type i with Prop for example and keep track of it. The sort
constraints are thrown away at the end of unification for the moment,
but we can detect inconsistencies during unification.
Make unification more symmetric as well w.r.t. substitution of defined
metas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12137 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Restore failure when types don't unify in [unify_types] (undoing
r12075) but try to be more clever about cumulativity using the meta's
[instance_status] information.
- Fix second-order abstraction when K is not allowed to ensure that
we don't unify twice with the same subterm in
[w_unify_to_subterm_list]. A more elaborate solution would be give the
list to [w_unify_to_subterm] so that it keeps going when it finds an
already-found instantiation.
- Two "obvious" errors fixed: taking the wrong instance status when
unifying with a meta on the right and forgoting type equations in
[w_merge].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12136 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(bug 2092 and decl_mode.v in test suite).
- Added a debugging printer for pftreestate.
- Fixing American spelling in RefMan-decl.tex.
- Optimizing application of tactic validation by removing consistency
test in descend.
- Fixing printing ambiguity for Hint Rewrite ->/<- in extratactics.ml4.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12134 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
non-matching lists.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12133 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12132 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Primitive setup for firing typeclass resolution on-demand: add a flag to
control resolution of remaining evars (e.g. typeclasses) during
unification.
- Prevent canonical projection resolution when no delta is allowed
during unification (fixes incompatibility found in ssreflect).
- Correctly check types when the head is an evar _or_ a meta in w_unify.
Move [isEvar_or_Meta] to kernel/term.ml, it's used in two places now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
function name (instead of failure).
- Making descent through conjunctions in apply work on recursive
tuples such as Acc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12129 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
unification algorithm. Uses the same code to recognize projections
(check_conv_record) and the same unification steps on the solution as
evar_conv. This required to fold the sigma through unify_* along with
the meta and evar substitutions as this can grow during unification.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12128 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- Set implicit args on for Context decls
- Move class_apply tactic to Init
- Normalize evars before raising an error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12127 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12126 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
when it comes to notation declared in scope
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12125 85f007b7-540e-0410-9357-904b9bb8a0f7
|