aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui p...herbelin
2003-11-22Bug introduit avec le 'Simpl f'herbelin
2003-11-21Ajout 'Simpl f'herbelin
2003-11-19Deplacement subst_rawconstr dans Rawtermherbelin
2003-11-18Ajout mis_constructor_nargs_envherbelin
2003-11-09Ajout reduce_to_quantified_refherbelin
2003-11-04Amelioration message d'erreur pour ltacherbelin
2003-10-22Deplacement de iter_constr_with_full_binders dans Termopsherbelin
2003-10-13Export is_section_variableherbelin
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-02Le nom '_' n'est plus valable en v8 pour nommer les variablesherbelin
2003-09-29Oubli du type du terme a filtrer quand pas d'argument dans la traduction de caseherbelin
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom indépen...herbelin
2003-09-13Deplacement de Declare vers Termopsherbelin
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...herbelin
2003-09-12open superfluherbelin
2003-09-10Bug predicat old Caseherbelin
2003-09-09Bug predicat let-tupleherbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
2003-08-31V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclassherbelin
2003-08-12Bug et améliorations diversesherbelin
2003-08-12Bug détypage du fixherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-11Pb quand une meme classe est definie dans 2 fichiersherbelin
2003-06-10Simplification case_infoherbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2003-06-10Factorisation de detype_case pour utilisation par l'afficheur de patternherbelin
2003-06-10Amélioration afficheur de Cases pour les constr_patternherbelin
2003-06-08Tables logarithmiques pour les coercions + nettoyageherbelin
2003-05-22Preservation affichage des ?n en V7herbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-13Rien d'importantherbelin
2003-04-27Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...herbelin
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...letouzey
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-01Correction bug #261 + amélioration nommageherbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2003-03-21*** empty log message ***barras
2003-03-12*** empty log message ***barras
2003-02-02Bug affichage let destructurantherbelin
2003-02-01Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)herbelin
2003-01-31Ajout d'un filtrage d'application partielleherbelin
2003-01-31Unification plus efficace vis à vis du LetInherbelin
2003-01-23reparation des contribs: lors de l'unification, reduire les beta redexesbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:30:28 +0000