index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
/
evars.v
Commit message (
Expand
)
Author
Age
*
An optimization in the use of unification candidates so as to get the
Hugo Herbelin
2015-01-01
*
Fixing orientation of postponed subtyping problems.
Hugo Herbelin
2014-12-10
*
Improving evar restriction (this is a risky change, as I remember a
Hugo Herbelin
2014-12-07
*
Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.
herbelin
2013-03-21
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Evarconv: Fix #2936 + comments
pboutill
2012-11-28
*
Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.
ppedrot
2012-06-12
*
Unification: Added a heuristic to solve problems of the form
herbelin
2012-03-26
*
Type inference unification: fixed a 8.4 bug in the presence of unification
herbelin
2012-01-04
*
Discarding let-ins from the instances of the evars in the
herbelin
2011-12-04
*
Fixing another bug revealing ill-typed use of evar restriction.
herbelin
2011-10-24
*
Improved define_evar_as_lambda which was creating an unrelated new evar
herbelin
2011-03-05
*
Improve handling of metas as evars in unification (patch by Hugo)
letouzey
2010-09-30
*
Attempt to capture on time unification errors for "with" bindings.
herbelin
2009-10-30
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Fixing #2090 (occur check missing when trying to solve evar-evar equation).
herbelin
2009-04-25
*
From v8.2 to trunk:
herbelin
2009-02-06
*
Correction de bugs:
herbelin
2008-08-05
*
Préférence donnée aux constantes qui ne sont pas des projections
herbelin
2008-06-29
*
Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk
herbelin
2008-06-18
*
Complément aux commits 10124 et 10125 sur l'inférence de type (correction
herbelin
2007-09-26
*
Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)
herbelin
2007-09-18
*
Raffinement de l'algorithme d'inférence de type
herbelin
2007-09-17
*
Réponse à une incompatibilité introduite dans 10114 (calcul du nombre
herbelin
2007-09-16
*
Report de l'heuristique d'unification premier ordre flexible/rigide
herbelin
2006-09-15
*
Adaptation au passage de option dans Type
herbelin
2006-05-28
*
Ajout test relatif au bug #984
herbelin
2006-03-05
*
Ajout test bug 1089
herbelin
2006-03-02
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
Ajout bug do_restrict_hyp
herbelin
2004-12-08
*
Test bug 705
herbelin
2004-04-29
*
Il ne doit plus y avoir de preuves non terminées à la sortie du fichier
herbelin
2003-01-19
*
La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...
herbelin
2001-11-21
*
*** empty log message ***
herbelin
2001-11-16
*
entetes
filliatr
2001-03-15
*
*** empty log message ***
herbelin
2001-03-14