aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-10-04Ajout LetIn dans prim_extractorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@649 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Nouveau bug dans la réduction de Fix par red_elim_constherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@648 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Touche finale à la réduction du let in dans conv et closureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@647 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Elimination des coupures sur le type constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@646 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@645 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Renommage tactique Let en LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@644 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Ajout castedopenconstrargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@643 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Ajout de globpr dans tacprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@642 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@641 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Ajout castedopenconstrarg; Renommage tactique Let en LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@640 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Reorganisation des interp_constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@639 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Rebranchement de la tactique Letherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@638 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03L'argument de Refine est un terme ouvertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@637 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03mise en pageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@636 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en Appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@635 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en Appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en App; Suppression castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@633 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01whd_castapp_stack va de Term dans Reductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@632 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Suppression de ensure_applherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@631 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Bug message erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@630 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@629 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Code comateuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@628 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Plus de whd_castappherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@627 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Chasse aux de-cast inutilesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@626 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01renommage map_constr_with_named_bindersherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@625 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Plus de whd_castappherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@624 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Plus de whd_castapp_stackherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@623 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01renommage map_constr_with_named_bindersherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@622 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Passage de la structure DOPN, DOP2, ... à une structure exprimant ↵herbelin
directement les constructions; disparition du type oper mais nouveau type global_reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@621 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Déplacement 'a reference et binder_kind de Term vers Rawtermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@619 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@618 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Elimination de coupures...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@617 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-26Retrait de whd_ise1_metasherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@616 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-26Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion ↵herbelin
de 'OpenConstr' constitué d'un terme avec Métas et d'une liste de types pour les métas git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@615 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@614 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-18mise a jour dependancesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@613 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-15On laisse les LetIn dans les types des constructeurs et des éliminationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@612 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-15Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@611 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-15Messages d'erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@610 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-15Expression anglaiseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@609 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Minor correction for Ocamlweb + doc updatecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@608 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Bugs parenthèsesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@607 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@606 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Suppression Redinfo Sosub Abstractionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@605 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Abstraction de constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Déplacement de fonctions de Reduction vers Tacredherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@603 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Nouvelle version de frterm; ajout des contextes dans l'enviornnement de ↵herbelin
réduction de Closure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@602 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Intégré à Tacredherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@601 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Rendus obsolètes par le LetInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@600 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 01:36:34 +0000