index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
pretyping.ml
Commit message (
Expand
)
Author
Age
...
*
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
*
ratrapage exception, deja fait ...
bgregoir
2011-01-11
*
Fixing an uncaught exception bug with use of vmcast
herbelin
2011-01-07
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Improving a few error messages in Ltac interpretation
herbelin
2010-09-11
*
Fix [clenv_missing] to compute a better approximation of missing
msozeau
2010-08-02
*
Minor fixes:
msozeau
2010-07-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Documentation of pretype_id (minor commit).
herbelin
2010-05-28
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
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
*
Fix splitting evars tactics and stop dropping evar constraints when
msozeau
2010-03-15
*
Reorder resolution of type class and unification constraints.
msozeau
2010-03-07
*
Fix treatment of remaining unification constraints: raise a more
msozeau
2010-03-07
*
Opened the possibility to type Ltac patterns but it is not fully functional yet
herbelin
2009-12-24
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Make usage of Dyn explicit
glondu
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
*
Fixes for r12197, the refined evars were not returned in case fail_evar
msozeau
2009-06-22
*
Use more consistent resolution parameters in Program and regular typing
msozeau
2009-06-18
*
Fix "unsatisfiable constraints" error messages to include all the
msozeau
2009-06-18
*
When typing a non-dependent arrow, do not put the (anonymous) variable
msozeau
2009-06-11
*
- New cleaning phase for the entry points of pretyping.ml
herbelin
2009-04-24
*
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
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
Apply vmconv if there are no _undefined_ evars around.
msozeau
2008-11-08
*
Slight change of the semantics of user-given casts: they don't really
msozeau
2008-11-07
*
Move Record desugaring to constrintern and add ability to use notations
msozeau
2008-11-05
*
More debugging of handling of open constrs with typeclasses:
msozeau
2008-10-25
*
Open notation for declaring record instances.
msozeau
2008-10-23
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Various improvements in handling of evars in general and typing
msozeau
2008-06-21
*
Fixes incorrect handling of existing existentials variables in
msozeau
2008-06-03
*
Mise en place d'un algorithme d'inversion des contraintes de type lors
herbelin
2008-05-05
*
Réutilisation de l'infrastructure pour le polymorphisme d'univers des
herbelin
2008-04-30
*
Little fixes in setoid_rewrite.
msozeau
2008-04-17
*
Fix evar bugs in type classes:
msozeau
2008-04-09
*
- Second pass on implementation of let pattern. Parse "let ' par [as x]?
msozeau
2008-03-28
*
Various fixes on typeclasses:
msozeau
2008-03-27
*
Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)
herbelin
2008-03-10
*
Syntax changes in typeclasses, remove "?" for usual implicit arguments
msozeau
2008-03-06
*
Change implementation of resolution for typeclasses to use a customized
msozeau
2008-02-08
[prev]
[next]