-let find_in_context name context =
- let rec aux acc = function
- | [] -> raise Not_found
- | (hd,_) :: tl when hd = name -> acc
- | _ :: tl -> aux (acc + 1) tl
- in
- aux 1 context
-;;
-
-let clear name status goal =
- let goalty = get_goalty status goal in
- let j =
- try find_in_context name (ctx_of goalty)
- with Not_found -> fail (lazy ("hypothesis '" ^ name ^ "' not found")) in
- let n,h,metasenv,subst,o = status.pstatus in
- let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal [j] in
- { status with pstatus = n,h,metasenv,subst,o }
-;;
-
-let clear_tac name = distribute_tac (clear name);;
-