Checking typability of evar instances. Using ";" to separate bindings

in instances.

1 files changed, 2 insertions, 16 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4dc3672a4..813a21229 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -279,22 +279,6 @@ let instantiate_evar_array info c args =
   | [] -> c
   | _ -> replace_vars inst c
 
-let complete_instance hyps update =
-  let oldinst = List.map (fun (id,_,_) -> mkVar id) hyps in
-  let rec aux seen newinst = function
-    | [] -> newinst
-    | (id,c) :: l ->
-        if List.mem id seen then
-          user_err_loc (Loc.ghost,"",pr_id id ++ str "appears more than once.")
-        else
-          let l1,l2 = List.split_when (fun c -> isVarId id c) newinst in
-          match l2 with
-          | [] ->
-              user_err_loc (Loc.ghost,"",str "No such variable in the signature of the existential variable: " ++ pr_id id)
-          | _::tl ->
-              aux (id::seen) (l1 @ c :: tl) l in
-  Array.of_list (aux [] oldinst update)
-
 module StringOrd = struct type t = string let compare = String.compare end
 module UNameMap = struct
 
@@ -1554,6 +1538,8 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (**********************************************************)
 (* Pretty-printing *)
 
+let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma)
+
 let pr_instance_status (sc,typ) =
   begin match sc with
   | IsSubType -> str " [or a subtype of it]"