index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
vnorm.ml
Commit message (
Expand
)
Author
Age
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Removing useless casts between arrays and lists.
ppedrot
2013-08-04
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Restrict (try...with...) to avoid catching critical exn (part 7)
letouzey
2013-03-13
*
Term.dest* functions now raise specific DestKO exn instead of Invalid_argument
letouzey
2013-03-12
*
More informative error when a global reference is used in a context of
herbelin
2013-02-28
*
Modulification of identifier
ppedrot
2012-12-14
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Fixing vm_compute bug #2729 (function used to decompose constructors
herbelin
2012-03-13
*
fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...
barras
2010-07-29
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Correcting a delta normalization bug in VM (checked by benjamin)
jforest
2008-09-30
*
fixed bug #1780: a lift was missing (match predicate)
barras
2008-05-29
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
Nettoyage de code en vue de la release. Plus de Warning: Unused
aspiwack
2007-12-18
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Protection contre les warnings 'unused variable' de ocaml 3.09
herbelin
2007-01-19
*
correction du bug : VM value extraction error (PR#1290)
bgregoir
2006-11-29
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
- Ajout d'un cast vm dans la syntaxe : x <: t
bgregoir
2006-07-22