aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...Gravatar msozeau2007-06-09
* Unification des types + clause filtrage manquante + uniformisation localeGravatar herbelin2007-06-07
* Toujours l'unification de apply : nouveau raffinement pour ne testerGravatar herbelin2007-06-06
* Amélioration de la complexité de auto (l'utilisation des types dansGravatar herbelin2007-06-05
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Contrôle de la compatibilité de apply via une information dans lesGravatar herbelin2007-05-28
* Unification suite: petits affinements pour préserver la compatibilitéGravatar herbelin2007-05-24
* Tentative d'insertion de coercions avant unification si le type de laGravatar herbelin2007-05-23
* Suite restructuration unification et division des problèmesGravatar herbelin2007-05-23
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Essai d'une nouvelle heuristique pour clenv_unique_resolver : si leGravatar herbelin2007-05-21
* Protection d'un warning par if_verboseGravatar herbelin2007-05-21
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771Gravatar herbelin2007-04-18
* Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,Gravatar herbelin2007-04-14
* Correction bug #1491Gravatar herbelin2007-04-13
* Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantGravatar herbelin2007-04-13
* Modification de la vm:Gravatar notin2007-03-27
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Ajout fonction clenv_conv_leq pour résoudre les pbs de la formeGravatar herbelin2007-02-22
* Utilisation de l'environnement pour l'affichage de certains messages d'erreursGravatar herbelin2007-02-21
* Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESGravatar herbelin2007-02-21
* Add functionality to permit printing terms with references to anonymous varia...Gravatar msozeau2007-02-16
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* Correction d'un bug dans check_and_clear_in_constr + simplification deGravatar notin2007-01-31
* Nouvelle implantation de clear_hypsGravatar notin2007-01-30
* correction d'un bug d'efficacite dans le printerGravatar jforest2007-01-26
* Correction du bug #1315:Gravatar notin2007-01-22
* Correction d'un bug d'unification-pattern dans l'algo d'unificationGravatar herbelin2007-01-22
* Correction pour le rapport de bug #1325 par rétablissement duGravatar herbelin2007-01-22
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
* Rework subtac pattern matching equalities generation.Gravatar msozeau2007-01-02
* Protection contre une source possible de liaison de lambda anonymeGravatar herbelin2006-12-29
* Confusion sur le paramètre à donner à concrete_name lors du commit 9450Gravatar herbelin2006-12-14
* Alignement de la politique de renommage de rename_bound_var (utilisé pourGravatar herbelin2006-12-13
* Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...Gravatar notin2006-12-12
* Correction du bug #1273 (problème avec les paramètres non récursivement un...Gravatar notin2006-12-12
* 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
* Évitement des noms de constructeurs dans les motifs de filtrage de "match"Gravatar herbelin2006-12-09
* correction du bug : VM value extraction error (PR#1290)Gravatar bgregoir2006-11-29
* Code mort découvert par MatthieuGravatar herbelin2006-11-22
* Dépendance inutile en Tacexpr, de proofs, qui se compile en principe aprèsGravatar herbelin2006-11-19
* Raffinement de l'unification de "apply": mémorisation de certainsGravatar herbelin2006-11-19
* Code mort (duplication de code dans reductionops.ml)Gravatar herbelin2006-11-18
* Suppression source de complexité polynomiale introduite par le polymorphismeGravatar herbelin2006-11-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 02:47:27 +0000