aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Correction message d'erreur ltac et adoption du modèle de message de TacinterpGravatar herbelin2006-03-04
* Correctif pour bug #1089 (cannot define an isevar twice)Gravatar herbelin2006-03-02
* Localisation des erreurs de sorte du prétypageGravatar herbelin2006-02-08
* oubli de code de debuggingGravatar herbelin2006-02-07
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
* Mise en conformité de l'ordre des occurrences de pattern avec l'affichageGravatar herbelin2006-02-07
* Optimisation filtrage sans lieurs (utile pour Ltac)Gravatar herbelin2006-02-01
* Suppression fonctions d'interprétation du vieux CaseGravatar herbelin2006-01-30
* Gestion des erreurs pour nombre incorrect d'argument des constructeurs (et deGravatar herbelin2006-01-30
* - Prise en compte de la clause 'in I' pour coercer le type du terme à filtrerGravatar herbelin2006-01-30
* Fonctions retournant les arits des constructeurs et inductifs (suite)Gravatar herbelin2006-01-30
* Fonctions retournant les arits des constructeurs et inductifsGravatar herbelin2006-01-30
* - Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;Gravatar herbelin2006-01-30
* DocumentationGravatar herbelin2006-01-29
* Version préliminaire d'inversion de la compilation du filtrageGravatar herbelin2006-01-16
* Standardisation du nom de subst_raw en subst_rawconstrGravatar herbelin2006-01-11
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression résidus code v7 et traducteurGravatar herbelin2006-01-11
* Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...Gravatar herbelin2006-01-10
* Fonctions de conversion rawconstr <-> cases_patternGravatar herbelin2006-01-08
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Orthographe de 'instantiate'Gravatar herbelin2005-12-17
* changement d'egalite pour le named_context_valGravatar gregoire2005-12-05
* Changement des named_contextGravatar gregoire2005-12-02
* parametres inductifsGravatar mohring2005-11-28
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Correction bug invert_names (cf bug #1031)Gravatar herbelin2005-11-02
* Léger nettoyage et uniformisation + généralisation du point d'entrée ltac...Gravatar herbelin2005-09-09
* Un vieux bug d'affichage des lieurs (cf bug #1005)Gravatar herbelin2005-09-06
* pas besoin de List.length pour savoir si une liste est videGravatar letouzey2005-08-19
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* backtrack sur le typage des instantiations d\'evarsGravatar barras2005-06-09
* evar declarees avec mauvais typeGravatar barras2005-06-08
* pas de filtrages partielsGravatar barras2005-06-07
* 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
* Added subtac contrib.Gravatar coq2005-05-25
* Added clenv_environments_evars that behaves as clen_environments butGravatar sacerdot2005-05-24
* WARNING: unification changed (to fix a bug).Gravatar sacerdot2005-05-24
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* DocumentationGravatar herbelin2005-05-20
* A wish by Bas Spitters granted: a little more of unification up toGravatar sacerdot2005-05-19
* Fix bug in prepare_predicate_from_tycon; improved error message when no claus...Gravatar herbelin2005-04-29