| _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
| _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
-and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
- ugraph
+and type_of_aux' ?(clean_dummy_dependent_types=true)
+ ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph
=
let rec type_of_aux subst metasenv context t ugraph =
let module C = Cic in
exn ->
enrich localization_tbl s' exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(2) The term " ^
CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
exn ->
enrich localization_tbl term' exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(3) The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst term'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
exn ->
enrich localization_tbl constructor'
~f:(fun _ ->
- lazy ("The term " ^
+ lazy ("(4) The term " ^
CicMetaSubst.ppterm_in_context metasenv subst p'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context metasenv subst actual_type
exn ->
enrich localization_tbl p exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(5) The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst p
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst instance'
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(7) The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(8) The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
coerce_to_something_aux t infty expty subst metasenv context ugraph
with Uncertain _ | RefineFailure _ as exn ->
let f _ =
- lazy ("The term " ^
+ lazy ("(9) The term " ^
CicMetaSubst.ppterm_in_context metasenv subst t context ^
" has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
infty context ^ " but is here used with type " ^
(* eat prods ends here! *)
let t',ty,subst',metasenv',ugraph1 =
- type_of_aux [] metasenv context t ugraph
+ type_of_aux subst metasenv context t ugraph
in
let substituted_t = CicMetaSubst.apply_subst subst' t' in
let substituted_ty = CicMetaSubst.apply_subst subst' ty in
else
substituted_metasenv
in
- (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
+ (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1)
+;;
+
+let type_of metasenv subst context t ug =
+ type_of_aux' metasenv subst context t ug
+;;
+
+let type_of_aux'
+ ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug
+=
+ let t,ty,m,s,ug =
+ type_of_aux' ?clean_dummy_dependent_types ?localization_tbl
+ metasenv [] context t ug
+ in
+ t,ty,m,ug
;;
let undebrujin uri typesno tys t =
RefineFailure _
| Uncertain _ as exn ->
let msg =
- lazy ("The term " ^
+ lazy ("(1) The term " ^
CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
" has type " ^
CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^