let set_eqP t = eqPref := fun _ -> t;;
let default_eqP() =
- let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/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
type t = NCic.term
- let eq x y = NCicReduction.alpha_eq C.metasenv C.subst C.context x y;;
+ let eq x y = x = y;;
+ (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *)
let rec compare x y =
match x,y with
| ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
| NCic.Appl _, NCic.Meta _ -> ~-1
| NCic.Meta _, NCic.Appl _ -> 1
- | _ -> assert false
+ | _ -> Pervasives.compare x y
+ (* was assert false, but why? *)
+
;;
let compare x y =
- if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0
+ (* if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 *)
+ if x = y then 0
else compare x y
;;
let saturate t ty =
let sty, _, args =
- NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
+ NCicMetaSubst.saturate ~delta:0 C.metasenv C.subst C.context
ty 0
in
let proof =