- bugfix for expand_implicits, return correct term on Fix and CoFix cases

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
index 0ee364053f846667059467ec1dc7ac44afe73cb5..6944a4fc210dfe1a68d016dcf513e5f4d9a86d09 100644 (file)
--- 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