aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
AgeCommit message (Collapse)Author
2000-03-21Inlining prod_createherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@336 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@310 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10Reparation bug isevars dans pretypingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@309 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08La partie 'val' de trad_constraints devient un typed_typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@306 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-07Renommage mt_con -> empty_conherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@300 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-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Correction pbs liés aux evarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@265 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-11Intégration initiale du Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@234 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-02modifs pour premiere edition de liensfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 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-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-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-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-24Versions initialesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@136 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 13:49:32 +0000