- refine's type_of no longer return a substitution

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 3fc0dcf5a4003585b10f17e19240fc0932c04994..a6506d5cacb057c13c0f7de4813364c813922d68 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -460,13 +460,8 @@ and type_of_aux' metasenv context t =
 
  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
   let module C = Cic in
-   (* ti could be a metavariable in the domain of the substitution *)
-   let t1' = CicMetaSubst.apply_subst subst t1 in
-   let t2' = CicMetaSubst.apply_subst subst t2 in
-    let t1'' = CicMetaSubst.whd subst context t1' in
-    let t2'' =
-      CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2'
-    in
+    let t1'' = CicMetaSubst.whd subst context t1 in
+    let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
@@ -519,24 +514,22 @@ and type_of_aux' metasenv context t =
      (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst'))
      metasenv'
    in
-    CicMetaSubst.apply_subst subst' t,
-     CicMetaSubst.apply_subst subst' ty,
-      subst', metasenv''
+   (CicMetaSubst.apply_subst subst' t,
+    CicMetaSubst.apply_subst subst' ty,
+    CicMetaSubst.apply_subst_metasenv subst' metasenv'')
 ;;
 
 (* DEBUGGING ONLY *)
 let type_of_aux' metasenv context term =
  try
-  let (t,ty,s,m) = type_of_aux' metasenv context term in
+  let (t,ty,m) = type_of_aux' metasenv context term in
    debug_print
     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 (*
-   debug_print
-    ("@@@ REFINE SUCCESSFUL (subst):\n" ^ CicMetaSubst.ppsubst s);
    debug_print
     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
 *)
-   (t,ty,s,m)
+   (t,ty,m)
  with
  | CicUnification.AssertFailure msg as e ->
      debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";