aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
AgeCommit message (Expand)Author
2011-03-23- Remove useless grammar rulemsozeau
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2011-03-11- Better error messages taking unif. constraints into account.msozeau
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
2011-03-10Do not forget conv_pbs when resetting an evm: msozeau
2011-02-17- Use transparency information all the way through unification andmsozeau
2010-12-15Misc improvements about evar_mapletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-03-15Stop dropping evar constraints when building a new goal evar defs.msozeau
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-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-24Temporary fixes in unification:msozeau
2009-05-23A try at using sort variables during unification. Instead of refreshingmsozeau
2009-04-08Some dead code removal + cleanupsletouzey
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-20On ne met plus rien dans les last_mods tant que conv_pbs est vide.aspiwack
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-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-14Diverses corrections herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
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-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin