Substitution no longer returned from CicRefine.type_of_aux

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 5a8b9a646b02749946276b92e65206ed971deb77..41c404392f429b2ac4a68debe6c5f9c36207a34c 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -51,7 +51,7 @@ let refine metasenv context term =
   let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
   debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
   try
-    let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in
+    let term', _, metasenv' = CicRefine.type_of_aux' metasenv context term in
     Ok (term', metasenv')
   with
     | CicRefine.Uncertain _ ->