let position to_skip n (shift, lc) =
match lc with
- | NCic.Irl _ when to_skip > 0 -> assert false (* unclear to me *)
- | NCic.Irl len when n <= shift || n > shift + len ->
+ | NCic.Irl len when n <= shift + to_skip || n > shift + len ->
raise (NotFound `NotInTheList)
| NCic.Irl _ -> n - shift
| NCic.Ctx tl ->
;;
let rec is_flexible status context ~subst = function
- | NCic.Meta (i,_) ->
+ | NCic.Meta (i,lc) ->
+ (try
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ let t = NCicSubstitution.subst_meta status lc t in
+ is_flexible status context ~subst t
+ with NCicUtils.Subst_not_found _ -> true)
+ | NCic.Appl (NCic.Meta (i,lc) :: args)->
(try
- let _,_,t,_ = List.assoc i subst in
- is_flexible status context ~subst t
- with Not_found -> true)
- | NCic.Appl (NCic.Meta (i,_) :: args)->
- (try
- let _,_,t,_ = List.assoc i subst in
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ let t = NCicSubstitution.subst_meta status lc t in
is_flexible status context ~subst
(NCicReduction.head_beta_reduce status ~delta:max_int
(NCic.Appl (t :: args)))
- with Not_found -> true)
+ with NCicUtils.Subst_not_found _ -> true)
(* this is a cheap whd, it only performs zeta-reduction.
*
* it works when the **omissis** disambiguation algorithm
NCicUtils.Meta_not_found _ ->
(* Fake metavariable used in NTacStatus and NCicRefiner :-( *)
assert (n = -1); res
+ | NCicTypeChecker.TypeCheckerFailure msg ->
+ HLog.error "----------- Problem with Dependent Types ----------";
+ HLog.error (Lazy.force msg) ;
+ HLog.error "---------------------------------------------------";
+ raise (NotFound `NotWellTyped)
| TypeNotGood
| NCicTypeChecker.AssertFailure _
| NCicReduction.AssertFailure _