aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.mli
AgeCommit message (Expand)Author
2009-12-24Opened the possibility to type Ltac patterns but it is not fully functional yetherbelin
2009-12-22Attached evar source to the evar_info and add location to tclWITHHOLES errorsherbelin
2009-12-21In "progress", extending the set of evars w/o solving an existing one isherbelin
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-09-18- Fixed a bug in checking that implicit arguments are all correctlyherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-06-02Backtrack on experimental unification with sort variables: it requires msozeau
2009-06-01Change unification with sort constraints to not use the kernelmsozeau
2009-05-27Populate the sort constraints set correctly during unification. Add amsozeau
2009-05-23A try at using sort variables during unification. Instead of refreshingmsozeau
2009-04-08- Fixing bug #2084 (unification not checking sort constraints), hopingherbelin
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-04Backtrack sur la mémoïsation de nf_evar.aspiwack
2009-02-27=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...aspiwack
2009-02-20On passe les last_mods (un des champs de Evd.evar_defs) de listaspiwack
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-01-23Really compare evar maps in progress, due to merging in apply and othermsozeau
2009-01-17DISCLAIMERpuech
2008-10-26Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiherbelin
2008-10-18Optimisation de clenv.ml pour que meta_instance ne soit pas appeléherbelin
2008-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
2008-08-04Évolutions diverses et variées.herbelin
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-04-27Quelques bricoles autour de l'unification:herbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-14Diverses corrections herbelin
2008-03-21Correct bug introduced in r10589, where we lost information thatmsozeau
2008-03-10Pas très propre de reposer sur la capture des anomalies (et celaherbelin
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-09-26Complément aux commits 10124 et 10125 sur l'inférence de type (correction herbelin
2007-09-17Raffinement de l'algorithme d'inférence de typeherbelin
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-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-07reparations de quelques petits bugs d\'unification + introduction de la notio...barras
2005-03-08Ajout foldherbelin