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
*
Updating headers.
herbelin
2012-08-08
*
Practical fix for bug #1206 (anomaly raised in pretyping instead of
herbelin
2012-07-06
*
Cleaning opening of the standard List module.
ppedrot
2012-06-28
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Forward-port fixes from 8.4 (15358, 15353, 15333).
msozeau
2012-06-04
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Fix interface of resolve_typeclasses: onlyargs -> with_goals:
msozeau
2012-03-20
*
More adaptations of pretyping/coercion to Program mode.
msozeau
2012-03-19
*
Fix merge and add missing file.
msozeau
2012-03-14
*
Revise API of understand_ltac to be parameterized by a flag for resolution of...
msozeau
2012-03-14
*
Merge fixes
msozeau
2012-03-14
*
Everything compiles again.
msozeau
2012-03-14
*
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
*
A bit of cleaning: unifying push_rels and push_rel_context.
herbelin
2012-03-13
*
Noise for nothing
pboutill
2012-03-02
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
Now consider remaining conversion problems in solve_remaining_evars.
herbelin
2011-10-22
*
It happens that the type inference algorithm (pretyping) did not check
herbelin
2011-10-05
*
Moving implicit tactic support from Tacinterp to Pfedit and final evar
herbelin
2011-09-26
*
Failing instead of switching to the coercion mechanism when VMcast
herbelin
2011-05-15
*
- Make typeclass transparency information directly available
msozeau
2011-04-13
*
- Remove create_evar_defs
msozeau
2011-04-13
*
Replaced printing number of ill-typed branch by printing name of constructor
herbelin
2011-04-08
*
Tentative to make unification check types at every instanciation of an
msozeau
2011-03-11
*
- Better error messages taking unif. constraints into account.
msozeau
2011-03-11
*
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
[next]