;;
let look_for_coercion src tgt =
+ None
+ (*
if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
(tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con"))
then
(CicPp.ppterm tgt));
None
end
+ *)
;;
canonical_context l ugraph
in
(* trust or check ??? *)
- C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
+ C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
subst', metasenv', ugraph1
(* type_of_aux subst metasenv
- context (CicSubstitution.lift_meta l term) *)
+ context (CicSubstitution.subst_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let l',subst',metasenv', ugraph1 =
check_metasenv_consistency n subst metasenv context
canonical_context l ugraph
in
- C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
+ C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
subst', metasenv',ugraph1)
| C.Sort (C.Type tno) ->
let tno' = CicUniv.fresh() in
function
[] -> []
| (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
| (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
| (Some (n,C.Def (t,Some ty)))::tl ->
(Some (n,
- C.Def ((S.lift_meta l (S.lift i t)),
- Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+ C.Def ((S.subst_meta l (S.lift i t)),
+ Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
in
aux 1 canonical_context
in
(cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
;;
+let type_of_aux' metasenv context term ugraph =
+ try
+ type_of_aux' metasenv context term ugraph
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+
+
(* DEBUGGING ONLY
let type_of_aux' metasenv context term =
try