From 7ea34971b64c60e5440bf2cc42cee560f6a86abe Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 16:15:43 +0000 Subject: [PATCH] - bugfix for expand_implicits, return correct term on Fix and CoFix cases --- helm/ocaml/cic_unification/cicMkImplicit.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 0ee364053..6944a4fc2 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -149,6 +149,7 @@ let expand_implicits metasenv context term = (new_metasenv, (name, new_type) :: types)) funs (metasenv, []) in +List.iter (fun (_, t) -> assert (t <> Cic.Implicit)) types; let context' = (List.rev_map (fun (name, t) -> Some (Cic.Name name, Cic.Decl t)) @@ -166,7 +167,7 @@ let expand_implicits metasenv context term = | ((name, index, _, _) :: funs_tl), ((_, typ) :: typ_tl), (body :: body_tl) -> - (name, index, typ, term) :: combine (funs_tl, typ_tl, body_tl) + (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl) | [], [], [] -> [] | _ -> assert false in @@ -197,7 +198,7 @@ let expand_implicits metasenv context term = | ((name, _, _) :: funs_tl), ((_, typ) :: typ_tl), (body :: body_tl) -> - (name, typ, term) :: combine (funs_tl, typ_tl, body_tl) + (name, typ, body) :: combine (funs_tl, typ_tl, body_tl) | [], [], [] -> [] | _ -> assert false in -- 2.39.2