aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.ml
Commit message (Expand)AuthorAge
* Amélioration du message d'erreur "w_unify"Gravatar clrenard2003-12-01
* Amelioration du message d'erreur en cas de tentative d'instanciationGravatar clrenard2003-11-15
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Added Instantiate ... inGravatar corbinea2003-11-06
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* backtrack dans l'algo d'unificationGravatar barras2002-04-10
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Suppression du retypage dans w_DeclareGravatar herbelin2001-09-09
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Bug dans l'utilisation de l'option debugGravatar herbelin2000-12-20
* Code mortGravatar herbelin2000-12-18
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Nettoyage de GenericGravatar herbelin2000-05-31
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* modules Evar_refiner et Typing_evGravatar filliatr1999-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 15:24:28 +0000