| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
binders.
- Change syntax of type class instances to better match the usual syntax of
lemmas/definitions with name first, then arguments ":" instance.
Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
Program.Utils, and subset_scope as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
lists of occurrences through tactics. Implement the "at" variants of
setoid_replace correspondingly.
Fix in class_tactics efor w_unify not checking types when unifying a
meta with anything (problematic at top-level only).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10820 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10496 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from
svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses
........
r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
Comment grammar error
........
r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
The initial Type Classes patch.
This patch introduces type classes and instance definitions a la Haskell.
Technically, it uses the implicit arguments mechanism which was extended a bit.
The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac).
........
r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
Fix interface
........
r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
Fix more xlate code
........
r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
Bug fixes in Instance decls.
........
r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
Streamline typeclass context implementation, prepare for class binders in proof statements.
........
r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
Stupid bug
........
r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
Other bugs related to naming in typeclasses fixed.
........
r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
Progress on setoids using type classes, recognize setoid equalities in hyps better.
Streamline implementation to return more information when resolving setoids (return the results setoid).
........
r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
Syntax change, more like Coq
........
r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
Work on type classes based rewrite tactic.
........
r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
Forgot to add a file
........
r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and
implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations.
Add useful tactics to Program.Subsets.
........
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
implicite du rapport de bug #468); utilisation pour cela d'un
mécanisme différent de localisation des échecs Ltac (mécanisme
probablement à affiner).
- Factorisation au passage des appels au débuggeur Ltac.
- Trivialités en passant dans clenv.ml.
- Tentative de documentation de l'infâme Reductionops.instance et essai
de déplacement plus amont du test "s = []".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10222 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
modification de interp_ltac_reference pour passer les ids utilisées
dans le contexte d'appel d'une tactique.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
de résoudre des buts comme celui-ci :
Record nat_retract : Type :=
{f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}.
Goal nat_retract.
exists (fun x => x) (fun x => x).
- Nouvelle tentative d'utilisation des types des metas/evars pour
inférer de nouvelles instances de metas/evars; permet par exemple
d'utiliser f_equal sans option with, mais aussi, avec la modif
précédente, de résoudre des buts tels que
Goal exists f:bool->Prop, f true = True.
exists (fun x => True).
[Les expériences passées avaient montré qu'en prenant en compte les
types dans l'unification, on peut unifier trop tôt une evars à une
mauvaise sorte; à défaut de mécanisme de prise en compte des problème
d'unification avec sous-typage, on s'est interdit ici d'unifier des
types qui sont des arités.]
- Tout les constr de tactic_expr deviennent des open_constr (même si seul
with_bindings les accepte au final... c'est pas l'idéal).
- Renommage env -> evd et templenv -> env dans clausenv.
- Renommage closed_generic_argument -> typed_generic_argument.
- Renommage closed_abstract_argument_type -> typed_abstract_argument_type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Tactic Notation acceptant des listes en entrée avec application à la
définition de revert dans Tactics.v.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
(provisoire ?) + export nouvelle macro pour maple.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8975 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8971 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7841 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
résolution des implicites restant après interprétation des termes dans les tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7363 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6680 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
dans redexpr.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
camlp4-generated code even if it is not found using grep)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6351 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6350 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
the new module kernel/mod_subst.ml.
MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now
possible to define substitutions that also delta-expand constants
(by associating the delta-expanded form to the constant name).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
des IntroPattern au parsing, à l'interprétation, à la traduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5134 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4678 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
compatibilité avec les foncteurs + réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de tactique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4112 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Utilisation d'ident plutôt que int pour PMeta/CPatVar
Ajout CEvar pour la saisie des Evar
Pas d'entrée utilisateur pour les Meta noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
pour compatibilité avec les modules.
Globalisation partielle des invocations de tactiques hors définitions
(partielle car noms des Intros/Assert/Inversion/... non connus).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3529 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3237 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
constrextern.ml est l'équivalent de termast.ml pour le nouveau
printer; topconstr.ml; contient la définition de "constr_expr";
modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
|
msozeau
herbelin
notin
barras
corbinea
sacerdot
gregoire