X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=24ab7b4afbf1129cafb2d0462a169bf26ca42913;hb=4d602b51da8071c1d21424ec78691c90b2bd2f0e;hp=d34e3efcc00abb6a485ecafe1de844b8ea9f902d;hpb=a981b42002f822aa49a41b3889a76b9438b093bb;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d34e3efcc..24ab7b4af 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -147,19 +147,24 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
     if swap then unify test_eq_only m s c t2 t1 
     else unify test_eq_only m s c t1 t2
   in
-  let ty_t = 
-    try NCicTypeChecker.typeof ~subst ~metasenv context t 
-    with NCicTypeChecker.TypeCheckerFailure msg -> 
-      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
-      prerr_endline (Lazy.force msg);
-      assert false
-  in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  let lty = NCicSubstitution.subst_meta lc ty in
-  pp (lazy("On the types: " ^
-   NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
-    ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
-  let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
+  let metasenv, subst = 
+    match ty with 
+    | NCic.Implicit (`Typeof _) -> metasenv, subst
+    | _ ->
+       let lty = NCicSubstitution.subst_meta lc ty in
+       let ty_t = 
+         try NCicTypeChecker.typeof ~subst ~metasenv context t 
+         with NCicTypeChecker.TypeCheckerFailure msg -> 
+           prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+           prerr_endline (Lazy.force msg);
+           assert false
+       in
+       pp (lazy("On the types: " ^
+        NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
+         ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
+       unify test_eq_only metasenv subst context lty ty_t 
+  in
   let (metasenv, subst), t = 
     try NCicMetaSubst.delift metasenv subst context n lc t
     with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
@@ -169,6 +174,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
   try
     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
     let oldt = NCicSubstitution.subst_meta lc oldt in
+    let t = NCicSubstitution.subst_meta lc t in
     (* conjecture: always fail --> occur check *)
     unify test_eq_only metasenv subst context oldt t
   with NCicUtils.Subst_not_found _ -> 
@@ -176,7 +182,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
      * we could ? := Type_j with j <= i... *)
     let subst = (n, (name, ctx, t, ty)) :: subst in
     pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
-      ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t)));
+      ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
     let metasenv = 
       List.filter (fun (m,_) -> not (n = m)) metasenv 
     in