index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
evd.ml
Age
Commit message (
Expand
)
Author
2007-09-26
Complément aux commits 10124 et 10125 sur l'inférence de type (correction
herbelin
2007-09-18
Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)
herbelin
2007-09-17
Raffinement de l'algorithme d'inférence de type
herbelin
2007-09-06
Uniformisation politique de nommage evd/isevars (evd si evar_defs,
herbelin
2007-06-06
Toujours l'unification de apply : nouveau raffinement pour ne tester
herbelin
2007-05-29
Correction d'un bug dans l'affichage du message d'erreur real_clean
herbelin
2007-05-28
Contrôle de la compatibilité de apply via une information dans les
herbelin
2007-05-23
Suite restructuration unification et division des problèmes
herbelin
2007-05-22
Nouvelle stratégie d'unification des types des with-bindings dans
herbelin
2007-05-21
Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le
herbelin
2007-05-20
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-03-19
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-02-21
Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES
herbelin
2007-01-22
Correction du bug #1315:
notin
2006-11-19
Raffinement de l'unification de "apply": mémorisation de certains
herbelin
2006-09-20
Declarative Proof Language: main commit
corbinea
2006-09-15
Débogage: ajout affichage contraintes d'unification
herbelin
2006-09-05
Workaround Map.fold semantic change in ocaml-3.08.4 and higher.
msozeau
2006-04-28
Standardisation du nom des méthodes de Evd
herbelin
2006-04-07
- Documentation of the Program tactics.
msozeau
2005-12-05
changement d'egalite pour le named_context_val
gregoire
2005-12-02
Changement des named_context
gregoire
2005-06-07
pas de filtrages partiels
barras
2005-06-07
reparations de quelques petits bugs d\'unification + introduction de la notio...
barras
2005-06-06
essai de typage des instantiations d\'evars
barras
2005-06-05
eradication de Evarutil.w_Define
barras
2005-03-08
Ajout fold
herbelin
2004-12-08
Bug nom exception
herbelin
2004-11-16
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-10-20
COMMITED BYTECODE COMPILER
barras
2004-09-23
error if binder was already defined
barras
2004-09-17
restructuration des printers: proofs passe avant parsing
barras
2004-09-15
hiding the meta_map in evar_defs
barras
2004-09-12
inclusion de meta_map dans evar_defs
barras
2004-09-03
premiere reorganisation de l\'unification
barras
2004-07-16
Nouvelle en-tête
herbelin
2004-06-30
updated printing of evar context (may loop ?)
corbinea
2003-09-06
Paramétrisation vis à vis de existential_key
herbelin
2001-11-06
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-05
GROS COMMIT:
barras
[prev]