aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.mli
Commit message (Expand)AuthorAge
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Diverses corrections Gravatar herbelin2008-04-14
* Correct bug introduced in r10589, where we lost information thatGravatar msozeau2008-03-21
* Pas très propre de reposer sur la capture des anomalies (et celaGravatar herbelin2008-03-10
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* 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
* Toujours l'unification de apply : nouveau raffinement pour ne testerGravatar herbelin2007-06-06
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Contrôle de la compatibilité de apply via une information dans lesGravatar herbelin2007-05-28
* Suite restructuration unification et division des problèmesGravatar herbelin2007-05-23
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Essai d'une nouvelle heuristique pour clenv_unique_resolver : si leGravatar herbelin2007-05-21
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESGravatar herbelin2007-02-21
* 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
* 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
* reparations de quelques petits bugs d\'unification + introduction de la notio...Gravatar barras2005-06-07
* Ajout foldGravatar herbelin2005-03-08
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* 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