diff options
| author | herbelin | 1999-12-01 23:13:01 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-01 23:13:01 +0000 |
| commit | f99150300603ce0d87db716efc52fa88967d4460 (patch) | |
| tree | 4a85be13031030ac01659359b032411bfd63a73b /pretyping/pretyping.ml | |
| parent | 3a49dbf016e1ebf8f8d12ed43fde14c5619ca55e (diff) | |
Intégration du Termast et du Retyping de HH, et modifications connexes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 500e6bfe74..96e97a040d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -328,7 +328,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) check_cofix env !isevars cofix; make_judge cofix lara.(i)) -| RSort (loc,RProp c) -> make_judge_of_prop_contents c +| RSort (loc,RProp c) -> judge_of_prop_contents c | RSort (loc,RType) -> { uj_val = dummy_sort; uj_type = dummy_sort; uj_kind = dummy_sort } @@ -424,7 +424,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) uj_kind = snd (splay_prod env !isevars evalPt)} | RCases (loc,prinfo,po,tml,eqns) -> - Multcase.compile_multcase + Cases.compile_multcase ((fun vtyc env -> pretype vtyc env isevars),isevars) vtcon env (po,tml,eqns) @@ -473,6 +473,11 @@ let j_apply f env sigma j = variables du sigma original. il faudrait que la fonction de typage retourne aussi le nouveau sigma... *) +let ise_resolve_casted sigma env typ c = + let isevars = ref sigma in + let j = unsafe_fmachine (mk_tycon typ) false isevars [] env c in + (j_apply (fun _ -> process_evars true) env !isevars j).uj_val + let ise_resolve fail_evar sigma metamap env c = let isevars = ref sigma in let j = unsafe_fmachine mt_tycon false isevars metamap env c in |