aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...herbelin
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...herbelin
2005-12-17Orthographe de 'instantiate'herbelin
2005-12-05changement d'egalite pour le named_context_valgregoire
2005-12-02Changement des named_contextgregoire
2005-11-28parametres inductifsmohring
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 11:02:06 +0000