From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 2 Feb 2004 16:15:43 +0000 (+0000)
Subject: - bugfix for expand_implicits, return correct term on Fix and CoFix cases
X-Git-Tag: V_0_2_3~113
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ea34971b64c60e5440bf2cc42cee560f6a86abe;p=helm.git

- 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 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