The regression tests now check also the generated disambiguation environments.

[helm.git] / helm / gTopLevel / batchParser.ml

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
index 515c417cb4cc1e29d996e3b9ae9b450ba96d9ebc..f7370422f7fccf70b03ebe0bd9508c0b27eb2223 100644 (file)
--- a/helm/gTopLevel/batchParser.ml
+++ b/helm/gTopLevel/batchParser.ml
@@ -66,11 +66,10 @@ let parse mqi_handle ?(uri_pred = constants_only) =
   let empty_context = [] in
   let empty_metasenv = [] in
   fun input ->
-   List.map (fun (_,metasenv,term) -> metasenv,term)
-    (Disambiguate'.disambiguate_term
-      mqi_handle empty_context empty_metasenv input empty_environment)
+   (Disambiguate'.disambiguate_term
+     mqi_handle empty_context empty_metasenv input empty_environment)
 
 let parse_pp mqi_handle ?uri_pred input = 
- List.map (fun (_,t) -> CicPp.ppterm t)
+ List.map (fun (_,_,t) -> CicPp.ppterm t)
   (parse mqi_handle ?uri_pred input)