aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-01-30Adds a possibility to construct a term as if it had been parsed throughbertot
2003-01-30Make sure the parser is compiled in native mode.bertot
2003-01-30Ajoute les directives pour créer aussi bin/coq-interface.optbertot
2003-01-30Auto with zarith essaye Abstract Omega sur un but Falsefilliatr
2003-01-30changement de place du Initial State (maintenant apres l'analyse de la ligne ...filliatr
2003-01-30pas de Xml.vofilliatr
2003-01-30fignolageletouzey
2003-01-30pb d'hier resolu. Recommitletouzey
2003-01-29apres le backtrack precedent, remise de trois points precis et sursletouzey
2003-01-29Ca a tout pété -> Bactrack a la version d'hierletouzey
2003-01-29affichage module et module typeletouzey
2003-01-29affichage module et module typeletouzey
2003-01-29affichage module et module typeletouzey
2003-01-28workaround en attendant traitement reel des modules typesletouzey
2003-01-28amelioration du pretty-print des modulesletouzey
2003-01-28nouvelle gestion des constantes de typeletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-09 16:00:59 +0000