aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
Commit message (Expand)AuthorAge
* amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)Gravatar barras2006-05-05
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Correction bug invert_names (cf bug #1031)Gravatar herbelin2005-11-02
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Uniformisation de destApplication en destAppGravatar herbelin2005-02-12
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...Gravatar herbelin2004-12-29
* UserError in reduce_to_*_refGravatar herbelin2004-11-29
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Vérification de la typability de 'pattern'Gravatar herbelin2004-10-17
* Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient inc...Gravatar herbelin2004-09-08
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Essai de suppression de eta dans simpl (cf bug #779)Gravatar herbelin2004-06-29
* Terminologie plus intuitive: evaluable -> unfoldableGravatar herbelin2004-04-30
* bug #606: mis un message d'erreur plus clairGravatar barras2004-04-07
* 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