aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.ml
Commit message (Expand)AuthorAge
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envGravatar herbelin2013-01-29
* Monomorphization (proof)Gravatar ppedrot2012-11-25
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Revise API of understand_ltac to be parameterized by a flag for resolution of...Gravatar msozeau2012-03-14
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* 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
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Take constraints into account in the "instantiate" tacticGravatar herbelin2009-10-30
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et unifo...Gravatar notin2007-04-26
* Report de révision 9583 de la v8.1 dans le trunkGravatar notin2007-02-01
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* bypass w_Define when w_refine-ingGravatar corbinea2004-07-07
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* more evar stuffGravatar corbinea2004-06-28
* effective evar refiningGravatar corbinea2004-06-26
* Amélioration du message d'erreur "w_unify"Gravatar clrenard2003-12-01
* Amelioration du message d'erreur en cas de tentative d'instanciationGravatar clrenard2003-11-15
* factorisation et generalisation des clausesGravatar barras2003-11-13