aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* MAJGravatar herbelin2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9322 85f007b7-540e-0410-9357-904b9bb8a0f7
* typoGravatar herbelin2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9321 85f007b7-540e-0410-9357-904b9bb8a0f7
* dependencesGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9320 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9319 85f007b7-540e-0410-9357-904b9bb8a0f7
* missing Require LegacyRfieldGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9318 85f007b7-540e-0410-9357-904b9bb8a0f7
* LegacyRfield was opening R_scopeGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit polymorphismeGravatar herbelin2006-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Exports manquants dans ringGravatar barras2006-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
| | | | | | | | | Amélioration affichage des univers. Réparation de petits oublis du premier commit. Essai d'une nouvelle stratégie : si le type d'une constante est mentionné explicitement, la constante est monomorphe dans Type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9314 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ nouvelles théoriesGravatar herbelin2006-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9312 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte dépendance de subtyping en typeops (polymorphisme de defs)Gravatar herbelin2006-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
| | | | | | | | | | (suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9309 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 9256: autres cas incorrects de prise en compte de @ dans les identGravatar herbelin2006-10-28
| | | | | | | pour F4 dans CoqIDE git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9307 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation de "Set Printing Universes", "Print Universes" (anciennementGravatar herbelin2006-10-28
| | | | | | | | "Dump Universes"), "Universe inconsistency", et description brève des univers algébriques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9306 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in experimental merging of functional graphs.Gravatar courtieu2006-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option Set Printing Universes et amélioration affichage des universGravatar herbelin2006-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout fold_rel_declaration et fold_named_declarationGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9303 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de 2 bugs critiques du polymorphisme d'universGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9301 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes on functional graphs merging: put functional results at the endGravatar courtieu2006-10-27
| | | | | | | of args. Still a bug with parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9300 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le caractère ² fait planter make docGravatar notin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Check that sort-polymorphic inductive types is not too laxGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9297 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes on functional graphs merging: removed debug printing.Gravatar courtieu2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9296 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes on functional graphs merging: names of constructors.Gravatar courtieu2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cette dérivation de paradoxe passait en V8.1betaGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restriction au implémenteursGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9293 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout ListTacticsGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout ListTacticsGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement des propriétés générales de BinList dans List et des ↵Gravatar herbelin2006-10-26
| | | | | | | | | tactiques de BinList dans un nouveau ListTactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage d'un message d'erreur losque qu'une relation n'a pas été ↵Gravatar notin2006-10-26
| | | | | | déclarée (Setoid_replace.find_relation_class) (ferme le bug #1259) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9289 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noms de compatibilité déplacés en bloc à la fin du fichierGravatar herbelin2006-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9288 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some fixes in experimental merging of two functional graphs. Gravatar courtieu2006-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9287 85f007b7-540e-0410-9357-904b9bb8a0f7
* added doc for declarative languageGravatar corbinea2006-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Experimental merging of two functional graphs.Gravatar courtieu2006-10-26
| | | | | | | temporary synatx: Mergeschemes (G1 a b c) with (G2 a d e) using G1G2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9285 85f007b7-540e-0410-9357-904b9bb8a0f7
* Facilities to automatically solve obligationsGravatar msozeau2006-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9284 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ crédits, fresh; documentation apply inGravatar herbelin2006-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9283 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9282 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit bug apply inGravatar herbelin2006-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applatissement des noeuds application vide dans le filtrage Ltac (ex:Gravatar herbelin2006-10-25
| | | | | | | None ne filtrait pas None à cause d'un PApp parasite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 9277Gravatar herbelin2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9279 85f007b7-540e-0410-9357-904b9bb8a0f7
* oups, ne chargeait pas les bons fichiersGravatar letouzey2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9278 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'une tentative incorrecte (révision 9266) de clarificationGravatar herbelin2006-10-25
| | | | | | | | du rôle de l'argument (-1) de make_clenv_binding_apply; nouvelle correction qui évite ce codage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9277 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdep -slashGravatar barras2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9276 85f007b7-540e-0410-9357-904b9bb8a0f7
* MénageGravatar notin2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9275 85f007b7-540e-0410-9357-904b9bb8a0f7
* oopsGravatar barras2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9274 85f007b7-540e-0410-9357-904b9bb8a0f7
* conflit de nom (Field_theory) modulo la casseGravatar barras2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9273 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de fresh (suite)Gravatar herbelin2006-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9272 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de la valeur par défaut de with_geoproof (stabilité coqide)Gravatar notin2006-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9271 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 23:47:11 +0000