| Age | Commit message (Collapse) | Author |
|---|
|
- 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11485 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11473 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(unrelated: a useless pattern variable becomes _ in Extract_env)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11458 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11456 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
-The use of Modops.type_of_mb seems to be sometimes an overkill :
it expands the situation where mb.mod_type=SEBident...
we use a simplier my_type_of_mb instead
-No more "truetype" boolean argument to this function. Normally,
the use of my_type_of_mb should ensure that all seb we inspect
are "true" module types, see the invariant written before this
function.
-Remove the use of replicate_msid: it was commented out since
a few months, no problem appeared, and anyway the handling of
"With ..." has completely changed since Elie's work.
-And by the way, cleanup of whitespaces at the end of lines...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11455 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11454 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
|
|
induction test-suite script.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11426 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
|
|
- Do not touch at the user equalities and so on by using a blocking
constant. This avoids the wild autoinjections and subst tactics that
were used before. Thanks to Brian Aydemir for an example were this hurt
a lot.
- Debug the tactic used to simplify induction hypotheses.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11415 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
cases where coercion could not occur as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11414 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by the automatically infered arguments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11407 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
normalization. Add test-suite file.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11406 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11405 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11403 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dance when defining a new program by default, which forces use of JMeq
but makes for much more robust tactics. Everything in success/Equations
works except for limitations due to JMeq or the guardness checker (one
example seems to actually diverge...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11402 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
|
|
recursive definitions and references to previous fields in record and
classes definitions. Fixes the corresponding typesetting issue in coqdoc
output.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11396 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11395 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11385 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
|
|
dependent [noConfusion] definitions in "A Few Constructions on
Constructors". Now the guardness check is blocking.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11374 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11356 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
|
|
support for "where" notation declarations as well. Better checking of
recursivity or not, after type-checking.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11354 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
definition is recursive or not based on occurence of a rec call in
the body. Examples updated, enjoy!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11353 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
|
|
- Fix an apparent bug in the printing of move, indeed by default
move is _not_ dependent when parsed (see parsing/g_tactic.ml4).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11351 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
backtracking on coercion classes when a coercion path fails).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11344 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Avoid using projections for singleton classes. Divides the size
of proofs by 2 and simplifies the typechecking as well.
- Switch to the new discrimination net implementation for classes,
with the current convention that all constants are unfoldable.
Users can add "Typeclasses Opaque" declarations make the dnet
discriminate more, otherwise it should be entirely
backward-compatible.
- Fix bug introduced in r11333 in "transitivity" tactic in presence
of coercions.
Up to 15% gains on setoid-intensive files like Ring_polynom and
Field_theory. More importantly, performance should not decrease
significantly by adding new Morphism/Setoid declarations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
obligation handler.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11335 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
syntax yet. Doesn't change the auto/eauto behavior either.
- Typeclass resolution now considers everything transparent by
default and does it consistently for "open" and closed terms.
- Correctly declare singleton classes definition as opaque for proof
search.
- Add a few initial declarations to make iff, id, compose... opaque
- Add definition of dependent signatures for dependent function types
and remove corresponding exception code in class_tactics. The
instance requires higher-order unification and is not really usable yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11333 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
inductive and Program defs. Fix eterm bug when generating obligations
and remove optimization of let-in removal which prevents factorization
of proofs/"asserts" in Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11330 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
csdpcert is not meant to be called directly by the user
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11327 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11318 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un
terme applicatif au moment de tester f u1 .. un = g v1 .. vn au
premier ordre : on revient sur l'algo tel qu'il était avant le
commit 11187.
- Bug #1887 (format récursif cassé à cause de la vérification des idents).
- Nouveau choix de formattage du message "Tactic Failure".
- Nettoyage vocabulaire "match context" -> "match goal" au passage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Correction divers messages d'erreur
- lorsque rien à réécrire dans une hyp,
- lorsqu'une variable ltac n'est pas liée,
- correction anomalie en présence de ?id dans le "as" de induction,
- correction mauvais env dans message d'erreur de unify_0.
- Diverses extensions et améliorations
- "specialize" :
- extension au cas (fun x1 ... xn => H u1 ... un),
- renommage au même endroit.
- "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
- "induction"
- intro des IH toujours au sommet même si induction sur var quantifiée,
- ajout d'un hack pour la reconnaissance de schémas inductifs comme
N_ind_double mais il reste du boulot pour reconnaître (et/ou
réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
dans l'ordre standard,
- vérification de longueur et éventuelle complétion des
intropatterns dans le cas de sous-patterns destructifs dans induction
(par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
le n dans le contexte),
- localisation des erreurs d'intropattern,
- ajout d'un pattern optionnel après "as" pour forcer une égalité et la
nommer (*).
- "apply" accepte plusieurs arguments séparés par des virgules (*).
- Plus de robustesse pour clear en présence d'evars.
- Amélioration affichage TacFun dans Print Ltac.
- Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
(incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
- Fusion VTactic/VFun dans l'espoir.
- Mise en place d'un système de trace de la pile des appels Ltac (tout en
préservant certains aspects de la récursivité terminale - cf bug #468).
- Tactiques primitives
- ajout de "move before" dans les tactiques primitives et ajout des
syntaxes move before et move dependent au niveau utilisateur (*),
- internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
- suppression de Intro_replacing et du code sous-traitant
- Nettoyage
- Suppression cible et fichiers minicoq non portés depuis longtemps.
(*) Extensions de syntaxe qu'il pourrait être opportun de discuter
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Also check mutuality of fixpoints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11257 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11252 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It breaks tauto as [?X _ _] matches much more terms. It is mostly fixed
by not destructing objects of record types. The new [intuition] was also
pulling an unneeded dependency in Field_theory which can be cleared
easily. Zis_gcd_bezout is also considered a conjunction now, which seems
correct(?).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11243 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
When doing monolithic extraction, the initial dependency graph
may turn to be too broad thanks to later optimisations. We now do
an extra dependency pass at the end, killing more useless code.
In addition, when doing an "Extract Constant t => ...", if t
isn't an axiom, we don't include the dependencies of the body of t.
This may break earlier extraction setups (with or without Extract
Constant), since they may take advantage of objects that were earlier
"wrongly" included in the extracted code. The fix is simple : just
add these missing objects to the extraction command-line.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11239 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de coqdoc (compatibilité)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
effacé dans un intro-pattern (suggéré par ssreflect).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11228 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11211 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In fact, Qge and Ggt disappear, and we only leave notations for > and >=
that map directly to Qlt and Qle.
We also adopt the same approach for BigN, BigZ, BigQ.
By the way, various clean-up concerning Zeq_bool, Zle_bool and similar
functions for Q.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11205 85f007b7-540e-0410-9357-904b9bb8a0f7
|
