aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/abstraction.ml
Commit message (Collapse)AuthorAge
* 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
* 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
* 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
* Nettoyage de GenericGravatar herbelin2000-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
* - abstractionGravatar filliatr1999-08-26
- univers fonctionnels - erreurs de typage maintenant sous forme d'exception, déclarées dans Type_errors git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@24 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 11:55:56 +0000