aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
Commit message (Expand)AuthorAge
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
* If a fixpoint is not written with an explicit { struct ... }, then Gravatar letouzey2007-07-07
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* Export de check_evars vers command.mlGravatar herbelin2006-09-01
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Subtac fixes, single fixpoint definitions are working again. Added a toggle o...Gravatar msozeau2006-03-22
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Léger nettoyage et uniformisation + généralisation du point d'entrée ltac...Gravatar herbelin2005-09-09
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* Nouvelle en-têteGravatar herbelin2004-07-16
* Amelioration message d'erreur pour ltacGravatar herbelin2003-11-04
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* - modifs de la condition de garde pour mieux tenir compte des raisonnementsGravatar barras2002-04-02
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* Ajout de dynamiques pour les quotations constr et tacticGravatar delahaye2001-10-02
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Nettoyage CoercionGravatar herbelin2000-10-19
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* portage RefineGravatar filliatr2000-07-20
* Séparation des contraintes de type et de valeur dans pretypingGravatar herbelin2000-06-29
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...Gravatar herbelin2000-03-28
* changement type add_anonymous_leafGravatar filliatr1999-12-05
* - global_reference traite des variablesGravatar filliatr1999-12-03
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* ocamlwebGravatar filliatr1999-11-30
* Modification pour faire compiler pretyping.ml qui maintenant compileGravatar herbelin1999-11-26
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
* organisation de trad (entre parsing/ et pretyping/)Gravatar filliatr1999-10-13