aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2005-11-02Types inductifs parametriquesmohring
2005-11-02Correction bug invert_names (cf bug #1031)herbelin
2005-09-09Léger nettoyage et uniformisation + généralisation du point d'entrée ltac...herbelin
2005-09-06Un vieux bug d'affichage des lieurs (cf bug #1005)herbelin
2005-08-19pas besoin de List.length pour savoir si une liste est videletouzey
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
2005-06-09backtrack sur le typage des instantiations d\'evarsbarras
2005-06-08evar declarees avec mauvais typebarras
2005-06-07pas de filtrages partielsbarras
2005-06-07reparations de quelques petits bugs d\'unification + introduction de la notio...barras
2005-06-06essai de typage des instantiations d\'evarsbarras
2005-06-05eradication de Evarutil.w_Definebarras
2005-06-05assouplissement de real_clean: ne tient pas compte des occcurences flexibles ...barras
2005-05-28unification: evar_define checks the free variables are bound in the evar contextbarras
2005-05-25Added subtac contrib.coq
2005-05-24Added clenv_environments_evars that behaves as clen_environments butsacerdot
2005-05-24WARNING: unification changed (to fix a bug).sacerdot
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-05-20Documentationherbelin
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
2005-04-29Fix bug in prepare_predicate_from_tycon; improved error message when no claus...herbelin
2005-03-15Backtrack sur la substitution combinée avec l'instanciation en réponse à l...herbelin
2005-03-12Backtrack version 1.82 awaiting for better understanding of the consequences ...herbelin
2005-03-11Méthode plus raisonnable pour supprimer l'inefficacité des evars dépendant...herbelin
2005-03-10A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...herbelin
2005-03-10A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...herbelin
2005-03-09bug #931 (continued): no recursion on the evars instantiationherbelin
2005-03-08Fix bug #931: leave dependent evars as such for refineherbelin
2005-03-08Ajout foldherbelin
2005-03-01Code mortherbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse in...herbelin
2005-02-18Ajout it_mkNamedProd_wo_LetInherbelin
2005-02-18Ajout splay_lambdaherbelin
2005-02-12Uniformisation de destApplication en destAppherbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2005-02-02Correction de la précédence des contexts de variables rel, ltac et varherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
2005-01-03HUGE COMMITsacerdot
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...herbelin
2004-12-29ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...herbelin
2004-12-29Bug control_only_guardherbelin
2004-12-09Correction du bug de build_initial_predicate a révèlé un autre bug dans ex...herbelin
2004-12-09Achèvement correction bug do_restrict_hys: ne pas inverser les argumentsherbelin
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
2004-12-08Bugs dans la déclaration du type du terme filtré si non définiherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 00:45:38 +0000