Remove unused substitution functions in checker.

4 files changed, 0 insertions, 124 deletions

diff --git a/checker/term.ml b/checker/term.ml
index 3438f497a..1b8177325 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -404,77 +404,6 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
 let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c
 
-let subst_univs_fn_constr f c =
-  let changed = ref false in
-  let fu = Univ.subst_univs_universe f in
-  let fi = Univ.Instance.subst_fn (Univ.level_subst_of f) in
-  let rec aux t = 
-    match t with
-    | Sort (Type u) -> 
-      let u' = fu u in
-	if u' == u then t else 
-	  (changed := true; Sort (Type u'))
-    | Const (c, u) -> 
-      let u' = fi u in 
-	if u' == u then t
-	else (changed := true; Const (c, u'))
-    | Ind (i, u) ->
-      let u' = fi u in 
-	if u' == u then t
-	else (changed := true; Ind (i, u'))
-    | Construct (c, u) ->
-      let u' = fi u in 
-	if u' == u then t
-	else (changed := true; Construct (c, u'))
-    | _ -> map_constr aux t
-  in 
-  let c' = aux c in
-    if !changed then c' else c
-
-let subst_univs_constr subst c =
-  if Univ.is_empty_subst subst then c
-  else 
-    let f = Univ.make_subst subst in
-      subst_univs_fn_constr f c
-
-
-let subst_univs_level_constr subst c =
-  if Univ.is_empty_level_subst subst then c
-  else 
-    let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in
-    let changed = ref false in
-    let rec aux t = 
-      match t with
-      | Const (c, u) -> 
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Const (c, u'))
-      | Ind (i, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-	  let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Ind (i, u'))
-      | Construct (c, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Construct (c, u'))
-      | Sort (Type u) -> 
-         let u' = Univ.subst_univs_level_universe subst u in
-	   if u' == u then t else 
-	     (changed := true; Sort (Type u'))
-      | _ -> map_constr aux t
-    in
-    let c' = aux c in
-      if !changed then c' else c
-
-let subst_univs_level_context s = 
-  map_rel_context (subst_univs_level_constr s)
-
 let subst_instance_constr subst c =
   if Univ.Instance.is_empty subst then c
   else
@@ -509,9 +438,6 @@ let subst_instance_constr subst c =
     let c' = aux c in
       if !changed then c' else c
 
-(* let substkey = Profile.declare_profile "subst_instance_constr";; *)
-(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *)
-
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
   else map_rel_context (fun x -> subst_instance_constr s x) ctx
diff --git a/checker/term.mli b/checker/term.mli
index 3c4835dbb..ab488b2b7 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -53,10 +53,6 @@ val isArity : constr -> bool
 val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 val eq_constr : constr -> constr -> bool
 
-val subst_univs_constr : Univ.universe_subst -> constr -> constr
-val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr
-val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context
-
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : Univ.universe_instance -> constr -> constr
 val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context
diff --git a/checker/univ.ml b/checker/univ.ml
index 04897e85c..a895021f0 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1299,14 +1299,7 @@ type universe_context = UContext.t
 
 (** Substitutions. *)
 
-let make_universe_subst inst (ctx, csts) = 
-  try Array.fold_left2 (fun acc c i -> LMap.add c i acc)
-        LMap.empty (Instance.to_array ctx) (Instance.to_array inst)
-  with Invalid_argument _ -> 
-    anomaly (Pp.str "Mismatched instance and context when building universe substitution")
-
 let is_empty_subst = LMap.is_empty
-
 let empty_level_subst = LMap.empty
 let is_empty_level_subst = LMap.is_empty
 
@@ -1322,20 +1315,6 @@ let subst_univs_level_universe subst u =
   let u' = Universe.smartmap f u in
     if u == u' then u
     else Universe.sort u'
-	
-let subst_univs_level_constraint subst (u,d,v) =
-  let u' = subst_univs_level_level subst u 
-  and v' = subst_univs_level_level subst v in
-    if d != Lt && Level.equal u' v' then None
-    else Some (u',d,v')
-
-let subst_univs_level_constraints subst csts =
-  Constraint.fold 
-    (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
-    csts Constraint.empty 
-
-(* let instantiate_univ_context subst (_, csts) =  *)
-(*   subst_univs_level_constraints subst csts *)
 
 (** Substitute instance inst for ctx in csts *)
 
@@ -1395,24 +1374,6 @@ let subst_univs_universe fn ul =
 	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
 	  substs nosubst
 
-let subst_univs_level fn l = 
-  try Some (fn l)
-  with Not_found -> None
-
-let subst_univs_constraint fn (u,d,v as c) cstrs =
-  let u' = subst_univs_level fn u in
-  let v' = subst_univs_level fn v in
-  match u', v' with
-  | None, None -> Constraint.add c cstrs
-  | Some u, None -> enforce_univ_constraint (u,d,make v) cstrs
-  | None, Some v -> enforce_univ_constraint (make u,d,v) cstrs
-  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
-
-let subst_univs_constraints subst csts =
-  Constraint.fold 
-    (fun c cstrs -> subst_univs_constraint subst c cstrs)
-    csts Constraint.empty 
-
 (** Pretty-printing *)
 
 let pr_arc = function
diff --git a/checker/univ.mli b/checker/univ.mli
index 27f4c9a6e..89dd64486 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -197,19 +197,12 @@ val is_empty_level_subst : universe_level_subst -> bool
 val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
 val subst_univs_level_universe : universe_level_subst -> universe -> universe
 
-(** Make a universe level substitution: the instances must match. *)
-val make_universe_subst : Instance.t -> universe_context -> universe_level_subst
-(** Get the instantiated graph. *)
-val instantiate_univ_context : universe_level_subst -> universe_context -> constraints
-
 (** Level to universe substitutions. *)
 
 val is_empty_subst : universe_subst -> bool
 val make_subst : universe_subst -> universe_subst_fn
 
 val subst_univs_universe : universe_subst_fn -> universe -> universe
-val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
-
 
 (** Substitution of instances *)
 val subst_instance_instance : universe_instance -> universe_instance -> universe_instance