aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-01-23reparation des contribs: lors de l'unification, reduire les beta redexesbarras
2003-01-23Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).corbinea
2003-01-23Make proof by pointing work for the new notations of existential quantification.bertot
2003-01-23oubli des add_recursors singleton logiquesletouzey
2003-01-23status de l'extractionletouzey
2003-01-23maj V7.4letouzey
2003-01-22MAJherbelin
2003-01-22Mauvais environnement d'évaluation pour les globauxherbelin
2003-01-22*** empty log message ***barras
2003-01-22modified the unification algorithm to try first order unification beforebarras
2003-01-22Documentation du contenu de REALSdesmettr
2003-01-22ajout de whd_state dans l'interfacebarras
2003-01-22Changements dans REALSdesmettr
2003-01-22removes all references to ctast.ml the Makefile has been updated accordingly.bertot
2003-01-22Modifications dans SeqPropdesmettr
2003-01-22Renommages dans Rtrigo_defdesmettr
2003-01-22I changed the interface to make sure SearchAbout is defined according tobertot
2003-01-22Commentairesdesmettr
2003-01-22Renommages nombreuxdesmettr
2003-01-22Commentairesdesmettr
2003-01-22Correction bug réecriture à la racine pour le sétoide Prop.clrenard
2003-01-22Renommage f_pos -> IVT (Intermediate Value Theoremdesmettr
2003-01-22Suppression d'un Import R_scope probablement oubliedesmettr
2003-01-22Commentairesdesmettr
2003-01-22Renommages dans RListdesmettr
2003-01-22MAJ pour renommage Rcompletdesmettr
2003-01-22Renommages dans Rcompletedesmettr
2003-01-22Renommage Rcomplet.v -> Rcomplete.vdesmettr
2003-01-22Suppression de lemmes superflusdesmettr
2003-01-22Commentairesdesmettr
2003-01-22Renommages dans PartSumdesmettr
2003-01-22Bug 'with Module' corrigecoq
2003-01-22Bug precedenceherbelin
2003-01-22petit bug pp haskellletouzey
2003-01-22majfilliatr
2003-01-22Extraction des modules, enfin !letouzey
2003-01-22id_of_msid en plusletouzey
2003-01-21Adaptation à la nouvelle sémantique plus uniforme de "Match term"herbelin
2003-01-21Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueurherbelin
2003-01-21portabilitedoligez
2003-01-21Renommage dans MVTdesmettr
2003-01-21MAJ dans Exp_propdesmettr
2003-01-21Renommage dans Binomial.vdesmettr
2003-01-21Binome.v -> Binomial.vdesmettr
2003-01-21Binome.v -> Binomial.vdesmettr
2003-01-21MAJ ArithPropdesmettr
2003-01-21Renommage dans AltSeries.vdesmettr
2003-01-21Renommage dans Alembert.vdesmettr
2003-01-21Quelques améliorationsdesmettr
2003-01-21Suppression de INR2 / Conséquence logique de la nouvelle représentation des...desmettr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 06:23:30 +0000