;;
+let test_subst () =
+ let module C = Cic in
+ let module M = CicMetaSubst in
+ let term = C.Appl [
+ C.Rel 1;
+ C.Appl [C.Rel 11;
+ C.Meta (43, []);
+ C.Appl [C.Rel 15; C.Rel 12; C.Meta (41, [])]];
+ C.Appl [C.Rel 11;
+ C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])];
+ C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (12, [])]]
+ ] in
+ let subst1 = [
+ (43, ([], C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])], C.Rel 16));
+ (10, ([], C.Rel 12, C.Rel 16));
+ (12, ([], C.Meta (41, []), C.Rel 16))
+ ]
+ and subst2 = [
+ (43, ([], C.Appl [C.Rel 15; C.Rel 12; C.Meta (11, [])], C.Rel 16));
+ (10, ([], C.Rel 12, C.Rel 16));
+ (12, ([], C.Meta (41, []), C.Rel 16))
+ ] in
+ let t1 = M.apply_subst subst1 term
+ and t2 = M.apply_subst subst2 term in
+ Printf.printf "t1 = %s\nt2 = %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
+;;
+
+
(* differing ();; *)
(* next_after ();; *)
-discrimination_tree_test ();;
+(* discrimination_tree_test ();; *)
(* path_indexing_test ();; *)
+test_subst ();;