aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/clenv.mli
Commit message (Expand)AuthorAge
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Solde de code mort et petites optimisations sur lesquels je suisGravatar herbelin2008-02-09
* Mise en place d'une toute petite amélioration de l'unification deGravatar herbelin2008-02-07
* Uniformisation du comportement de rewrite et rewrite in : quand leGravatar herbelin2007-10-12
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Ajout fonction clenv_conv_leq pour résoudre les pbs de la formeGravatar herbelin2007-02-22
* Correction d'une tentative incorrecte (révision 9266) de clarificationGravatar herbelin2006-10-25
* Ajout de la tactique "apply in".Gravatar herbelin2006-10-24
* Orthographe de 'instantiate'Gravatar herbelin2005-12-17
* Added clenv_environments_evars that behaves as clen_environments butGravatar sacerdot2005-05-24
* A wish by Bas Spitters granted: a little more of unification up toGravatar sacerdot2005-05-19
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* 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
* simplification de clenvGravatar barras2004-09-10
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* deplacement de clenv vers pretypingGravatar barras2004-09-03