aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Added a clause for VernacDefineModule, but with an error as result.Gravatar bertot2003-02-03
* majGravatar filliatr2003-02-03
* maj status de l'extraction des modulesGravatar letouzey2003-02-03
* hack horrible pour renommage dans Modules Types et FuncteursGravatar letouzey2003-02-03
* encore un long_knGravatar letouzey2003-02-03
* contrib/extraction/table utilise printerGravatar letouzey2003-02-02
* plus d'environment fixe cur_env mais un environment evolutifGravatar letouzey2003-02-02
* Bug affichage let destructurantGravatar herbelin2003-02-02
* Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)Gravatar herbelin2003-02-01
* Ajout d'un filtrage d'application partielleGravatar herbelin2003-01-31
* MAJGravatar herbelin2003-01-31
* MAJGravatar herbelin2003-01-31
* MAJGravatar herbelin2003-01-31
* Unification plus efficace vis à vis du LetInGravatar herbelin2003-01-31
* preparation pkg deb for 7.4Gravatar courant2003-01-31
* *** empty log message ***Gravatar courant2003-01-31
* MAJ syntaxe modules + nouveau fichier mod_decl qui explique toutGravatar coq2003-01-31
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
* majGravatar filliatr2003-01-31
* Pb de parenthèse dans "Check (S (plus O O))"Gravatar herbelin2003-01-30
* Adds a possibility to construct a term as if it had been parsed throughGravatar bertot2003-01-30
* Make sure the parser is compiled in native mode.Gravatar bertot2003-01-30
* Ajoute les directives pour créer aussi bin/coq-interface.optGravatar bertot2003-01-30
* Auto with zarith essaye Abstract Omega sur un but FalseGravatar filliatr2003-01-30
* changement de place du Initial State (maintenant apres l'analyse de la ligne ...Gravatar filliatr2003-01-30
* pas de Xml.voGravatar filliatr2003-01-30
* fignolageGravatar letouzey2003-01-30
* pb d'hier resolu. RecommitGravatar letouzey2003-01-30
* apres le backtrack precedent, remise de trois points precis et sursGravatar letouzey2003-01-29
* Ca a tout pété -> Bactrack a la version d'hierGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* workaround en attendant traitement reel des modules typesGravatar letouzey2003-01-28
* amelioration du pretty-print des modulesGravatar letouzey2003-01-28
* nouvelle gestion des constantes de typeGravatar letouzey2003-01-28
* MAJ pour RegGravatar desmettr2003-01-28
* Deux p\'tits trucs ;)Gravatar coq2003-01-27
* all tactics should be covered now: remainsGravatar bertot2003-01-26
* Add translations for many tactics but a dozen are still remainingGravatar bertot2003-01-25
* Un type "standardisé" pour new_hypGravatar herbelin2003-01-25
* Inspect does not work for pcoq and there is no simple fix because inspectGravatar bertot2003-01-24
* on cree toujours le sous-repertoire tactics/Gravatar filliatr2003-01-24
* The data constructed when detecting an error in a list of commands mustGravatar bertot2003-01-24
* Corrects the way conjunctions, existential quantifications, and arrows areGravatar bertot2003-01-24
* majGravatar filliatr2003-01-24
* Make sure proof by pointing works.Gravatar bertot2003-01-23
* reparation des contribs: lors de l'unification, reduire les beta redexesGravatar barras2003-01-23
* Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).Gravatar corbinea2003-01-23
* Make proof by pointing work for the new notations of existential quantification.Gravatar bertot2003-01-23