index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
coercion.ml
Commit message (
Expand
)
Author
Age
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
Removing almost all new_untyped_evar, and a bunch of Evd.add.
ppedrot
2013-09-18
*
Uniformization: isevars -> evdref/sigma/evd
herbelin
2013-05-09
*
Small cleaning of Evd interface.
ppedrot
2013-05-06
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
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
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of identifier
ppedrot
2012-12-14
*
Removed some FIXME related to equality on universes.
ppedrot
2012-11-26
*
Monomorphization (pretyping)
ppedrot
2012-11-22
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Fix regression introduced in r15418 that broke MathClasses. In program mode, ...
msozeau
2012-07-11
*
Forward-port fixes from 8.4 (15358, 15353, 15333).
msozeau
2012-06-04
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Avoid unneeded head-normalizations in coercion code.
msozeau
2012-04-25
*
Do not delta-head-normalize the proposition argument of sigma types during co...
msozeau
2012-04-25
*
Fix interface of resolve_typeclasses: onlyargs -> with_goals:
msozeau
2012-03-20
*
Fix bugs related to Program integration.
msozeau
2012-03-19
*
Second step of integration of Program:
msozeau
2012-03-14
*
Remove support for "abstract typing constraints" that requires unicity of sol...
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
Fixing use of type constraint for refining the "return" clause of "match".
herbelin
2011-10-25
*
Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v
herbelin
2011-04-08
*
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
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Cleaning the use of parentheses around evd and evdref (cosmetic commit).
herbelin
2010-10-31
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphic
herbelin
2010-03-28
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Jolification : tentative de supprimer les "( evd)" et associés qui
aspiwack
2009-07-07
*
Try typeclass resolution in coercion if no solution can be found to a
msozeau
2009-06-18
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about
herbelin
2008-09-02
*
Various improvements in handling of evars in general and typing
msozeau
2008-06-21
*
Mise en place d'un algorithme d'inversion des contraintes de type lors
herbelin
2008-05-05
*
- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec
herbelin
2008-04-26
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
[next]