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
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
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
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
petite modif pour ne pas expanser trop de let pendant l'unification
barras
2002-02-12
*
substitution et pattern modulo let
barras
2002-02-11
*
compat ocaml 3.03
filliatr
2001-12-13
*
Bug mauvaise instance
herbelin
2001-11-20
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
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
*
Passage aux univers algébriques
herbelin
2001-09-09
*
Préparation du prétypage à la mise en place d'univers algébriques
herbelin
2001-09-09
*
has_undefined_isevars était buggé
herbelin
2001-07-06
*
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
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
Prise en compte des Let dans l'instance des evars
herbelin
2001-03-14
*
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
Nouveaux bugs instanciation d'evar par des evar
herbelin
2001-01-19
*
Rajout de la restriction de l'instance en cas d'unification de 2 variables ex...
herbelin
2001-01-04
*
Oubli test de correction à l'instantiation des evars
herbelin
2000-12-14
*
Branchement du mécanisme d'instantiation des Evar en présence de définitio...
herbelin
2000-11-27
*
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...
herbelin
2000-11-06
*
correction Abstract (et make world passe!)
filliatr
2000-11-02
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Petit nettoyage de Evarutil et Evarconv
herbelin
2000-10-23
*
Bug indices dans l'instance d'une evar
herbelin
2000-10-21
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Renommage AppL en App
herbelin
2000-10-01
*
renommage map_constr_with_named_binders
herbelin
2000-10-01
*
Abstraction de constr
herbelin
2000-09-14
*
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
herbelin
2000-09-12
*
Correction pour make doc
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Séparation des contraintes de type et de valeur dans pretyping
herbelin
2000-06-29
*
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
herbelin
2000-06-01
*
Nettoyage de Generic
herbelin
2000-05-31
*
Bug existential_value au lieu de existential_type + divers sur existential
herbelin
2000-05-25
*
Bug de cast
herbelin
2000-05-23
*
Inlining prod_create
herbelin
2000-03-21
*
*** empty log message ***
barras
2000-03-10
*
Reparation bug isevars dans pretyping
herbelin
2000-03-10
[next]