]> matita.cs.unibo.it Git - helm.git/commitdiff
More debug informations.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Feb 2004 12:34:32 +0000 (12:34 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Feb 2004 12:34:32 +0000 (12:34 +0000)
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) ->