index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evarconv.ml
Commit message (
Expand
)
Author
Age
...
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
Tentative to make unification check types at every instanciation of an
msozeau
2011-03-11
*
Reverted commit r13893 about propagation of more informative
herbelin
2011-03-07
*
Revert commit r13883: instantiating ?n by a lambda when "?n a" has to
herbelin
2011-03-07
*
Added propagation of evars unification failure reasons for better
herbelin
2011-03-07
*
Added support for instantiation of ?n by a lambda when "?n a" has to
herbelin
2011-03-05
*
Reorganized a bit evarconv.ml:
herbelin
2011-03-05
*
- Use transparency information all the way through unification and
msozeau
2011-02-17
*
Added eta-expansion in kernel, type inference and tactic unification,
herbelin
2010-09-20
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Fix bug 2307
pboutill
2010-05-20
*
Improved the efficiency of evars traverals thanks to a split of
herbelin
2010-05-13
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Added a function in typing.ml to solve evars of a constr w/o going back down ...
herbelin
2010-04-05
*
Fix treatment of remaining unification constraints: raise a more
msozeau
2010-03-07
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Relatively ad hoc fix to an ill-typed instantiation bug in type
herbelin
2009-08-11
*
Jolification : tentative de supprimer les "( evd)" et associés qui
aspiwack
2009-07-07
*
change in the order of unification constraints solving (for canonical structu...
amahboub
2009-07-06
*
Backtrack on experimental unification with sort variables: it requires
msozeau
2009-06-02
*
Properly catch sort constraint inconsistency exception in
msozeau
2009-05-28
*
Populate the sort constraints set correctly during unification. Add a
msozeau
2009-05-27
*
A try at using sort variables during unification. Instead of refreshing
msozeau
2009-05-23
*
fix a bug in canonical structures (bug found and fixed by Cyril)
barras
2009-05-09
*
Fixes to make Ynot compile with the trunk:
msozeau
2009-03-20
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
memoized is_ground_env
barras
2009-02-09
*
pushed evar reduction in kernel
barras
2009-02-06
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
fixed problem with r11612
barras
2008-11-21
*
fixed exponential behavior of evar unif (ground case)
barras
2008-11-21
*
Fix universe problem appearing ConCaT using the existing infrastructure for
msozeau
2008-11-07
*
Correction de bugs:
herbelin
2008-08-05
*
Suite 11187 et 11298 : ne retarder le dépliage d'une projection
herbelin
2008-08-05
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Correction d'un bug dans l'analyse des contraintes non résolues
herbelin
2008-06-29
*
Préférence donnée aux constantes qui ne sont pas des projections
herbelin
2008-06-29
*
Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)
herbelin
2008-06-21
*
Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk
herbelin
2008-06-18
*
Correction d'un bug de l'unification pattern qui oubliait d'expanser
herbelin
2008-05-20
*
Résolution des problèmes ambigus d'inférence du type de retour des
herbelin
2008-05-14
*
Mise en place d'un algorithme d'inversion des contraintes de type lors
herbelin
2008-05-05
*
Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
herbelin
2008-04-25
*
added products and sorts as possible heads for canonical structures
corbinea
2008-02-19
*
Added default canonical structures (see example in test-suite)
corbinea
2008-02-14
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Amendement à la révision 10124 : déplacement de apprec_nohdbeta entre
herbelin
2007-10-01
*
Raffinement de l'algorithme d'inférence de type
herbelin
2007-09-17
[prev]
[next]