aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.ml
Commit message (Expand)AuthorAge
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et unifo...Gravatar notin2007-04-26
* Report de révision 9583 de la v8.1 dans le trunkGravatar notin2007-02-01
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* bypass w_Define when w_refine-ingGravatar corbinea2004-07-07
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* more evar stuffGravatar corbinea2004-06-28
* effective evar refiningGravatar corbinea2004-06-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 17:59:24 +0000