aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-06-29Renommage mk_unsafe_judgment en get_judgment_ofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@525 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Extension de l'inférence des types des lambdas du prédicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@524 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Achèvement abstraction du mécanisme (optionnel) de castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@523 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Rienherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@522 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Essai de simplification compte tenu de l'info de locationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@521 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-28Modifs de presentation.delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@520 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-28Rattrapage d'un Not_found pour les VAR's.delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@519 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-27Retrait du 'strip' en cas de profilingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@518 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21$BINDER -> BINDERfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@517 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21 - $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)filliatr
- suite portage Ring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@516 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21Require Plus ajoutefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@515 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> ↵filliatr
.vo plus petits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@514 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21portage EAuto et Ringfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@513 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21Ringfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@512 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21theories/Realsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@511 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21theories/Relationsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@510 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21theories/Setsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@509 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21theories/Listsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@508 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-15Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@507 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-12Auto with zarith provisoirement remplace par un Omegafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@506 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-12mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@505 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-12dependance des CONTRIBVO envers initial.coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@504 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-09Bugsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@503 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-09Amelioration messages erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@502 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-09Docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@501 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-03Diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@500 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-03Retrait des lam_and_pop and co (2ème - bug)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@499 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-03Retrait des lam_and_pop and coherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@498 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-03Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@497 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Retrait de decomp_prod non conforme à sa specherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@496 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Retrait de certains castsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@495 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02bugs infrence des arguments manquants dans le prdicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@494 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02bugs et simplification (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@493 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@492 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@491 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Bug DLAM dans strongherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@490 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Bugs/Messages d'erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@489 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@488 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Bugs et simplifications coercionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@487 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02':>' est devenu un seul tokenherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@486 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@485 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Afficahge des locationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@483 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Nettoyage de Genericherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@481 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@480 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Amélioration capture des erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@479 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans ↵herbelin
les instances de références git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@478 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-25Déplacement de save_thm and co de PFedit vers Commandherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@477 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-25Bug existential_value au lieu de existential_type + divers sur existentialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@476 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 03:07:43 +0000