let eqPref = ref (fun _ -> assert false);;
let set_eqP t = eqPref := fun _ -> t;;
-let default_eqP() =
- let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+let default_eqP() =
+ let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
NCic.Const ref
;;
let set_default_eqP() = eqPref := default_eqP
-let set_reference_of_oxuri f =
- let eqnew = function
- _ ->
- let r = f(UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
- in
- NCic.Const r
- in
- eqPref := eqnew
-;;
-
-
module type NCicContext =
sig
val metasenv : NCic.metasenv
type t = NCic.term
- let eq x y = x = y;;
- (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *)
+ let eq x y =
+ (* CSC: NCicPp.status is the best I can put here *)
+ x = y ||
+ NCicReduction.alpha_eq (new NCicPp.status) C.metasenv C.subst C.context x y;;
let height_of_ref = function
| NReference.Def h -> h
| NReference.Fix(_,_,h) -> h
| _ -> 0
+ external old_hash_param :
+ int -> int -> 'a -> int = "caml_hash_univ_param" (*[@@noalloc]*);;
+
+ let old_hash = old_hash_param 10 100;;
+
let compare_refs (NReference.Ref (u1,r1)) (NReference.Ref (u2,r2)) =
let x = height_of_ref r2 - height_of_ref r1 in
if x = 0 then
- Hashtbl.hash (NUri.string_of_uri u1,r1) -
- Hashtbl.hash (NUri.string_of_uri u2,r2)
+ old_hash (NUri.string_of_uri u1,r1) -
+ old_hash (NUri.string_of_uri u2,r2)
else x
let rec compare x y =
;;
let compare x y =
- if NCicReduction.alpha_eq [] [] [] x y then 0
- (* if x = y then 0 *)
+ if eq x y then 0
else compare x y
;;
| _ -> None
let pp t =
- NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
+ (* CSC: NCicPp.status is the best I can put here *)
+ (new NCicPp.status)#ppterm ~context:C.context
+ ~metasenv:C.metasenv ~subst:C.subst t;;
type input = NCic.term
let saturate t ty =
let sty, _, args =
- NCicMetaSubst.saturate ~delta:0 C.metasenv C.subst C.context
- ty 0
+ (* CSC: NCicPp.status is the best I can put here *)
+ NCicMetaSubst.saturate (new NCicPp.status) ~delta:0 C.metasenv C.subst
+ C.context ty 0
in
let proof =
if args = [] then Terms.Leaf t