aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.mli
Commit message (Expand)AuthorAge
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* 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
* Nouvelle en-têteGravatar herbelin2004-07-16
* more evar stuffGravatar corbinea2004-06-28
* effective evar refiningGravatar corbinea2004-06-26
* factorisation et generalisation des clausesGravatar barras2003-11-13
* petits changements de syntaxeGravatar barras2003-11-12
* Added Instantiate ... inGravatar corbinea2003-11-06
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-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
* reparation de make doc (ocamlweb & _)Gravatar letouzey2001-12-19
* 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
* Suppression du retypage dans w_DeclareGravatar herbelin2001-09-09
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* DocumentationGravatar herbelin2000-12-18
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - documentation repertoire proofs/Gravatar filliatr1999-10-20
* modules Evar_refiner et Typing_evGravatar filliatr1999-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 11:56:24 +0000