aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-04-30MODIFS pour compatibilité aussi 2.99herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@391 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-30Intégration progressiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@390 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-30Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@389 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-30Bug affichage Error et Valueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@388 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@387 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@386 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Renommage bdize -> ast_of_constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@385 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Déplacement du type reference dans Termherbelin
Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@384 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Déplacement du type reference dans Termherbelin
Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@383 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@382 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28portage Omega (code seulement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@381 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28mise sous CVS d'Omegafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@380 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28portage en ocaml / camlp4 3.00filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@379 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28chgt unify_0herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@378 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Changement de représentation du contexte des réf dans rawconstr et patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@377 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-27Retrait fullmind de inductive_summary pour simplicitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@376 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26suppression doublonfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@375 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26Débranchement provisoire equality et tautoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@374 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@373 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@372 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@371 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26renommage ancien pattern en cases_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@370 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26N'importe quel rawconstr maintenant dans le contexte d'une référenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@369 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@368 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@367 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-21discharge des axiomesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@366 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-21Compilation pbs (coqc not finding coqtop, coqc not finding .vo whencourant
building states, coqc wrongly giving option -bindir to coqtop) fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@365 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-21Sign.db_signature is now an abstract typecourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@364 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@363 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-17Prise en compte du renommage des fonctions de Asttermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@361 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-31Portage (pour la forme) de minicoqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@360 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-30erreurs lexicales dans les patterns (manquait des espaces)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@359 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-30Réajout globalize_commandherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@358 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-28Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en ↵herbelin
{pf_,}interp_constr* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@357 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-28Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en ↵herbelin
interp_constr etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@356 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-27Inversion (pas termine)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@355 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-23Amélioration d'un message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@354 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21 - bug make_module_marker (plus de # et de .obj maintenant)filliatr
- portage (partiel) de Zarith - bug discrEverywhere (manquait un "fun gls ->") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@353 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Modification de type_of_case, type_case_branches, etcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@352 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@351 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-30 13:08:47 +0000