]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.ml
More debug informations.
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml
index 41c404392f429b2ac4a68debe6c5f9c36207a34c..e8d3e58f15e303607496d1f82ada36d754de7fa5 100644 (file)
@@ -381,6 +381,7 @@ module Make (C: Callbacks) =
           let rec filter = function
             | [] -> []
             | codomain_item :: tl ->
+                debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
                 let new_env = Environment.add item codomain_item current_env in
                 (match test_env new_env remaining_dom with
                 | Ok (term, metasenv) ->