index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
evar_refiner.ml
Commit message (
Expand
)
Author
Age
*
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-12-17
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Generalizing the use of maps instead of lists in the interpretation
ppedrot
2013-06-22
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
Restrict (try...with...) to avoid catching critical exn (part 12)
letouzey
2013-03-13
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env
herbelin
2013-01-29
*
Monomorphization (proof)
ppedrot
2012-11-25
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
Revise API of understand_ltac to be parameterized by a flag for resolution of...
msozeau
2012-03-14
*
Second step of integration of Program:
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
Reverted commit r13893 about propagation of more informative
herbelin
2011-03-07
*
Added propagation of evars unification failure reasons for better
herbelin
2011-03-07
*
- Use transparency information all the way through unification and
msozeau
2011-02-17
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
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
*
Take constraints into account in the "instantiate" tactic
herbelin
2009-10-30
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Fixing bug #2308 ("instantiate" tactic did not comply with
herbelin
2009-04-24
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Fixes incorrect handling of existing existentials variables in
msozeau
2008-06-03
*
Correction d'un bug dans l'affichage du message d'erreur real_clean
herbelin
2007-05-29
*
Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et unifo...
notin
2007-04-26
*
Report de révision 9583 de la v8.1 dans le trunk
notin
2007-02-01
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
2006-03-22
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
unification encore...
barras
2004-09-08
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
bypass w_Define when w_refine-ing
corbinea
2004-07-07
*
updated printing of evar context (may loop ?)
corbinea
2004-06-30
*
more evar stuff
corbinea
2004-06-28
*
effective evar refining
corbinea
2004-06-26
*
Amélioration du message d'erreur "w_unify"
clrenard
2003-12-01
*
Amelioration du message d'erreur en cas de tentative d'instanciation
clrenard
2003-11-15
*
factorisation et generalisation des clauses
barras
2003-11-13
[next]