+ aux metasenv subst n context (CicSubstitution.lift_meta l t')
+ ugraph
+ with CicMetaSubst.SubstNotFound _ ->
+ let (subst, metasenv, context, local_context,ugraph1) =
+ List.fold_left
+ (fun (subst, metasenv, context, local_context,ugraph) t ->
+ match t with
+ | None ->
+ (subst, metasenv, context, None::local_context, ugraph)
+--------- *)
+ subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
+ | C.Meta (i,l) ->
+ (* andrea: in general, beta_expand can create badly typed
+ terms. This happens quite seldom in practice, UNLESS we
+ iterate on the local context. For this reason, we renounce
+ to iterate and just lift *)
+ let l =
+ List.map
+ (function
+ Some t -> Some (CicSubstitution.lift 1 t)
+ | None -> None) l in
+ subst, metasenv, C.Meta (i,l), ugraph
+ (*
+ let (subst, metasenv, context, local_context) =
+ List.fold_right
+ (fun t (subst, metasenv, context, local_context) ->
+ match t with
+ | None -> (subst, metasenv, context, None :: local_context)
+
+ | Some t ->
+ let (subst, metasenv, t, ugraph1) =
+ aux metasenv subst n context t ugraph
+ in
+(* THIS WAS BEFORE ----
+ (subst, metasenv, context,
+ (Some t)::local_context,ugraph1))
+ (subst, metasenv, context, [],ugraph) l
+ in
+ (subst, metasenv,(C.Meta (i, local_context)),ugraph1))
+-------- *)
+ (subst, metasenv, context, Some t :: local_context))
+ l (subst, metasenv, context, [])
+ in
+ prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context))));
+ (subst, metasenv, C.Meta (i, local_context)) *)