From b82f304b26de27ec6f59faa29ec41eadd221cfa8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 9 Feb 2004 09:27:25 +0000 Subject: [PATCH] eat_prods now uses mk_implicit_type. --- helm/ocaml/cic_unification/cicRefine.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 338928e8d..fbbb10a6e 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -527,7 +527,7 @@ and type_of_aux' metasenv context t = in let context'' = Some (name, Cic.Decl argty') :: context' in let (metasenv, idx) = - CicMkImplicit.mk_implicit metasenv (context'' @ context) in + CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in let irl = (Some (Cic.Rel 1))::args' @ (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2 -- 2.39.2