(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
+let reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
+
+
let eqP () =
let r =
- OCic2NCic.reference_of_oxuri
+ !reference_of_oxuri
(UriManager.uri_of_string
"cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
in
let eq_ind () =
let r =
- OCic2NCic.reference_of_oxuri
+ !reference_of_oxuri
(UriManager.uri_of_string
"cic:/matita/logic/equality/eq_ind.con")
in
let eq_ind_r () =
let r =
- OCic2NCic.reference_of_oxuri
+ !reference_of_oxuri
(UriManager.uri_of_string
"cic:/matita/logic/equality/eq_elim_r.con")
in
let eq_refl () =
let r =
- OCic2NCic.reference_of_oxuri
+ !reference_of_oxuri
(UriManager.uri_of_string
"cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
in
match t with
| Terms.Leaf _
| Terms.Var _ ->
-(* prerr_endline ("term: " ^ ppfot ft); *)
+ let module Pp =
+ Pp.Pp(NCicBlob.NCicBlob(
+ struct
+ let metasenv = [] let subst = [] let context = []
+ end))
+ in
+ prerr_endline ("term: " ^ Pp.pp_foterm ft);
prerr_endline ("path: " ^ String.concat ","
(List.map string_of_int p1));
+ prerr_endline ("leading to: " ^ Pp.pp_foterm t);
assert false
| Terms.Node l ->
let l =
t vl
in
let get_literal id =
- let (_, lit, vl, proof),_ = Terms.M.find id bag in
+ let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
let lit =match lit with
| Terms.Predicate t -> assert false
| Terms.Equation (l,r,ty,_) ->
if ongoal then id1,id,get_literal id1
else id,id1,(lit,vl,proof)
in
- let vl = if ongoal then Subst.filter subst vl else vl in
+ let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
let proof_of_id id =
let vars = List.rev (vars_of id seen) in
let args = List.map (Subst.apply_subst subst) vars in