index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evarutil.mli
Commit message (
Expand
)
Author
Age
...
*
Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
herbelin
2008-04-25
*
Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)
herbelin
2008-03-10
*
Move generally useful definition of nf_evar on contexts to evarutil.
msozeau
2008-02-08
*
Complément aux commits 10124 et 10125 sur l'inférence de type (correction
herbelin
2007-09-26
*
Raffinement de l'algorithme d'inférence de type
herbelin
2007-09-17
*
Correction d'un bug dans check_and_clear_in_constr + simplification de
notin
2007-01-31
*
Nouvelle implantation de clear_hyps
notin
2007-01-30
*
Correction du bug #1315:
notin
2007-01-22
*
Report de l'heuristique d'unification premier ordre flexible/rigide
herbelin
2006-09-15
*
Ajout unification pattern dans l'algorithme d'unification des
herbelin
2006-09-12
*
Prise en compte de l'instance des evars dans la détection des 'motifs'
herbelin
2006-08-29
*
Diverses modifications autour de l'unification modulo conversion:
herbelin
2006-08-28
*
Fixes for new unification, not used in default version as it really changes u...
msozeau
2006-04-10
*
Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...
msozeau
2006-04-10
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
Changement des named_context
gregoire
2005-12-02
*
reparations de quelques petits bugs d\'unification + introduction de la notio...
barras
2005-06-07
*
essai de typage des instantiations d\'evars
barras
2005-06-06
*
eradication de Evarutil.w_Define
barras
2005-06-05
*
Fix bug #931: leave dependent evars as such for refine
herbelin
2005-03-08
*
Correction d'un bug historique de do_restrict_hyps + code mort
herbelin
2004-12-08
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Suppression de Rawterm.loc, branchement sur Util.loc
herbelin
2004-07-16
*
updated printing of evar context (may loop ?)
corbinea
2004-06-30
*
Reparation d'une rupture (en presence de types implicites) de l'invariant que...
herbelin
2004-01-29
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...
herbelin
2002-04-11
*
Amélioration des messages d'erreurs concernant l'inférence des implicites
herbelin
2002-04-10
*
Introduction d'univers frais dans les types implicites engendrés par le pré...
herbelin
2001-11-08
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...
herbelin
2001-09-14
*
Préparation du prétypage à la mise en place d'univers algébriques
herbelin
2001-09-09
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)
herbelin
2001-05-10
*
deux fois $Id$
filliatr
2001-03-29
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Branchement du mécanisme d'instantiation des Evar en présence de définitio...
herbelin
2000-11-27
*
correction Abstract (et make world passe!)
filliatr
2000-11-02
*
Petit nettoyage de Evarutil et Evarconv
herbelin
2000-10-23
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
[prev]
[next]