| Commit message (Expand) | Author | Age |
|---|
| * | Misc improvements about evar_map |  letouzey | 2010-12-15 |
| * | Updated all headers for 8.3 and trunk |  herbelin | 2010-07-24 |
| * | Added Chung-Kil Hur's smart "pattern" tactic (h_resolve). | herbelin | 2010-06-22 |
| * | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
| * | Improved the efficiency of evars traverals thanks to a split of | herbelin | 2010-05-13 |
| * | Deux commentaires retirés de ocamldoc. |  aspiwack | 2010-05-07 |
| * | Various minor improvements of comments in mli for ocamldoc | letouzey | 2010-04-29 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Move from ocamlweb to ocamdoc to generate mli documentation |  pboutill | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
| * | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin | 2009-12-24 |
| * | Attached evar source to the evar_info and add location to tclWITHHOLES errors | herbelin | 2009-12-22 |
| * | In "progress", extending the set of evars w/o solving an existing one is | herbelin | 2009-12-21 |
| * | Promote evar_defs to evar_map (in Evd) |  glondu | 2009-11-11 |
| * | - Fixed a bug in checking that implicit arguments are all correctly | herbelin | 2009-09-18 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | Backtrack on experimental unification with sort variables: it requires |  msozeau | 2009-06-02 |
| * | Change unification with sort constraints to not use the kernel | msozeau | 2009-06-01 |
| * | Populate the sort constraints set correctly during unification. Add a | msozeau | 2009-05-27 |
| * | A try at using sort variables during unification. Instead of refreshing | msozeau | 2009-05-23 |
| * | - Fixing bug #2084 (unification not checking sort constraints), hoping | herbelin | 2009-04-08 |
| * | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau | 2009-03-28 |
| * | Backtrack sur la mémoïsation de nf_evar. | aspiwack | 2009-03-04 |
| * | =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=... | aspiwack | 2009-02-27 |
| * | On passe les last_mods (un des champs de Evd.evar_defs) de list | aspiwack | 2009-02-20 |
| * | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack | 2009-02-19 |
| * | Really compare evar maps in progress, due to merging in apply and other | msozeau | 2009-01-23 |
| * | DISCLAIMER |  puech | 2009-01-17 |
| * | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin | 2008-10-26 |
| * | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin | 2008-10-18 |
| * | Better handling of the opacity of proof obligations, add the possibility of | msozeau | 2008-09-07 |
| * | Évolutions diverses et variées. | herbelin | 2008-08-04 |
| * | Mise en place d'un algorithme d'inversion des contraintes de type lors | herbelin | 2008-05-05 |
| * | Quelques bricoles autour de l'unification: | herbelin | 2008-04-27 |
| * | Prise en compte des coercions dans les clauses "with" même si le type | herbelin | 2008-04-23 |
| * | Diverses corrections | herbelin | 2008-04-14 |
| * | Correct bug introduced in r10589, where we lost information that | msozeau | 2008-03-21 |
| * | Pas très propre de reposer sur la capture des anomalies (et cela | herbelin | 2008-03-10 |
| * | Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145) | herbelin | 2008-03-10 |
| * | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin | 2007-10-03 |
| * | Complément aux commits 10124 et 10125 sur l'inférence de type (correction | herbelin | 2007-09-26 |
| * | Raffinement de l'algorithme d'inférence de type | herbelin | 2007-09-17 |
| * | Toujours l'unification de apply : nouveau raffinement pour ne tester | herbelin | 2007-06-06 |
| * | Correction d'un bug dans l'affichage du message d'erreur real_clean | herbelin | 2007-05-29 |
| * | Contrôle de la compatibilité de apply via une information dans les | herbelin | 2007-05-28 |
| * | Suite restructuration unification et division des problèmes | herbelin | 2007-05-23 |
| * | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin | 2007-05-22 |
| * | Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le | herbelin | 2007-05-21 |
| * | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin | 2007-05-20 |
| * | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau | 2007-03-19 |
letouzey
herbelin
aspiwack
pboutill
glondu
msozeau
puech