| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
processed in the larger context instead of the bodies.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11400 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
|
|
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
|
|
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
|
|
instance multiple times at each section closing (still a hack).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11338 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
|
|
11126 et qui faisait qu'on ne backtrackait en fait plus sur les
sous-termes d'un terme qui lui filtrait.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11304 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
canonique que si elle contribue vraiment à une équation canonique,
c'est-à-dire si son argument principal est une evar; sinon on
répercute le comportement historique qui est de préférer le dépliage
du côté droit d'une équation constante/constante.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11303 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
un nom importé) de la 8.2 vers le trunk.
--Cette ligne, et les suivantes ci-dessous, seront ignorées--
M pretyping/termops.ml
M toplevel/command.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11302 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
|
|
celui-là: si une structure canonique existe déjà avec une certaine
projection canonique donnée, on garde l'ancienne structure si jamais
une structure canonique plus récente arrive avec la même projection
canonique).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11298 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
class constraints of the form Π x1 ... xn, Class args.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11278 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Now there is a class "SetoidRelation" for registering relations that
should always be considered as setoids and never unfolded. Every "Add
Relation" command adds an instance and impl,iff are there by
default. Now the test is: if there is a SetoidRelation instance, use it
; otherwise, allow unfolding to find an eq or fallback on
setoid_rewrite. To avoid searching for SetoidRelation instances
repeateadly we check that it is really needed first by unfolding the
hyp. Only two scripts relied on the now-forbidden semantics of rewriting
by an @eq inside a setoid relation, in Numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11269 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
contraintes bornant par le haut le type de l'inductif (ce qui peut
arriver quand l'inductif est argument d'une constante) étaient
oubliées : on pouvait se retrouver avec des inductifs dont le type des
constructeurs, une fois instancié par des paramètres) n'était plus
typable (seul leur réduit, après expansion des constantes, était
typable). [kernel, test-suite]
+ Affichage des inductifs (via Print) en prenant la forme utilisateur des
constructeurs.
+ Correction warning dans compilation gallina.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11253 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
|
|
setting "Set Manual Implicit Arguments" for manual-only implicits.
Fix test-suite script. This removes the discharge_info argument of
"dynamic" object's rebuild function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11242 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
|
|
majuscule - si pas un ident ou un terme - et se terminent par un point).
Restent quelques utilisations de "error" qui sont liées à des usages internes,
ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas
où c'est le n-ième sous-termes qui finalement réussit (passage à une
complexité en n plutôt que n^2, via l'utilisation de continuations).
- Sémantique du filtrage: suppression dans sub_match de la recherche
dans le type des let (puisque ce n'est pas cencé être une
information utilisateur) mais rajout de la recherche dans le champ
cast qui lui est utilisateur.
- Nouvelle fonctionnalité: récupération des noms des variables liantes
filtrées (dans matches/sub_match) et utilisation de ces noms dans
ltac (utile pour récupérer x dans "exists x, P x");
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11226 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
classes, and simplify the implementation.
- Experimental syntax {{ cl : Class args }} and (( cl : Class args ))
which respectively make cl an implicit or explicit argument ({{ }} is
equivalent to [ ]). Could be extended to any type of binder, eg.
[Definition flip ((R : relation carrier)) : relation carrier := ...].
The idea behind double brackets is to distinguish macro-binders which
perform implicit generalization from regular binders. It could also save
[ ] for other uses.
- Fix bug #1901 about {} binders in records.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11210 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Now [ id : Class foo ] makes id an explicit argument,
and [ Class foo ] is equivalent to [ {someid} : Class foo ].
This makes declarations such as "Class Ord [ eq : Eq a ]" have
sensible implicit args.
- Better handling of {} in class and record declarations, refactorize
code for declaring structures and classes.
- Fix merging of implicit arguments information on section closing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11204 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Cases on multiple objects
- Avoid dangerous coercion with evars in subtac_coercion
- Resolve typeclasses method-by-method to get better error messages.
- Correct merging of instance databases (and add debug printer)
- Fix a script in NOrder where a setoid_replace was not working before.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11198 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(report de 11190 de v8.2 vers trunk). Le code fautif n'était en fait
plus utilisé car les contraintes de la forme ?n[..,x,..,x,..] := x que
ce code analysait sont finalement résolues par une heuristique de
consider_remaining_univ_constraints consistant à reproduire le
comportement de la 8.1.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11192 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
canoniques lors d'une unification constante/constante s'apprêtant à
déplier l'une des deux constantes (suggestion des utilisateurs de
structures canoniques), ceci afin de préserver des possibilités
ultérieures de résolution d'evars par équipement en structure
canonique.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11187 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Change from named_context to rel_context for class params and fields.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11163 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11160 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
discriminate/injection/simplify_eq acceptent maintenant un terme
comme argument. Les clauses "with" et les variantes "e" sont aussi
acceptées. Aussi, discriminate sans argument essaie maintenant
toutes les hyps quantifiées (au lieu de traiter seulement les buts
t1<>t2).
--This line, and those below, will be ignored--
M doc/refman/RefMan-tac.tex
M CHANGES
M pretyping/evd.ml
M pretyping/termops.ml
M pretyping/termops.mli
M pretyping/clenv.ml
M tactics/extratactics.ml4
M tactics/inv.ml
M tactics/equality.ml
M tactics/tactics.mli
M tactics/equality.mli
M tactics/tacticals.ml
M tactics/eqdecide.ml4
M tactics/tacinterp.ml
M tactics/tactics.ml
M tactics/extratactics.mli
M toplevel/auto_ind_decl.ml
M contrib/funind/invfun.ml
M test-suite/success/Discriminate.v
M test-suite/success/Injection.v
M proofs/clenvtac.mli
M proofs/clenvtac.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11158 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
constraints in Program:
- normalize types and defs of local fixpoints before checking the
guardness condition to avoid having to give type annotations, e.g:
<<
Definition fold (A B : Set) (f : B -> A -> B) : B -> tree A -> B :=
fix aux acc t :=
match t with
| Leaf x => f acc x
| Node l => fold_left aux l acc
end.
>>
- add new inh_coerce_to_prod to allow coercion of the typing constraint
to a product before trying to split it. It's a noop in standard mode,
and forgets subsets in Program. Allows to typecheck:
<< (λ x, x) : { f : nat -> nat | ... } >>.
- Better handling of the "abstract" typing constraints in Program.
- Correctly normalize w.r.t. evars. the tycon given by users in Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11156 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(résolution entre autres des bugs 1882, 1883, 1884).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
discharge time. Also fix bug when loading modules containing classes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11134 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unsatisfiable constraints.
Add a resolution call in tacinterp before trying the default tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
disambiguate syntax:
[ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x :
nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will
not parse.
Add applicative contexts in tactics match, to be able to match arbitrary partial
applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end
will bind C to [ ∙ 1 2 ] and x to 0.
Minor improvements in coqdoc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
restriction du contexte était attendue) + suppression warning +
amélioration affichage en cas de clause "at" incorrecte + report
commit 11121 (correction bug 1367) de la 8.2 vers le trunk.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11128 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
components and resolving them separately, reporting more precise failures.
Improve error messages.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11105 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Changement au passage de la convention "at -n1 ... -n2" en
"at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
pas mélanger des positifs et des négatifs.
- Au passage:
- simplification de gclause avec fusion de onconcl et concl_occs,
- généralisation de l'utilisation de la désignation des occurrences par la
négative aux cas de setoid_rewrite, clrewrite et rewrite at,
- correction d'un bug de "rewrite in at" qui utilisait le at de la
conclusion dans les hyps.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Correction wish 1866 (un "admit" plus fin dans sa généralisation des hyps)
- Bricoles dans cases.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
imbriqués) du bug 1834, mais le bug 1834 reste ouvert [cases.ml].
- Réactivation de l'interprétation des listes dans "generalize" cassée
depuis 11072) [tacinterp.ml].
- Bricoles et petit nettoyage en passant [cases.ml et g_vernac.ml4].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11083 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Relecture, mise à jour, correction d'erreurs et petite
réorganisation du chapitre sur les commandes vernaculaires.
- Correction bug #1865 (rafraichissement des univers algébriques).
- Suppression de la dépendance du initial.coq en les noms longs des fichiers
de façons à ce que les dépendances ne soient que purement logique.
- Encore un (petit) bug undo ide.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- MAJ CHANGES et COMPATIBILITY
- Réservation de || et && dans Notations.v
- code mort et MAJ suite commit 11072 (tactics.ml et changes.txt)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Ajout clause "in" à "remember" (et passage du code en ML).
- Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute
aussi une égalité pour se souvenir du terme sur lequel l'induction
ou l'analyse de cas s'applique.
- Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de
Programs qui avait la sémantique de "pose proof" tandis que le nouveau
a la même sémantique que "pose (id:=t)").
- Un peu de réorganisation, uniformisation de noms dans Arith, et
ajout EqNat dans Arith.
- Documentation tactiques et notations de tactiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11055 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
typeclass code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11047 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
files, about definitions and type of references.
- Add missing location information on fixpoints/cofixpoint in topconstr and
syntactic definitions in vernacentries for correct dumping.
- Dump definition information in vernacentries: defs, constructors,
projections etc...
- Modify coqdoc/index.mll to use this information instead of trying to
scan the file.
- Use the type information in latex output, update coqdoc.sty accordingly.
- Use the hyperref package to do crossrefs between definition and
references to coq objects in latex.
Next step is to test and debug it on bigger developments.
On the side:
- Fix Program Let which was adding a Global definition.
- Correct implicits for well-founded Program Fixpoints.
- Add new [Method] declaration kind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11017 85f007b7-540e-0410-9357-904b9bb8a0f7
|
