aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
Commit message (Expand)AuthorAge
* Bug numerotation des occurrences pour 'simpl id at n' (suite)Gravatar herbelin2004-02-13
* Bug numerotation des occurrences pour 'simpl id at n' (2 protections maintena...Gravatar herbelin2004-02-13
* Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramĂ...Gravatar herbelin2004-01-27
* Affichage opaqueGravatar herbelin2003-12-23
* Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'Gravatar herbelin2003-12-17
* Bug introduit avec le 'Simpl f'Gravatar herbelin2003-11-22
* Ajout 'Simpl f'Gravatar herbelin2003-11-21
* Ajout reduce_to_quantified_refGravatar herbelin2003-11-09
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Renommage CMeta en CPatVar qui sert Ă  saisir les PMeta de PatternGravatar herbelin2003-05-19
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* *** empty log message ***Gravatar barras2003-03-12
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* retour en arriere concernant la recherche d'occurence modulo expansion des le...Gravatar barras2002-10-09
* correction de bugs:Gravatar barras2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Mise au point de declare_red_exprGravatar herbelin2002-05-30
* Finalement un seul constr pour l'instant dans ExtraRedExprGravatar herbelin2002-05-30
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* Non dépliage des Fix non réductibles dans HnfGravatar herbelin2001-12-20
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* TransparentGravatar barras2001-09-20
* Nettoyage reduce_to_ind et one_step_reduceGravatar herbelin2001-09-09
* Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)Gravatar herbelin2001-09-07
* Bug SimplGravatar herbelin2001-07-24
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* traitement du let dans red_product (tactique Red)Gravatar barras2001-06-29
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Changement de la structure des points fixesGravatar barras2001-05-03
* entetesGravatar filliatr2001-03-15
* DĂ©placement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Reparation reduce_to_mindGravatar mohring2001-02-01
* - coqc : option -imageGravatar filliatr2001-02-01
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* DĂ©placement du type stack de Reduction vers Closure et utilisation pour accĂ...Gravatar herbelin2000-12-26
* RĂ©tablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...Gravatar herbelin2000-12-20
* Debut de nettoyage de SimplGravatar mohring2000-12-18
* PrinterGravatar mohring2000-12-15
* LetIn dans SimplGravatar mohring2000-12-14
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* Debut de reparation de simplGravatar mohring2000-12-11
* La table de pré-évaluation des constantes ne doit pas persister au dischargeGravatar herbelin2000-11-27
* Prise en compte des let-in dans les fonctions de réduction pour les tactiquesGravatar herbelin2000-11-27
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 04:56:45 +0000