| Age | Commit message (Expand) | Author |
| 2011-03-23 | - Remove useless grammar rule | msozeau |
| 2011-03-11 | Tentative to make unification check types at every instanciation of an | msozeau |
| 2011-03-11 | - Better error messages taking unif. constraints into account. | msozeau |
| 2011-03-10 | Forgot a use of evars_reset_evd in nf_evars, add an optional argument as | msozeau |
| 2011-03-10 | Do not forget conv_pbs when resetting an evm: | msozeau |
| 2011-02-17 | - Use transparency information all the way through unification and | msozeau |
| 2010-12-15 | Misc improvements about evar_map | letouzey |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | Added Chung-Kil Hur's smart "pattern" tactic (h_resolve). | herbelin |
| 2010-06-12 | Fixed bug #2135 (second-order unification was raising cryptic message) | herbelin |
| 2010-05-13 | Improved the efficiency of evars traverals thanks to a split of | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-03-15 | Stop dropping evar constraints when building a new goal evar defs. | msozeau |
| 2009-12-24 | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin |
| 2009-12-22 | Attached evar source to the evar_info and add location to tclWITHHOLES errors | herbelin |
| 2009-12-21 | In "progress", extending the set of evars w/o solving an existing one is | herbelin |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-06-02 | Backtrack on experimental unification with sort variables: it requires | msozeau |
| 2009-06-01 | Change unification with sort constraints to not use the kernel | msozeau |
| 2009-05-27 | Populate the sort constraints set correctly during unification. Add a | msozeau |
| 2009-05-24 | Temporary fixes in unification: | msozeau |
| 2009-05-23 | A try at using sort variables during unification. Instead of refreshing | msozeau |
| 2009-04-08 | Some dead code removal + cleanups | letouzey |
| 2009-04-08 | - Fixing bug #2084 (unification not checking sort constraints), hoping | herbelin |
| 2009-03-28 | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau |
| 2009-03-04 | Backtrack 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-20 | On passe les last_mods (un des champs de Evd.evar_defs) de list | aspiwack |
| 2009-02-20 | On ne met plus rien dans les last_mods tant que conv_pbs est vide. | aspiwack |
| 2009-02-19 | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack |
| 2009-01-23 | Really compare evar maps in progress, due to merging in apply and other | msozeau |
| 2009-01-17 | DISCLAIMER | puech |
| 2008-10-26 | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-09-07 | Better handling of the opacity of proof obligations, add the possibility of | msozeau |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-05-05 | Mise en place d'un algorithme d'inversion des contraintes de type lors | herbelin |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-14 | Diverses corrections | herbelin |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-03-21 | Correct bug introduced in r10589, where we lost information that | msozeau |
| 2008-03-10 | 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 |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |