aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.ml
Commit message (Expand)AuthorAge
* Modification de la vm:Gravatar notin2007-03-27
* Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESGravatar herbelin2007-02-21
* Correction d'un bug dans check_and_clear_in_constr + simplification deGravatar notin2007-01-31
* Nouvelle implantation de clear_hypsGravatar notin2007-01-30
* Correction du bug #1315:Gravatar notin2007-01-22
* Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...Gravatar herbelin2006-12-12
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* Code mort (duplication de code dans reductionops.ml)Gravatar herbelin2006-11-18
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* Ajout unification pattern dans l'algorithme d'unification desGravatar herbelin2006-09-12
* Ajout (pour complétude) du cas d'inversion d'un pattern de Miller visGravatar herbelin2006-08-29
* Prise en compte de l'instance des evars dans la détection des 'motifs'Gravatar herbelin2006-08-29
* Diverses modifications autour de l'unification modulo conversion:Gravatar herbelin2006-08-28
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Fixes for new unification, not used in default version as it really changes u...Gravatar msozeau2006-04-10
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...Gravatar msozeau2006-04-10
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Orthographe de 'instantiate'Gravatar herbelin2005-12-17
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* backtrack sur le typage des instantiations d\'evarsGravatar barras2005-06-09
* reparations de quelques petits bugs d\'unification + introduction de la notio...Gravatar barras2005-06-07
* essai de typage des instantiations d\'evarsGravatar barras2005-06-06
* eradication de Evarutil.w_DefineGravatar barras2005-06-05
* assouplissement de real_clean: ne tient pas compte des occcurences flexibles ...Gravatar barras2005-06-05
* unification: evar_define checks the free variables are bound in the evar contextGravatar barras2005-05-28
* WARNING: unification changed (to fix a bug).Gravatar sacerdot2005-05-24
* Backtrack version 1.82 awaiting for better understanding of the consequences ...Gravatar herbelin2005-03-12
* Méthode plus raisonnable pour supprimer l'inefficacité des evars dépendant...Gravatar herbelin2005-03-11
* bug #931 (continued): no recursion on the evars instantiationGravatar herbelin2005-03-09
* Fix bug #931: leave dependent evars as such for refineGravatar herbelin2005-03-08
* Code mortGravatar herbelin2005-03-01
* Achèvement correction bug do_restrict_hys: ne pas inverser les argumentsGravatar herbelin2004-12-09
* Correction d'un bug historique de do_restrict_hyps + code mortGravatar herbelin2004-12-08
* C'est trop compliqué de mettre à jour les types du metamap en passant sous ...Gravatar herbelin2004-12-06
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* unification encore...Gravatar barras2004-09-08
* petit bug avec les effets de bordsGravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* bug #794: conv made in wrong envGravatar barras2004-07-13
* bug #790: better error_not_cleanGravatar barras2004-07-13
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* Reparation d'une rupture (en presence de types implicites) de l'invariant que...Gravatar herbelin2004-01-29