From 616ca3a4330ac51127b0bd91644354ac888d1ce3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Feb 2004 18:39:42 +0000 Subject: [PATCH] Substitution no longer returned from CicRefine.type_of_aux --- helm/ocaml/cic_disambiguation/disambiguate.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 _ -> -- 2.39.2