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
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
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
*
Orthographe de 'instantiate'
herbelin
2005-12-17
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
backtrack sur le typage des instantiations d\'evars
barras
2005-06-09
*
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
*
assouplissement de real_clean: ne tient pas compte des occcurences flexibles ...
barras
2005-06-05
*
unification: evar_define checks the free variables are bound in the evar context
barras
2005-05-28
*
WARNING: unification changed (to fix a bug).
sacerdot
2005-05-24
*
Backtrack version 1.82 awaiting for better understanding of the consequences ...
herbelin
2005-03-12
*
Méthode plus raisonnable pour supprimer l'inefficacité des evars dépendant...
herbelin
2005-03-11
*
bug #931 (continued): no recursion on the evars instantiation
herbelin
2005-03-09
*
Fix bug #931: leave dependent evars as such for refine
herbelin
2005-03-08
*
Code mort
herbelin
2005-03-01
*
Achèvement correction bug do_restrict_hys: ne pas inverser les arguments
herbelin
2004-12-09
*
Correction d'un bug historique de do_restrict_hyps + code mort
herbelin
2004-12-08
*
C'est trop compliqué de mettre à jour les types du metamap en passant sous ...
herbelin
2004-12-06
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
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
*
unification encore...
barras
2004-09-08
*
petit bug avec les effets de bords
barras
2004-09-08
*
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
*
bug #794: conv made in wrong env
barras
2004-07-13
*
bug #790: better error_not_clean
barras
2004-07-13
*
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
*
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
[next]