aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-06-29Ajout list_fold_right_and_leftherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@535 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@534 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Utilisation du STRIP de config/Makefile pour gérer le mode profileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@533 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_ofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@532 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Séparation des contraintes de type et de valeur dans pretypingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@531 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Relative prend sigma en plus pour la normalisation du message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@530 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Broutillesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@529 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Ajout make_typed_lazyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@528 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Normalisation des Evar avant génération des erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@527 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Bricolesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@526 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 10:47:20 +0000