aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.mli
Commit message (Expand)AuthorAge
* Correction d'un bug de l'unification pattern qui oubliait d'expanserGravatar herbelin2008-05-20
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* Move generally useful definition of nf_evar on contexts to evarutil.Gravatar msozeau2008-02-08
* Complément aux commits 10124 et 10125 sur l'inférence de type (correction Gravatar herbelin2007-09-26
* Raffinement de l'algorithme d'inférence de typeGravatar herbelin2007-09-17
* Correction d'un bug dans check_and_clear_in_constr + simplification deGravatar notin2007-01-31
* Nouvelle implantation de clear_hypsGravatar notin2007-01-30
* Correction du bug #1315:Gravatar notin2007-01-22
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* Ajout unification pattern dans l'algorithme d'unification desGravatar herbelin2006-09-12
* Prise en compte de l'instance des evars dans la détection des 'motifs'Gravatar herbelin2006-08-29
* Diverses modifications autour de l'unification modulo conversion:Gravatar herbelin2006-08-28
* Fixes for new unification, not used in default version as it really changes u...Gravatar msozeau2006-04-10
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...Gravatar msozeau2006-04-10
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* Changement des named_contextGravatar gregoire2005-12-02
* reparations de quelques petits bugs d\'unification + introduction de la notio...Gravatar barras2005-06-07
* essai de typage des instantiations d\'evarsGravatar barras2005-06-06
* eradication de Evarutil.w_DefineGravatar barras2005-06-05
* Fix bug #931: leave dependent evars as such for refineGravatar herbelin2005-03-08
* Correction d'un bug historique de do_restrict_hyps + code mortGravatar herbelin2004-12-08
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* 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
* Suppression de Rawterm.loc, branchement sur Util.locGravatar herbelin2004-07-16
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* Reparation d'une rupture (en presence de types implicites) de l'invariant que...Gravatar herbelin2004-01-29
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...Gravatar herbelin2002-04-11
* Amélioration des messages d'erreurs concernant l'inférence des implicitesGravatar herbelin2002-04-10
* Introduction d'univers frais dans les types implicites engendrés par le pré...Gravatar herbelin2001-11-08
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...Gravatar herbelin2001-09-14
* Préparation du prétypage à la mise en place d'univers algébriquesGravatar herbelin2001-09-09
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)Gravatar herbelin2001-05-10
* deux fois $Id$Gravatar filliatr2001-03-29
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Branchement du mécanisme d'instantiation des Evar en présence de définitio...Gravatar herbelin2000-11-27
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02