From e874af2d785b2b383ae8444fdd32bb5344fb914f Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 2 Feb 2004 17:01:50 +0000
Subject: [PATCH] - refine's type_of no longer return a substitution

---
 helm/ocaml/cic_unification/cicMetaSubst.ml  |  8 ++++++++
 helm/ocaml/cic_unification/cicMetaSubst.mli |  1 +
 helm/ocaml/cic_unification/cicRefine.ml     | 21 +++++++--------------
 helm/ocaml/cic_unification/cicRefine.mli    |  3 +--
 4 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index a28b853be..ba8ae7d98 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -475,6 +475,14 @@ let rec apply_subst_context subst context =
       | None -> None :: context)
     context []
 
+let apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, apply_subst_context subst context, apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+      metasenv)
+
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
 let ppcontext ?(sep = "\n") subst context =
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index fd770215a..730afcd10 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -54,6 +54,7 @@ val apply_subst_reducing :
  (int * int) option -> substitution -> Cic.term -> Cic.term
 
 val apply_subst_context : substitution -> Cic.context -> Cic.context
+val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
 
 (** {2 Pretty printers} *)
 
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 3fc0dcf5a..a6506d5ca 100644
--- 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:";
diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli
index ce97e8ab7..28a34f5ff 100644
--- a/helm/ocaml/cic_unification/cicRefine.mli
+++ b/helm/ocaml/cic_unification/cicRefine.mli
@@ -32,7 +32,6 @@ exception WrongUriToMutualInductiveDefinitions of string
 (* type_of_aux' metasenv context term                        *)
 (* refines [term] and returns the refined form of [term],    *)
 (* its type, the computed substitution and the new metasenv. *)
-(* The substitution returned is already unwinded             *)
 val type_of_aux':
  Cic.metasenv -> Cic.context -> Cic.term ->
-  Cic.term * Cic.term * CicMetaSubst.substitution * Cic.metasenv
+  Cic.term * Cic.term * Cic.metasenv
-- 
2.39.2