aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
AgeCommit message (Expand)Author
2007-09-26Complément aux commits 10124 et 10125 sur l'inférence de type (correction herbelin
2007-09-18Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)herbelin
2007-09-17Raffinement de l'algorithme d'inférence de typeherbelin
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
2007-06-06Toujours l'unification de apply : nouveau raffinement pour ne testerherbelin
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
2007-05-23Suite restructuration unification et division des problèmesherbelin
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin
2007-05-21Essai d'une nouvelle heuristique pour clenv_unique_resolver : si leherbelin
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-02-21Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESherbelin
2007-01-22Correction du bug #1315:notin
2006-11-19Raffinement de l'unification de "apply": mémorisation de certainsherbelin
2006-09-20Declarative Proof Language: main commitcorbinea
2006-09-15Débogage: ajout affichage contraintes d'unificationherbelin
2006-09-05Workaround Map.fold semantic change in ocaml-3.08.4 and higher.msozeau
2006-04-28Standardisation du nom des méthodes de Evdherbelin
2006-04-07- Documentation of the Program tactics.msozeau
2005-12-05changement d'egalite pour le named_context_valgregoire
2005-12-02Changement des named_contextgregoire
2005-06-07pas de filtrages partielsbarras
2005-06-07reparations de quelques petits bugs d\'unification + introduction de la notio...barras
2005-06-06essai de typage des instantiations d\'evarsbarras
2005-06-05eradication de Evarutil.w_Definebarras
2005-03-08Ajout foldherbelin
2004-12-08Bug nom exceptionherbelin
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-09-23error if binder was already definedbarras
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-07-16Nouvelle en-têteherbelin
2004-06-30updated printing of evar context (may loop ?)corbinea
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras