| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
| |
agreement with wish #2117 (pattern unification of evars remained
deactivated for 3 years because of incompatibilities with eauto [see
commit 9234]; thanks to unification flags, it can be activated for
apply w/o changing eauto).
Also add test for bug #2123 (see commit 12228).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
evar is dependent or not (solve bug #2123).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12228 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12227 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
had wrong type). At least two problems remain:
- projection involving evar should check the type are compatible,
- instances of filtered evars should not be shrinked as all values are
needed to ensure the well-typedness of the instanciated restricted evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12226 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
command list
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12225 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
traînaient un peu partout dans le code depuis la fusion d'evar_map et
evar_defs. Début du travail d'uniformisation des noms donnés aux
evar_defs à travers le code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
structures)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12223 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12222 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12220 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
selection of occurrences.
We use a new function [unify_to_subterm_all] to return all occurrences
of a lemma and produce the rewrite depending on a new [conditions] option
that controls if we must rewrite one or all occurrences and if the side
conditions should be solved or not for a single rewrite to be successful.
[rewrite*] will rewrite the first occurrence whose side-conditions are
solved while [autorewrite*] will rewrite all occurrences whose
side-conditions are solved.
Not supported by [setoid_rewrite] yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12218 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- theories: made a hint database with the constructor of eq_true
- coqide: binding F5 to About dans coqide + made coqide aware of
string interpretation inside comments
- lexer: added warning when ending comments inside a strings itself in a comment
- xlate: completed patten-matching on IntroForthComing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12217 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
wrong tycon.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12216 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
dependent argument.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12215 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
in Program's pattern-matching compilation (fixes bug #2131).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12214 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
on a matched variable when it is of dependent type, when its type allows
it (no constructor in the real arguments).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12213 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12212 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
flags of manual implicit arguments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12211 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
in the right environment and substitute the actual argument in the
remaining signature. It works as long as we do no try to rewrite
a dependent argument itself.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12207 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
was true.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12206 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12203 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
pattern unification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12202 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12201 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
framework anyway)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12199 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12198 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
and add an optional fail_evar flag to control resolution better in
interpretation functions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12197 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
necessary information. Fix implementation of [split_evars] and
use splitting more wisely as it has a big performance impact.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12196 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
conversion problem. TODO: The right fix is to use constraints and
backtracking search when solving them.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12195 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
tactics that use it won't be in scope either.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12193 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
rewriting lemma more precisely. This should make rewrite properly fail
when existentials are around instead of giving an identical goal up to
new evars. Also a first step towards adding occurences to the leibniz
rewrite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12192 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
may be a product.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12188 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12186 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
unnecessarily computed when the user won't see it (avoids the costly
nf_evar_defs in typeclass errors).
Add hook support for mutual definitions in Program.
Try to solve only the argument typeclasses when calling [refine].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12185 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
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
|