(* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
+let reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
+
module type NCicContext =
sig
val metasenv : NCic.metasenv
let rec compare x y =
match x,y with
- | NCic.Rel i, NCic.Rel j -> i-j
+ | NCic.Rel i, NCic.Rel j -> j-i
| NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
| NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
| NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
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