| Age | Commit message (Collapse) | Author |
|---|
|
declaring additional conversion problems when unifying the type of an
evar instance and the evar's declared type. Fix the corresponding
conversion heuristic which failed due to (misplaced?) assertions when
faced with general conversion problems.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11549 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
instances and the corresponding evar's type if it contains existentials
to avoid dangling evars. No noticeable performance impact (at least on the
stdlib). Subsumes (and fixes) the (broken) fix in unification.ml that was
previously patched by M. Puech.
Improve error messages related to existential variables and type
classes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11543 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for record fields (using "someproj : sometype where not := constr" syntax). Only one
notation allowed currently and no redeclaration after the record
declaration either (will be done for typeclasses).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 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
|
|
It solves feature request 1852, makes me and Arnaud happy and
will permit to factor some more code in typeclasses.
- Records are introduced using the syntax "{| x := t; y := foo |}" and
"with" clauses are currently parsed but not yet supported in the
elaboration. You are invited to suggest other syntaxes :)
- Missing fields are turned into holes, extra fields cause an error
message. The current implementation finds the type of the record
at pretyping time, from the typing constraint alone (and just expects
an inductive with one constructor). It is then impossible to use
scope information to parse the bodies: that may be wrong. The other
solution I see is using the fields to detect the type earlier, before
internalisation of the bodies, but then we get in name clash hell.
- In funind/contrib/interface I mostly put [assert false] everywhere to
avoid warnings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dans clos_norm_flags (cf échec dans CoRN.Transc.InvTrigonom.Tan_ilim). Ceci
dit :
- cela ne me parait pas moral que clos_norm_flags s'occupe de
normaliser les evars,
- mais comme "evar" n'est pas un flag supporté par closure.ml, on ne
peut pas le donner à la demande comme argument de clos_norm_flags
(question: pourrait-on faire supporter la réduction Evar par closure.ml ??).
Plus généralement, il y a un problème avec la propagation des
instantiations des evars à travers les buts (cf lemme eapply_evar dans
test-suite/success/apply.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11470 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
|
|
* Fixed typo in unify_0 regarding conv_pb
* First attempt to fix a problem related to rels in w_merge. Seems to
be unsuccessful at this point
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- backtrack on kernel modifications: the monomorphic instance of an inductive
type is constrained to live in an universe higher (or equal) than all the
instances
- improved support for polymorphic inductive types at the refiner level:
introduced type_of_inductive_knowing_conclusion that computes the
instance to match the current conclusion universe.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11435 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unfold first. The patch changes the usual order of unifications so some
may differ (only one example in the stdlib breaks because of more
unification happening).
Actually this change was trigerred because of an incompleteness which is
not resolved here. At least this way unfolding is consistent between
w_unify and the kernel.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11427 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11425 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11423 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
|
|
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
|
|
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
|
