#### EXPERIMENTAL COMMIT ####

[helm.git] / helm / software / components / cic_proof_checking / cicReduction.ml

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 18259a00441873ea85ea755e3a06e891de291872..0bc05674bced1f7ccf563c06532ab5cedb272b3a 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -1072,3 +1072,18 @@ let rec head_beta_reduce =
          head_beta_reduce he'''
   | Cic.Cast (te,_) -> head_beta_reduce te
   | t -> t
+
+(*Debugging code
+let are_convertible ?subst ?metasenv context t1 t2 ugraph =
+ let before = Unix.gettimeofday () in
+ let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in
+ let after = Unix.gettimeofday () in
+ let diff = after -. before in
+  if diff > 0.1 then
+   begin
+    let nc = List.map (function None -> None | Some (n,_) -> Some n) context in
+     prerr_endline
+      ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc);
+   end;
+  res
+*)