]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/testlibrary.ml
The disambiguation now returns a list of interpretations.
[helm.git] / helm / gTopLevel / testlibrary.ml
index 6c76a6b2d79e09f88c2e991ec4c6adc7cc9ab7cb..e40981861ff756fd3d75b8d12e9ae2d4b011581e 100644 (file)
@@ -44,11 +44,11 @@ let test_uri uri =
     debug_print ("ast:\n" ^ new_pp);
     let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
     debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
-    let (_, _, term) =
-      Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
-        DisambiguateTypes.Environment.empty
-    in
-    debug_print ("term: " ^ CicPp.ppterm term)
+    List.iter
+     (fun (_, _, term) ->
+       debug_print ("term: " ^ CicPp.ppterm term))
+     (Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
+       DisambiguateTypes.Environment.empty)
   in
   match annobj with
   | Cic.AConstant (_, _, _, None, ty, _) ->