aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.ml
Commit message (Expand)AuthorAge
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Backtrack on experimental unification with sort variables: it requires Gravatar msozeau2009-06-02
* Change unification with sort constraints to not use the kernelGravatar msozeau2009-06-01
* Populate the sort constraints set correctly during unification. Add aGravatar msozeau2009-05-27
* Temporary fixes in unification:Gravatar msozeau2009-05-24
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...Gravatar aspiwack2009-02-27
* On passe les last_mods (un des champs de Evd.evar_defs) de listGravatar aspiwack2009-02-20
* On ne met plus rien dans les last_mods tant que conv_pbs est vide.Gravatar aspiwack2009-02-20
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Really compare evar maps in progress, due to merging in apply and otherGravatar msozeau2009-01-23
* DISCLAIMERGravatar puech2009-01-17
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Better handling of the opacity of proof obligations, add the possibility ofGravatar msozeau2008-09-07
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Diverses corrections Gravatar herbelin2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* 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
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* 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
* Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)Gravatar herbelin2007-09-18
* Raffinement de l'algorithme d'inférence de typeGravatar herbelin2007-09-17
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* 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
* 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