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
*
Modification de la vm:
notin
2007-03-27
*
Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES
herbelin
2007-02-21
*
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
*
Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...
herbelin
2006-12-12
*
Correction bug #1041 (double cause : non évitement des noms existants en
herbelin
2006-12-12
*
Code mort (duplication de code dans reductionops.ml)
herbelin
2006-11-18
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
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
*
Ajout (pour complétude) du cas d'inversion d'un pattern de Miller vis
herbelin
2006-08-29
*
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
*
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
[next]