aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-03-21Modification de type_of_case, type_case_branches, etc;nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@350 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Ajout {prod,lambda}_nameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@349 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Retour sur les anciens nomsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@348 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@347 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21MAJ ocaml 2.99herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@346 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@345 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance ↵herbelin
utilisé par clenv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@344 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Prise en compte nouveau case_infoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@343 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Déplacement des fonctions spécifiques du discharge qui était dans ↵herbelin
Generic; prise en compte du sp dans MutCase git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@342 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Déplacement fonction du discharge dans Dischargeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@341 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Remplacement plain_instance en instance qui n'a plus besoin de envherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@340 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Plus besoin de env dans reduce_mind_case; make_arity et make_constructor ↵herbelin
sortent de inductive_summary et se renomment en get_arity et get_constructors git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@339 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Plus besoin de env dans reduce_mind_caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@338 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Prise en compte nouveau case_info et nouvel Reduction.instanceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@337 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Inlining prod_createherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@336 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Prise en compte nouveau case_info dans type_caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@335 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Prise en compte nouveau case_infoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@334 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Ajout des fonctions de formation du 'case_info'; Suppression de make_arity ↵herbelin
et make_constructor de inductive_summary git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@333 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Extension du case_info : ajout du nombre de vrais args de chaque constr pour ↵herbelin
la iota-réduction et d'autres informations pour l'affichage dans l'argument du cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@332 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-20Tautofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@331 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-20Affichage des <> pour débugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@330 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-20Bug ordre des inductifs mutuelsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@329 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-20Affichage des anonymes si lambdaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@328 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18ZArithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@327 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18Zarithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@326 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18on ne compile pas Div.v (Realizer)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@325 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18g_natsyntax.mlfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@324 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18bug discharge (work_alist contenanti plein de fois les memes choses)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@323 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-17Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@322 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-17Un cast inutileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@321 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16Syntactic Definition n'etaient pas correctemenet importeesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@320 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16theories/Boolfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@319 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16mise sous CVSfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@318 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16mauvais parenthesage dans hd_name (patterns imbriques)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@317 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16Utilisation de l'env pour nommer les Relherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@316 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16Qqes bugs (evars dans le predicat; tag des cas défauts)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@315 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10Eqdep_dec doit etre compilefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@314 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10t -> $t dans regle grammaire EXfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@313 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10compilation theories/Arithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@312 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10mise sous CVS du repertoire theories/Arithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@310 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10Reparation bug isevars dans pretypingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@309 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08Ajout theories/Logic/*.voherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@308 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@307 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08La partie 'val' de trad_constraints devient un typed_typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@306 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08Réparation du cast oublié lors d'une définition castéeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@305 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08MAJ nouveau try_mutind_ofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@304 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08Ajout du test d'égalité des vecteurs dans convert_forall2.herbelin
Raffinement de try_mutind_of. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@303 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08Un nouveau moteur pour Cases (phase 1)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@302 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08Peaufinement nouveaux types inductive_summary et constructor_summary en vueherbelin
de remplacer mispec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@301 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 12:21:11 +0000