aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.ml
Commit message (Expand)AuthorAge
* Correction du bug #1315:Gravatar notin2007-01-22
* Raffinement de l'unification de "apply": mémorisation de certainsGravatar herbelin2006-11-19
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Débogage: ajout affichage contraintes d'unificationGravatar herbelin2006-09-15
* Workaround Map.fold semantic change in ocaml-3.08.4 and higher.Gravatar msozeau2006-09-05
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* changement d'egalite pour le named_context_valGravatar gregoire2005-12-05
* Changement des named_contextGravatar gregoire2005-12-02
* pas de filtrages partielsGravatar barras2005-06-07
* 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
* Ajout foldGravatar herbelin2005-03-08
* Bug nom exceptionGravatar herbelin2004-12-08
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* error if binder was already definedGravatar barras2004-09-23
* 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
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05