aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
...
* Bug splay_prod_assumGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@668 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pr_uniGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@666 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en conformité nouveau Simpl pour FixGravatar herbelin2000-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Touche finale à la réduction du let in dans conv et closureGravatar herbelin2000-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@647 85f007b7-540e-0410-9357-904b9bb8a0f7
* Elimination des coupures sur le type constantGravatar herbelin2000-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@646 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@638 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage AppL en AppGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
* whd_castapp_stack va de Term dans ReductionGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@632 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de ensure_applGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@631 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug message erreurGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@630 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code comateuxGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@628 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
* 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
* 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
* 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
* Abstraction de constrGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 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
* 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
* 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@591 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
* 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
* 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
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
* retablissement minicoq (pour Jacek)Gravatar filliatr2000-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@565 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques (*i*) pour ne pas casser oczmlwebGravatar coq2000-07-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@557 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@549 85f007b7-540e-0410-9357-904b9bb8a0f7
* Précalcul de la forme canonique des constructeurs et arités pour traiter ↵Gravatar herbelin2000-07-01
| | | | | | les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@548 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout fonctions sur les aritésGravatar herbelin2000-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@547 85f007b7-540e-0410-9357-904b9bb8a0f7
* Précalcul de la forme canonique des constructeurs et arités pour traiter ↵Gravatar herbelin2000-07-01
| | | | | | les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@542 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relative prend sigma en plus pour la normalisation du message d'erreurGravatar herbelin2000-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@530 85f007b7-540e-0410-9357-904b9bb8a0f7
* BroutillesGravatar herbelin2000-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@529 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout make_typed_lazyGravatar herbelin2000-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@528 85f007b7-540e-0410-9357-904b9bb8a0f7
* Normalisation des Evar avant génération des erreursGravatar herbelin2000-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@527 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> ↵Gravatar filliatr2000-06-21
| | | | | | .vo plus petits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@514 85f007b7-540e-0410-9357-904b9bb8a0f7
* DocGravatar herbelin2000-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@501 85f007b7-540e-0410-9357-904b9bb8a0f7
* DiversGravatar herbelin2000-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constrGravatar herbelin2000-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@497 85f007b7-540e-0410-9357-904b9bb8a0f7