- NCicPp.ppterm applies the substitution

[helm.git] / helm / software / components / ng_kernel / nCicReduction.ml

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 4de73408fb2ff026a0481a18d24fa64af00c101b..bd7cbc842b1ad79bea25b565bd7b25faedf99168 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -171,8 +171,12 @@ let whd = R.whd
 
 let (===) x y = Pervasives.compare x y = 0 ;;
 
+let get_relevance = ref (fun ~subst:_ _ _ -> assert false);;
+
+let set_get_relevance f = get_relevance := f;;
+
 (* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) get_exact_relev =
+let are_convertible ?(subst=[]) =
  let rec aux test_eq_only context t1 t2 =
    let alpha_eq test_eq_only t1 t2 =
      if t1 === t2 then
@@ -239,7 +243,7 @@ let are_convertible ?(subst=[]) get_exact_relev =
               tl1 tl2 true relevance
             with Invalid_argument _ -> false
               | HExtlib.FailureAt fail ->
-                let relevance = get_exact_relev ~subst context hd1 tl1 in
+                let relevance = !get_relevance ~subst context hd1 tl1 in
                 let _,relevance = HExtlib.split_nth fail relevance in
                 let b,relevance = (match relevance with
                   | [] -> assert false
@@ -256,7 +260,7 @@ let are_convertible ?(subst=[]) get_exact_relev =
 
        | (C.Appl (hd1::tl1),  C.Appl (hd2::tl2)) ->
            aux test_eq_only context hd1 hd2 &&
-          let relevance = get_exact_relev ~subst context hd1 tl1 in
+          let relevance = !get_relevance ~subst context hd1 tl1 in
             (try
              HExtlib.list_forall_default3
               (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)