aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
1999-12-01déplacé dans kernelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@179 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01mise au point Declare et avancee dans Asttermfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@175 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01mise a jour Coercionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@172 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01 - environment -> safe_environmentfilliatr
- unsafe_env -> env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@168 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01 - Typing -> Safe_typingfilliatr
- proofs/Typing_ev -> pretyping/Typing - env -> sign - fonctions var_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-30inductive_key et constructor_keyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@166 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-30ocamlwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@165 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-30ocamlwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@163 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-29portage modules Evarconv et Evarutilfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@161 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-29portage Astterm (partiellement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-27fin Recordops, et debut Evarutilfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@158 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26Pas encore pretherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@157 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26Modification pour faire compiler pretyping.ml qui maintenant compileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@156 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26Maintenant compilableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@155 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26Version initialeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@153 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26module Classops; ajout de fonctions dans Declare en consequencefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@152 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-25Des progres dans l'integrationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@140 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-24MAJ pour fusion avec pretypingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-24Versions initialesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@136 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-24Deplace dans parsingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@135 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-24Version initialeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@134 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-19Version préliminaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@124 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-18pas de grosse banniere; pas de double point-virgukefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@120 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-24Traducteur ast -> rawtermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@118 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-24Type ML des termes non prétypésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@117 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-13organisation de trad (entre parsing/ et pretyping/)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@102 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-16 03:21:31 +0000