-let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
- let module I = Inference in
- let curi,metasenv,pbo,pty = proof in
- let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
- let eq_indexes, equalities, maxm = I.find_equalities context proof in
- let lib_eq_uris, library_equalities, maxm =
- I.find_library_equalities dbd context (proof, goal) (maxm+2) in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let library_equalities = List.map snd library_equalities in
- let goalterm = Cic.Meta (metano,irl) in
- let initgoal = Inference.BasicProof goalterm, [], goalterm in
- let equalities = equalities @ library_equalities in
- let table =
- List.fold_left
- (fun tbl eq -> index tbl eq)
- empty equalities
- in
- let _,(newproof, newty, newmetasenv) = demodulation_goal
- maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal
- in
- let proofterm = Inference.build_proof_term newproof in
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm)
- initialstatus
-
-let demodulate_tac ~dbd ~pattern =
- ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)