module S = CicSubstitution
module PT = PrimitiveTactics
-(*
-let module R = CicReduction
-*)
-
-let fail_msg0 = "not a declaration of the current context"
let fail_msg1 = "no applicable simplification"
let error msg = raise (PET.Fail msg)
-let rec declaration name = function
- | [] -> error fail_msg0
- | Some (hyp, Cic.Decl ty) :: _ when hyp = name -> ty
- | _ :: tail -> declaration name tail
-
(* lapply *******************************************************************)
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- ?(substs = []) what =
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) what =
let rec strip_dependent_prods metasenv context ss = function
| Cic.Prod (name, t1, t2) as t ->
if TC.does_not_occur context 0 1 t2 then metasenv, ss, t else
(* fwd **********************************************************************)
-let fwd_simpl_tac ~hyp ~dbd =
+let fwd_simpl_tac ~term ~dbd =
let fwd_simpl_tac status =
let (proof, goal) = status in
let _,metasenv,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let major = declaration hyp context in
+ let major,_ =
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+ in
match MetadataQuery.fwd_simpl ~dbd major with
| [] -> error fail_msg1
| uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])