aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
Commit message (Expand)AuthorAge
* Mauvais environnement d'évaluation pour les globauxGravatar herbelin2003-01-22
* Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueurGravatar herbelin2003-01-21
* Mauvaise interprétatin de IdentArgTypeGravatar herbelin2003-01-20
* Protection contre les noms de tactiques inconnus; restriction exceptions ratt...Gravatar herbelin2003-01-20
* Petits bugsGravatar herbelin2003-01-20
* Utilisation d'une exception 'catchable'Gravatar herbelin2003-01-19
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
* Traitement spécial pour les types à l'internalisationGravatar herbelin2002-12-15
* Ajout du vernac Proof withGravatar gregoire2002-12-12
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* Re-ajout constrInGravatar herbelin2002-11-14
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesGravatar herbelin2002-10-21
* NewDestruct/NewInduction acceptent l'option "using"Gravatar herbelin2002-10-21
* L'application de ltac attend une référence; meilleure protection contreGravatar herbelin2002-10-14
* correction de bugs:Gravatar barras2002-08-16
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Bug dans la globalisation des arguments de tactiques primitivesGravatar herbelin2002-07-16
* Que la localisation des erreurs pour les tactiques atomiques marcheGravatar herbelin2002-07-11
* Hack pour autoriser les $n dans les Grammar tacticGravatar herbelin2002-07-03
* Réparation de l'interprétation des fermetures (sans casser Field!)Gravatar herbelin2002-06-13
* Ajout coercion constr vers hyp quantifiéeGravatar herbelin2002-06-06
* Les VContext ne sont plus des fermetures (temporaire)Gravatar delahaye2002-05-31
* Finalement un seul constr pour l'instant dans ExtraRedExprGravatar herbelin2002-05-30
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29