aboutsummaryrefslogtreecommitdiff
path: root/pretyping/detyping.ml
AgeCommit message (Collapse)Author
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-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Correction pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Suppression de Abstherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
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
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Nettoyage de Genericherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans ↵herbelin
les instances de références git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@478 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 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-02Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@394 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Changement de représentation du contexte des réf dans rawconstr et patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@377 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26N'importe quel rawconstr maintenant dans le contexte d'une référenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@369 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Prise en compte nouveau case_infoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@343 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration ↵herbelin
du let-in git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@281 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Traduction constr->rawconstr (avant dans Termastherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@271 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:50:33 +0000