Parsing evar instances.

5 files changed, 27 insertions, 9 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 3bd23a8025..b59f67bc3c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -405,7 +405,7 @@ let rec detype isgoal avoid env sigma t =
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
         (* using numbers to be unparsable *)
-	GEvar (dl, Id.of_string (string_of_int n), None)
+	GEvar (dl, Id.of_string (string_of_int n), [])
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
 	 with Not_found -> GVar (dl, id))
@@ -439,10 +439,10 @@ let rec detype isgoal avoid env sigma t =
     | Evar (evk,cl) ->
       let id,l =
         try Evd.evar_ident evk sigma,
-            Some (Evd.evar_instance_array isVarId (Evd.find sigma evk) cl)
-        with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), None in
+            Evd.evar_instance_array isVarId (Evd.find sigma evk) cl
+        with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), [] in
         GEvar (dl,id,
-               Option.map (List.map (on_snd (detype isgoal avoid env sigma))) l)
+               List.map (on_snd (detype isgoal avoid env sigma)) l)
     | Ind (ind_sp,u) ->
 	GRef (dl, IndRef ind_sp, detype_instance u)
     | Construct (cstr_sp,u) ->
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 17928f26ea..4dc3672a46 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -279,6 +279,22 @@ 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
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 0d88415e2c..2cea0eaa2a 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -229,6 +229,8 @@ val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info ->
 
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
 
+val complete_instance : named_context -> (Id.t * constr) list -> constr array
+
 val subst_evar_defs_light : substitution -> evar_map -> evar_map
 (** Assume empty universe constraints in [evar_map] and [conv_pbs] *)
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 8a4fd65a19..fb52a0481c 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -65,7 +65,7 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with
 | GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
 | GEvar (_, id1, arg1), GEvar (_, id2, arg2) ->
   Id.equal id1 id2 &&
-  Option.equal (fun l1 l2 -> List.equal instance_eq l1 l2) arg1 arg2
+  List.equal instance_eq arg1 arg2
 | GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
   (b1 : bool) == b2 && Id.equal pat1 pat2
 | GApp (_, f1, arg1), GApp (_, f2, arg2) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f26d2d638e..a21548d574 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -407,7 +407,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id)
       tycon
 
-  | GEvar (loc, id, instopt) ->
+  | GEvar (loc, id, inst) ->
       (* Ne faudrait-il pas s'assurer que hyps est bien un
 	 sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
       let evk =
@@ -415,9 +415,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         with Not_found ->
           user_err_loc (loc,"",str "Unknown existential variable.") in
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
-      let args = match instopt with
-        | None -> Array.of_list (instance_from_named_context hyps)
-        | Some inst -> error "Non-identity subtitutions of existential variables not implemented" in
+      let f c = (pretype empty_tycon env evdref lvar c).uj_val in
+      let inst = List.map (on_snd f) inst in
+      let args = complete_instance hyps inst in
       let c = mkEvar (evk, args) in
       let j = (Retyping.get_judgment_of env !evdref c) in
 	inh_conv_coerce_to_tycon loc env evdref j tycon