| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
| |
match_conjunction/match_disjunction/array_for_all_i
- Finally activate fine-tuned unfolding of iff in tauto: it breaks at
only one place in the user contribs (FSetAVL_dep.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11726 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Backtrack on precise unfolding of "iff" in "tauto": it has effects on
the naming of hypotheses (especially when doing "case H" with H of
type "{x|P<->Q}" since not unfolding will eventually introduce a name
"i" while unfolding will eventually introduce a name "a" (deep sigh).
- Miscellaneous (error when a plugin is missing, doc hnf, standardization
of names manipulating type constr_pattern, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
inductive types was not taken into account).
- Virtually extended tauto to
- support arbitrary-length disjunctions and conjunctions,
- support arbitrary complex forms of disjunctions and
conjunctions when in the contravariant of an implicative hypothesis,
- stick with the purely propositional fragment and not apply reflexivity.
This is virtual in the sense that it is not activated since it breaks
compatibility with the existing tauto.
- Modified the notion of conjunction and unit type used in hipattern in a
way that is closer to the intuitive meaning (forbid dependencies
between parameters in conjunction; forbid indices in unit types).
- Investigated how far "iff" could be turned into a direct inductive
definition; modified tauto.ml4 so that it works with the current and
the alternative definition.
- Fixed a bug in the error message from lookup_eliminator.
- Other minor changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
automation.
- Permitted to use evars in the intermediate steps of "apply in" (as expected
in the test file apply.v).
- Back on the systematic use of eq_rect (r11697) for implementing
rewriting (some proofs, especially lemma DistOoVv in
Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in
Sophia-Antipolis/Semantics/example2.v are explicitly refering
to the name of the lemmas used for rewriting).
- Fixed at the same time a bug in get_sort_of (predicativity of Set was not
taken into account).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
the number of conjunctions to split.
- A few cleaning and uniformisation in auto.ml.
- Removal of v62 hints already in core.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
effect, old cut_replacing was betaiota-normalizing, new
cut_replacing, from commit 11662, does not; turn
betaiota-normalisation into a purer and simpler whd_beta of the
abstracted rewriting predicate to the rewritten term).
- Made "induction in" more flexible when induction is on a goal variable
(accept occurrences -- even if theoretically unnecessary -- so as e.g.
not to expand occurrences that would otherwise trigger reductions -
see example in Peano.mult_succ_r).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11697 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
variant of the [unify] tactic that takes a hint db as argument and does
unification modulo its [transparent_state]. Add test-file for bug #1939
and another [AdvancedTypeClasses.v] that mimicks
[AdvancedCanonicalStructure.v].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11685 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
right unification flags for exact hints in eauto (may break a lot of
things by succeeding much more often).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11681 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
descend_conjunction)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11670 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Added "simple apply in" (cf wish 1917) + conversion and descent
under conjunction + contraction of useless beta-redex in "apply in"
+ support for open terms.
- Did not solve the "problem" that "apply in" generates a let-in which
is type-checked using a kernel conversion in the opposite side of what
the proof indicated (hence leading to a potential unexpected penalty
at Qed time).
- When applyng a sequence of lemmas, it would have been nice to allow
temporary evars as intermediate steps but this was too long to implement.
Smoother API in tactics.mli for assert_by/assert_as/pose_proof.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11662 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11658 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11632 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
(if ever necessary).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Improved warning when found several path to the same file in path
[mltop.ml4, system.ml]
- Add support for "rewrite" on specific equality to true (i.e. eq_true)
[Datatypes.v, tactics]
PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
reducing the type of the given lemma.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11571 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
declaration code to toplevel/record, including support for singleton
classes as definitions. Parsing code also factorized. Arnaud: one more
thing to think about when refactoring the definitions in vernacentries.
Add support for specifying what to do with anonymous variables in
contexts during internalisation (fixes bug #1982), current choice is to
generate a name for typeclass bindings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
Evarutil.check_and_clear_in_constr in V8.2 revision 11309 and trunk
revision 11300).
- Improved various error messages related to inversion, evars and case
analysis (including the removal of the obsolete dependent/non dependent
distinction).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11561 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Program. No syntax to do it yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11550 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
introduced by the lemma remain in the subgoals (i.e. it's really
[erewrite]).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11544 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Grant wish #1988 ("fun" forces reduction in "refine" if needed)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11536 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
une réduction a eu lieu (insertion d'un "change" pour que "apply"
n'échoue pas). À faire : nettoyer la construction par tactique de la
preuve de symétrie de a=b -> b=a (quand le lemme de symétrie n'existe
pas) pour quelle ne lance pas une conversion potentiellement longue
entre a et b (le cas est arrivé dans CatsInZFC/notation.v !) [HH + MS]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11521 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Fixed doc of assert as.
- Doc of apply in + update credits.
- Nettoyage partiel de Even.v en utilisant "Theorem with".
- Added check that name is not in use for "generalize as".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- make the modifiers "value of" and "type of" for "set" working (it was not!),
- clear unselected hypotheses in the "in" clause of "induction/destruct" when
the destructed term is a variable (experimental),
- support for generalization of hypotheses in the induction hypotheses using
the "in" clause of "induction" (e.g. "induction n in m, H" will
generalize over m -- would it be better to have an explicit
"over"/"generalizing" clause ?).
Added clause "as" to "apply in".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11509 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
s'est avéré ralentir la compilation des user-contribs au final, sans
compter aussi le bug 1980 apparemment introduit par ce commit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11505 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
avoid trying to resolve classes early in open constr arguments for Ltac,
the tactics themselves should do whatever's appropriate with the constraints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11503 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11498 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
instead of a completely resolved [constr] as input. The propagation of the
evars associated to the lemma is only allowed when the evar flag is on
(i.e. for [eapply]), otherwise they should be resolved by the end of the
application. Should be completely backwards compatible...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11497 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- New constr_expr construct [CGeneralization of loc * binding_kind *
abstraction_kind option * constr_expr] to generalize the free vars of
the [constr_expr], binding these using [binding_kind] and making
a lambda or a pi (or deciding from the scope) using [abstraction_kind
option] (abstraction_kind = AbsLambda | AbsPi)
- Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{
... }" for implicit bindings (both "..(" and "_(" seem much more
difficult to implement). Subject to discussion! A few examples added
in a test-suite file.
- Also add missing syntax for implicit/explicit combinations for
_binders_: "{( )}" means implicit for the generalized (outer) vars,
explicit for the (inner) variable itself. Subject to discussion as well :)
- Factor much typeclass instance declaration code. We now just have to
force generalization of the term after the : in instance declarations.
One more step to using Instance for records.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11495 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Prise en compte des notations applicatives
- Remplacement du codage des arguments liste des notations récursives
sous forme de terme par une représentation directe (permet notamment
de résoudre un problème de stack overflow de la fonction d'affichage)
+ Correction bug affichage Lemma dans ppvernac.ml
+ Divers util.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11489 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Extension du test de réversibilité acyclique des notations dures aux
notations de type abbréviation (du genre inhabited A := A).
- Ajout options Local/Global à Transparent/Opaque.
- Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé
dependent retiré).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11472 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11468 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
abusivement sur les clauses.
Nettoyage au passage de metamap qui était utilisé à la fois pour les
substitutions de meta et pour les contextes de typage de meta.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
SearchAbout + referring objects by their notation).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11446 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- A new [dependent pattern] tactic to do a pattern on an object in an
inductive family and generalize by both the indexes and the object
itself. Useful to prepare a goal for elimination with a dependent
principle.
- Better dependent elimination simplification tactic that doesn't
throw away non-dependent equalities if they can't be injected.
- Add [fold_sub] and [unfold_sub] tactics for folding/unfolding
well-founded definitions using measures built by Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11420 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
evars at the end of unification as later evars can refer to
previous ones. This removes the assumption that evars are already
ordered in eterm's code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11419 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
[discriminated]] with a switch for using the more experimantal dnet impl
for every hint. Also add [Hint Transparent/Opaque] which parameterize
the dnet and the unification flags used by auto/eauto with a particular
database. Document all this. Remove [Typeclasses unfold] directives that
are no longer needed (everything is unfoldable by default) and move to
[Typeclasses Transparent/Opaque] syntax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11409 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11405 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
eauto goals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11404 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11401 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
when one wants a particular type. Rewrite of the unification behind
[Equations], much more robust but still buggy w.r.t. inaccessible
patterns.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11399 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
simplifications (homogeneous equations first).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11398 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Go back to refine_hyp instead of specialize, because only the former
handles open terms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11391 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This permits to create a database [relations] in [RelationClasses] with
a single extern tactic in it that tries to apply [reflexivity] or
[symmetry]. This is then automatically used in [auto with *] and repair
backward compatibility. The previous commit broke some scripts which were
using [intuition] to do (setoid) [reflexivity] or [symmetry]: this
worked only by accident, because the hint database of typeclasses was
used. Overrall, this also allows to put a bunch of
always-applicable, related tactics in some database or to use
[Hint Extern] but match only on hypotheses.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
making the auto apply entry. Makes indexing better and avoid polution of
[auto with *] with many abstract lemmas comming from [typeclass_instances].
Quite a nice speedup again, even Field_theory has dropped to 58s from
70s.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11381 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
reification: putting variables in a varmap.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11376 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
overriding the default tactic when adding a definition.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11373 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
only relevant hypotheses in it, slightly cutting the search space.
Makes setoid_rewrite less sensitive to the number of hypothesis (~ 5%
time improvment on the stdlib). This currently prevents resolution with
constants which reduce to classes, hence the modifications in Setoids.Setoid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11360 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
evar, do unification between the evar type and the type of the instance
to properly propagate information.
Typical example: in context ?A : Type, ?R : relation ?A. When we instantiate ?R
using a goal like x = y by @eq t, we need to instantiate A to t as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11357 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
the same typeclass method application tactic that's available to users.
Modify a bit the _red tactics to accomodate the new setup and comment
some dead code in setoid_replace. Next step is removing it completely.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11355 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
equations.
It is essentially an implementation of the "Eliminating Dependent
Pattern-Matching" paper by Goguen, McBride and McKinna, relying on the
new dependent eliminations tactics. The bulk is in
contrib/subtac/equations.ml4. It implements a tree splitting on a set of
clauses and the generation of a corresponding proof term along with some
obligations at each splitting node. The obligations are solved by
driving the dependent elimination tactic and you get a complete proof
term at the end with the code given by the equations at the right spots,
the rest of the cases being pruned automatically.
Does not support recursion yet, a file with examples is in the
test-suite. With recursion, it would be similar to Agda 2's pattern
matching, except it won't reduce in Coq due to JMeq's/K.
Incidentally, the simplification tactics after dependent elimination
have been improved, resulting in a clearer and more space efficient
implementation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11352 85f007b7-540e-0410-9357-904b9bb8a0f7
|