aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-01-28MAJ pour Regdesmettr
2003-01-27Deux p\'tits trucs ;)coq
2003-01-26all tactics should be covered now: remainsbertot
2003-01-25Add translations for many tactics but a dozen are still remainingbertot
2003-01-25Un type "standardisé" pour new_hypherbelin
2003-01-24Inspect does not work for pcoq and there is no simple fix because inspectbertot
2003-01-24on cree toujours le sous-repertoire tactics/filliatr
2003-01-24The data constructed when detecting an error in a list of commands mustbertot
2003-01-24Corrects the way conjunctions, existential quantifications, and arrows arebertot
2003-01-24majfilliatr
2003-01-23Make sure proof by pointing works.bertot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 07:23:44 +0000