index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evarutil.ml
Commit message (
Expand
)
Author
Age
*
Fixing Derive Inversion for new proof engine
herbelin
2010-05-26
*
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
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Fixed bugs from commit 12954 on unification complexity
herbelin
2010-04-20
*
Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).
herbelin
2010-04-19
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
In "progress", extending the set of evars w/o solving an existing one is
herbelin
2009-12-21
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Reverted an incorrect code simplification in function status_changed
herbelin
2009-11-02
*
Take constraints into account in the "instantiate" tactic
herbelin
2009-10-30
*
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
*
Made unification patch 12268 even more ad hoc (if evars remain in a
herbelin
2009-08-13
*
Relatively ad hoc fix to an ill-typed instantiation bug in type
herbelin
2009-08-11
*
Don't use recent ocaml tolerance for pattern "ProjectVar _" when
herbelin
2009-07-08
*
Add heuristic based on non-linearity of evars to determine whether an
herbelin
2009-07-08
*
Fixing bug 2129 (evar introduced to remember an ambiguous projection
herbelin
2009-07-08
*
Jolification : tentative de supprimer les "( evd)" et associés qui
aspiwack
2009-07-07
*
documented a bug of pattern unification with metas
barras
2009-06-22
*
A try at using sort variables during unification. Instead of refreshing
msozeau
2009-05-23
*
- Fixing #2090 (occur check missing when trying to solve evar-evar equation).
herbelin
2009-04-25
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
- Fixing bug #2084 (unification not checking sort constraints), hoping
herbelin
2009-04-08
*
Fix obvious bug in evars_of_named_context.
msozeau
2009-04-03
*
Fixes to make Ynot compile with the trunk:
msozeau
2009-03-20
*
Backtrack sur la mémoïsation de nf_evar.
aspiwack
2009-03-04
*
=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...
aspiwack
2009-02-27
*
On passe les last_mods (un des champs de Evd.evar_defs) de list
aspiwack
2009-02-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
*
From v8.2 to trunk:
herbelin
2009-02-06
*
- Fixing bug 1891 (abusive instantiations of evar arguments in
herbelin
2009-01-20
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
*
DISCLAIMER
puech
2009-01-17
*
Completed 11745 (move of jprover to user contribs) and cleaned 11743
herbelin
2009-01-05
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
fixed problem with r11612
barras
2008-11-21
*
- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in
herbelin
2008-11-09
*
Fix universe problem appearing ConCaT using the existing infrastructure for
msozeau
2008-11-07
*
Fix in the unification algorithm using evars: unify types of evar
msozeau
2008-11-05
*
Partial fix for bug #1948: recompute order of dependencies between
msozeau
2008-09-25
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Modification rapide du message d'erreur lorsqu'un _ ne peut être
herbelin
2008-07-18
*
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
*
Various improvements in handling of evars in general and typing
msozeau
2008-06-21
*
Correction bug 1878 (utilisation de extend_evar déplacée là où une
herbelin
2008-06-14
[next]