aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-05-22Retour comportement de la version précédenteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@456 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18bug (typage avec meta)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@455 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18parethèses de tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@454 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18bugsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@453 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18suppression ligne etrangeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@452 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18export get_current_contextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@451 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Ajout warning si variable existant par ailleursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@450 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18ciseauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@449 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18MAJ modifs Inductiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@448 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@447 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Ajouts des causes d'erreur de Indrecherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@446 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@445 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Restructuration des outils pour les inductifs.herbelin
- Les déclarations (mutual_inductive_packet et mutual_inductive_body), utilisisées dans Environ vont dans Constant - Instantiations du context local (mind_specif), instantiation des paramètres globaux (inductive_family) et instantiation complète (inductive_type, nouveau nom de inductive_summary) vont dans Inductive qui est déplacé après réduction - Certaines fonctions de Typeops et celle traitant des inductifs dans Reduction et Instantiate sont regroupées dans Inductive" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@444 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Ajout lift_contextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@443 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@442 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Centralisation prod_name and co dans Environ; mkLambda_string dans Termherbelin
Effets de bords suite à la restructuration des inductives (cf Inductive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@441 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Adaptation pour nouveaux inductifs (cf Inductive)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@440 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@439 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Restructuration des outils pour les inductifs.herbelin
- Les déclarations (mutual_inductive_packet et mutual_inductive_body), utilisisées dans Environ vont dans Constant - Instantiations du context local (mind_specif), instantiation des paramètres globaux (inductive_family) et instantiation complète (inductive_type, nouveau nom de inductive_summary) vont dans Inductive qui est déplacé après réduction - Certaines fonctions de Typeops et celle traitant des inductifs dans Reduction sont regroupées dans Inductive git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@438 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Centralisation prod_name and co dans Environ; mkLambda_string dans Termherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@437 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@436 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-16Ajout mis_typepathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@435 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@434 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-16RIENherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@433 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-16Rienherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@432 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-08contrib linkees en natiffilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@431 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-08un Declare ML Module inutilefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@430 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05ajout d'Inversionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@429 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@428 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@427 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05Ajout d'un strong 'light'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@426 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05ajout interp_sortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@425 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05Réorganisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@424 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05Achèvement nettoyage Pfedit; ajout intros_replacingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@423 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05Intégration de leminvherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@422 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05Achèvement nettoyage Pfeditherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@421 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05Ajoute option -byteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@420 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-04MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@419 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-04Vernacinterp passe après Commandherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@418 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-04les erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@417 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-04Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@416 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-04Nettoyage de l'interface de Pfeditherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@415 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03nettoyage (quelques oublis dans make clean)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@414 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03compilation bytecode / native :filliatr
- script de configuration - Makefile - simplification de coqmktop - option -opt de coqc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@413 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Retrait de PrintConstr vers top_printersdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@412 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Completion d'un match non exhaustifdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@411 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Ajout de PrintConstr pour debugdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@410 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Reparation du bug d'interpretation d'Abstractdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@409 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03diverses modifs pour ocamlwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@407 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 17:21:59 +0000