From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 2 Feb 2004 18:39:42 +0000 (+0000)
Subject: Substitution no longer returned from CicRefine.type_of_aux
X-Git-Tag: V_0_2_3~102
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=616ca3a4330ac51127b0bd91644354ac888d1ce3;p=helm.git

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 5a8b9a646..41c404392 100644
--- 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 _ ->