aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.ml
Commit message (Expand)AuthorAge
* - Remove useless grammar ruleGravatar msozeau2011-03-23
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
* Forgot a use of evars_reset_evd in nf_evars, add an optional argument asGravatar msozeau2011-03-10
* Do not forget conv_pbs when resetting an evm: Gravatar msozeau2011-03-10
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Misc improvements about evar_mapGravatar letouzey2010-12-15
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Stop dropping evar constraints when building a new goal evar defs.Gravatar msozeau2010-03-15
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Attached evar source to the evar_info and add location to tclWITHHOLES errorsGravatar herbelin2009-12-22
* In "progress", extending the set of evars w/o solving an existing one isGravatar herbelin2009-12-21
* 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