aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Plus de whd_castappGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@627 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chasse aux de-cast inutilesGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@626 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage map_constr_with_named_bindersGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@625 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de whd_castappGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de whd_castapp_stackGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@623 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage map_constr_with_named_bindersGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@622 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage de la structure DOPN, DOP2, ... à une structure exprimant ↵Gravatar herbelin2000-10-01
| | | | | | 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
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement 'a reference et binder_kind de Term vers RawtermGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@619 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Elimination de coupures...Gravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait de whd_ise1_metasGravatar herbelin2000-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion ↵Gravatar herbelin2000-09-26
| | | | | | 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
* MAJGravatar herbelin2000-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@614 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour dependancesGravatar filliatr2000-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@613 85f007b7-540e-0410-9357-904b9bb8a0f7
* On laisse les LetIn dans les types des constructeurs et des éliminationsGravatar herbelin2000-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@612 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar herbelin2000-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@611 85f007b7-540e-0410-9357-904b9bb8a0f7
* Messages d'erreursGravatar herbelin2000-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expression anglaiseGravatar herbelin2000-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor correction for Ocamlweb + doc updateGravatar coq2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs parenthèsesGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@607 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression Redinfo Sosub AbstractionGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction de constrGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de fonctions de Reduction vers TacredGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle version de frterm; ajout des contextes dans l'enviornnement de ↵Gravatar herbelin2000-09-14
| | | | | | réduction de Closure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégré à TacredGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rendus obsolètes par le LetInGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction de constrGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@599 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vers la paramétrisation des fonctions de Reduction et vers la fusion deGravatar herbelin2000-09-12
| | | | | | | Closure.stack avec une nouvelle abstraction des 'stacks' de Reduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@596 85f007b7-540e-0410-9357-904b9bb8a0f7
* nettoyageGravatar herbelin2000-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour make docGravatar herbelin2000-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de AbstGravatar herbelin2000-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
| | | | | | | Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@592 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
| | | | | | | Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
| | | | | | | Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. ↵Gravatar herbelin2000-09-10
| | | | | | Abstraction de constr. LetIn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print PathGravatar herbelin2000-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@588 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration à TermGravatar herbelin2000-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@587 85f007b7-540e-0410-9357-904b9bb8a0f7
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2000-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@585 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout erreur unexpected typeGravatar herbelin2000-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@584 85f007b7-540e-0410-9357-904b9bb8a0f7
* kernel/type_errors.mlGravatar herbelin2000-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@583 85f007b7-540e-0410-9357-904b9bb8a0f7
* cosmétiqueGravatar herbelin2000-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@582 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nametab.init - bug correctedGravatar coq2000-08-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans le filtrage des paires, nettoyageGravatar herbelin2000-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pattern matching de sous-termesGravatar delahaye2000-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pattern matching de sous-termes + exceptions dans le lexerGravatar delahaye2000-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@578 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-20 17:05:33 +0000