Referring to evars by names. Added a parser for evars (but parsing of

instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.

18 files changed, 210 insertions, 105 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index f9bd2d405..62bfef886 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -41,22 +41,24 @@ type pattern_matching_error =
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
 
-exception PatternMatchingError of env * pattern_matching_error
+exception PatternMatchingError of env * evar_map * pattern_matching_error
 
-let raise_pattern_matching_error (loc,ctx,te) =
-  Loc.raise loc (PatternMatchingError(ctx,te))
+let raise_pattern_matching_error (loc,env,sigma,te) =
+  Loc.raise loc (PatternMatchingError(env,sigma,te))
 
-let error_bad_pattern_loc loc cstr ind =
-  raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind))
+let error_bad_pattern_loc loc env sigma cstr ind =
+  raise_pattern_matching_error
+    (loc, env, sigma, BadPattern (cstr,ind))
 
 let error_bad_constructor_loc loc cstr ind =
-  raise_pattern_matching_error (loc, Global.env(), BadConstructor (cstr,ind))
+  raise_pattern_matching_error
+    (loc, Global.env(), Evd.empty, BadConstructor (cstr,ind))
 
 let error_wrong_numarg_constructor_loc loc env c n =
-  raise_pattern_matching_error (loc, env, WrongNumargConstructor(c,n))
+  raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargConstructor(c,n))
 
 let error_wrong_numarg_inductive_loc loc env c n =
-  raise_pattern_matching_error (loc, env, WrongNumargInductive(c,n))
+  raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n))
 
 let rec list_try_compile f = function
   | [a] -> f a
@@ -479,18 +481,18 @@ let check_and_adjust_constructor env ind cstrs = function
 	with Not_found ->
 	  error_bad_constructor_loc loc cstr ind
 
-let check_all_variables typ mat =
+let check_all_variables env sigma typ mat =
   List.iter
     (fun eqn -> match current_pattern eqn with
        | PatVar (_,id) -> ()
        | PatCstr (loc,cstr_sp,_,_) ->
-	   error_bad_pattern_loc loc cstr_sp typ)
+	   error_bad_pattern_loc loc env sigma cstr_sp typ)
     mat
 
 let check_unused_pattern env eqn =
   if not !(eqn.used) then
     raise_pattern_matching_error
-      (eqn.eqn_loc, env, UnusedClause eqn.patterns)
+      (eqn.eqn_loc, env, Evd.empty, UnusedClause eqn.patterns)
 
 let set_used_pattern eqn = eqn.used := true
 
@@ -1254,7 +1256,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   let () = match submat with
   | [] ->
     raise_pattern_matching_error
-      (Loc.ghost, pb.env, NonExhaustive (complete_history history))
+      (Loc.ghost, pb.env, Evd.empty, NonExhaustive (complete_history history))
   | _ -> ()
   in
 
@@ -1301,7 +1303,7 @@ and match_current pb (initial,tomatch) =
   let ((current,typ),deps,dep) = tomatch in
   match typ with
     | NotInd (_,typ) ->
-	check_all_variables typ pb.mat;
+	check_all_variables pb.env !(pb.evdref) typ pb.mat;
 	compile_all_variables initial tomatch pb
     | IsInd (_,(IndType(indf,realargs) as indt),names) ->
 	let mind,_ = dest_ind_family indf in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index d875edd79..e51055cef 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -27,7 +27,7 @@ type pattern_matching_error =
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
 
-exception PatternMatchingError of env * pattern_matching_error
+exception PatternMatchingError of env * evar_map * pattern_matching_error
 
 val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 3a355b91a..3bd23a802 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -393,7 +393,7 @@ let detype_instance l =
   if Univ.Instance.is_empty l then None
   else Some (List.map detype_level (Array.to_list (Univ.Instance.to_array l)))
 
-let rec detype (isgoal:bool) avoid env t =
+let rec detype isgoal avoid env sigma t =
   match kind_of_term (collapse_appl t) with
     | Rel n ->
       (try match lookup_name_of_rel n env with
@@ -404,25 +404,26 @@ let rec detype (isgoal:bool) avoid env t =
 	 in GVar (dl, Id.of_string s))
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
-	GEvar (dl, Evar.unsafe_of_int n, None)
+        (* using numbers to be unparsable *)
+	GEvar (dl, Id.of_string (string_of_int n), None)
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
 	 with Not_found -> GVar (dl, id))
     | Sort s -> GSort (dl,detype_sort s)
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
-        detype isgoal avoid env c1
+        detype isgoal avoid env sigma c1
     | Cast (c1,k,c2) ->
-        let d1 = detype isgoal avoid env c1 in
-	let d2 = detype isgoal avoid env c2 in
+        let d1 = detype isgoal avoid env sigma c1 in
+	let d2 = detype isgoal avoid env sigma c2 in
     let cast = match k with
     | VMcast -> CastVM d2
     | NATIVEcast -> CastNative d2
     | _ -> CastConv d2
     in
 	GCast(dl,d1,cast)
-    | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
-    | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
-    | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
+    | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env sigma na ty c
+    | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env sigma na ty c
+    | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env sigma na b c
     | App (f,args) ->
       let mkapp f' args' = 
  	match f' with
@@ -430,30 +431,34 @@ let rec detype (isgoal:bool) avoid env t =
  	  GApp (dl,f',args''@args')
  	| _ -> GApp (dl,f',args')
       in
- 	mkapp (detype isgoal avoid env f)
- 	  (Array.map_to_list (detype isgoal avoid env) args)
+	mkapp (detype isgoal avoid env sigma f)
+	  (Array.map_to_list (detype isgoal avoid env sigma) args)
     | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u)
     | Proj (p,c) ->
-        GProj (dl, p, detype isgoal avoid env c)
-    | Evar (ev,cl) ->
-        GEvar (dl, ev,
-               Some (List.map (detype isgoal avoid env) (Array.to_list cl)))
+        GProj (dl, p, detype isgoal avoid env sigma c)
+    | 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
+        GEvar (dl,id,
+               Option.map (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) ->
 	GRef (dl, ConstructRef cstr_sp, detype_instance u)
     | Case (ci,p,c,bl) ->
 	let comp = computable p (ci.ci_pp_info.ind_nargs) in
-	detype_case comp (detype isgoal avoid env)
-	  (detype_eqns isgoal avoid env ci comp)
+	detype_case comp (detype isgoal avoid env sigma)
+	  (detype_eqns isgoal avoid env sigma ci comp)
 	  is_nondep_branch avoid
 	  (ci.ci_ind,ci.ci_pp_info.style,
 	   ci.ci_cstr_ndecls,ci.ci_pp_info.ind_nargs)
 	  (Some p) c bl
-    | Fix (nvn,recdef) -> detype_fix isgoal avoid env nvn recdef
-    | CoFix (n,recdef) -> detype_cofix isgoal avoid env n recdef
+    | Fix (nvn,recdef) -> detype_fix isgoal avoid env sigma nvn recdef
+    | CoFix (n,recdef) -> detype_cofix isgoal avoid env sigma n recdef
 
-and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
+and detype_fix isgoal avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
   let def_avoid, def_env, lfi =
     Array.fold_left
       (fun (avoid, env, l) na ->
@@ -462,14 +467,14 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
       (avoid, env, []) names in
   let n = Array.length tys in
   let v = Array.map3
-    (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
+    (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env sigma c (lift n t))
     bodies tys vn in
   GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-and detype_cofix isgoal avoid env n (names,tys,bodies) =
+and detype_cofix isgoal avoid env sigma n (names,tys,bodies) =
   let def_avoid, def_env, lfi =
     Array.fold_left
       (fun (avoid, env, l) na ->
@@ -478,14 +483,14 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) =
       (avoid, env, []) names in
   let ntys = Array.length tys in
   let v = Array.map2
-    (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t))
+    (fun c t -> share_names isgoal 0 [] def_avoid def_env sigma c (lift ntys t))
     bodies tys in
   GRec(dl,GCoFix n,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-and share_names isgoal n l avoid env c t =
+and share_names isgoal n l avoid env sigma c t =
   match kind_of_term c, kind_of_term t with
     (* factorize even when not necessary to have better presentation *)
     | Lambda (na,t,c), Prod (na',t',c') ->
@@ -493,45 +498,45 @@ and share_names isgoal n l avoid env c t =
             Name _, _ -> na
           | _, Name _ -> na'
           | _ -> na in
-        let t = detype isgoal avoid env t in
+        let t = detype isgoal avoid env sigma t in
 	let id = next_name_away na avoid in
         let avoid = id::avoid and env = add_name (Name id) env in
-        share_names isgoal (n-1) ((Name id,Explicit,None,t)::l) avoid env c c'
+        share_names isgoal (n-1) ((Name id,Explicit,None,t)::l) avoid env sigma c c'
     (* May occur for fix built interactively *)
     | LetIn (na,b,t',c), _ when n > 0 ->
-        let t' = detype isgoal avoid env t' in
-        let b = detype isgoal avoid env b in
+        let t' = detype isgoal avoid env sigma t' in
+        let b = detype isgoal avoid env sigma b in
 	let id = next_name_away na avoid in
         let avoid = id::avoid and env = add_name (Name id) env in
-        share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c (lift 1 t)
+        share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env sigma c (lift 1 t)
     (* Only if built with the f/n notation or w/o let-expansion in types *)
     | _, LetIn (_,b,_,t) when n > 0 ->
-	share_names isgoal n l avoid env c (subst1 b t)
+	share_names isgoal n l avoid env sigma c (subst1 b t)
     (* If it is an open proof: we cheat and eta-expand *)
     | _, Prod (na',t',c') when n > 0 ->
-        let t' = detype isgoal avoid env t' in
+        let t' = detype isgoal avoid env sigma t' in
 	let id = next_name_away na' avoid in
         let avoid = id::avoid and env = add_name (Name id) env in
         let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-        share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c'
+        share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
         if n>0 then msg_warning (strbrk "Detyping.detype: cannot factorize fix enough");
-        let c = detype isgoal avoid env c in
-        let t = detype isgoal avoid env t in
+        let c = detype isgoal avoid env sigma c in
+        let t = detype isgoal avoid env sigma t in
         (List.rev l,c,t)
 
-and detype_eqns isgoal avoid env ci computable constructs consnargsl bl =
+and detype_eqns isgoal avoid env sigma ci computable constructs consnargsl bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
     let mat = build_tree Anonymous isgoal (avoid,env) ci bl in
-    List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c))
+    List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env sigma c))
       mat
   with e when Errors.noncritical e ->
     Array.to_list
-      (Array.map3 (detype_eqn isgoal avoid env) constructs consnargsl bl)
+      (Array.map3 (detype_eqn isgoal avoid env sigma) constructs consnargsl bl)
 
-and detype_eqn isgoal avoid env constr construct_nargs branch =
+and detype_eqn isgoal avoid env sigma constr construct_nargs branch =
   let make_pat x avoid env b ids =
     if force_wildcard () && noccurn 1 b then
       PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids
@@ -544,7 +549,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
     if Int.equal n 0 then
       (dl, Id.Set.elements ids,
        [PatCstr(dl, constr, List.rev patlist,Anonymous)],
-       detype isgoal avoid env b)
+       detype isgoal avoid env sigma b)
     else
       match kind_of_term b with
 	| Lambda (x,_,b) ->
@@ -569,18 +574,18 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
   in
   buildrec Id.Set.empty [] avoid env construct_nargs branch
 
-and detype_binder isgoal bk avoid env na ty c =
+and detype_binder isgoal bk avoid env sigma na ty c =
   let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
   let na',avoid' = match bk with
   | BLetIn -> compute_displayed_let_name_in flag avoid na c
   | _ -> compute_displayed_name_in flag avoid na c in
-  let r =  detype isgoal avoid' (add_name na' env) c in
+  let r =  detype isgoal avoid' (add_name na' env) sigma c in
   match bk with
-  | BProd -> GProd (dl, na',Explicit,detype false avoid env ty, r)
-  | BLambda -> GLambda (dl, na',Explicit,detype false avoid env ty, r)
-  | BLetIn -> GLetIn (dl, na',detype false avoid env ty, r)
+  | BProd -> GProd (dl, na',Explicit,detype false avoid env sigma ty, r)
+  | BLambda -> GLambda (dl, na',Explicit,detype false avoid env sigma ty, r)
+  | BLetIn -> GLetIn (dl, na',detype false avoid env sigma ty, r)
 
-let detype_rel_context where avoid env sign =
+let detype_rel_context where avoid env sigma sign =
   let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
   let rec aux avoid env = function
   | [] -> []
@@ -595,8 +600,8 @@ let detype_rel_context where avoid env sign =
 	    else
 	      compute_displayed_name_in
                 (RenamingElsewhereFor (env,c)) avoid na c in
-      let b = Option.map (detype false avoid env) b in
-      let t = detype false avoid env t in
+      let b = Option.map (detype false avoid env sigma) b in
+      let t = detype false avoid env sigma t in
       (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
   in aux avoid env (List.rev sign)
 
@@ -619,7 +624,7 @@ let rec subst_glob_constr subst raw =
   | GRef (loc,ref,u) ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-         detype false [] [] t
+         detype false [] [] Evd.empty t
 
   | GVar _ -> raw
   | GEvar _ -> raw
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 2cca25fd2..8a8302b8b 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -14,6 +14,7 @@ open Glob_term
 open Termops
 open Mod_subst
 open Misctypes
+open Evd
 
 (** Should we keep details of universes during detyping ? *)
 val print_universes : bool ref
@@ -27,7 +28,8 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr
    [isgoal] tells if naming must avoid global-level synonyms as intro does 
    [ctx] gives the names of the free variables *)
 
-val detype : bool -> Id.t list -> names_context -> constr -> glob_constr
+val detype : bool -> Id.t list -> names_context ->
+  evar_map -> constr -> glob_constr
 
 val detype_case :
   bool -> ('a -> glob_constr) ->
@@ -40,7 +42,7 @@ val detype_case :
 val detype_sort : sorts -> glob_sort
 
 val detype_rel_context : constr option -> Id.t list -> names_context ->
-  rel_context -> glob_decl list
+  evar_map -> rel_context -> glob_decl list
 
 (** look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_displayed  : env -> constr -> Id.t -> int option
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6d7765808..9f5de8c90 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -146,13 +146,7 @@ let restrict_evar_key evd evk filter candidates =
       let candidates = match candidates with
       | NoUpdate -> evi.evar_candidates
       | UpdateWith c -> Some c in
-      let ccl = evi.evar_concl in
-      let sign = evar_hyps evi in
-      let src = evi.evar_source in
-      let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
-      let ctxt = Filter.filter_list filter (evar_context evi) in
-      let id_inst = inst_of_vars ctxt in
-      Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
+      restrict_evar evd evk filter candidates
     end
 
 (* Restrict an applied evar and returns its restriction in the same context *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d14aa23a7..306032ed9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -342,6 +342,10 @@ let push_rel_context_to_named_context env typ =
 
 let default_source = (Loc.ghost,Evar_kinds.InternalHole)
 
+let restrict_evar evd evk filter candidates =
+  let evk' = new_untyped_evar () in
+  Evd.restrict evk evk' filter ?candidates evd, evk'
+
 let new_pure_evar_full evd evi =
   let evk = new_untyped_evar () in
   let evd = Evd.add evd evk evi in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index fc27d4776..2d3dd33a3 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -48,6 +48,9 @@ val e_new_type_evar : evar_map ref ->
 val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
+val restrict_evar : evar_map -> existential_key -> Filter.t ->
+  constr list option -> evar_map * existential_key
+
 (** Polymorphic constants *)
 
 val new_global : evar_map -> Globnames.global_reference -> evar_map * constr
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ff04bda80..17928f26e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -219,6 +219,17 @@ let map_evar_info f evi =
     evar_concl = f evi.evar_concl;
     evar_candidates = Option.map (List.map f) evi.evar_candidates }
 
+type existential_name = Id.t
+
+let evar_ident_info evi =
+  match evi.evar_source with
+  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
+  | _,Evar_kinds.VarInstance id -> id
+  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
+  | _ ->
+      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
+      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+
 (* spiwack: Revised hierarchy :
    - Evar.Map ( Maps of existential_keys )
    - EvarInfoMap ( .t = evar_info Evar.Map.t * evar_info Evar.Map )
@@ -231,7 +242,7 @@ exception NotInstantiatedEvar
 
 (* Note: let-in contributes to the instance *)
 
-let make_evar_instance_array info args =
+let evar_instance_array test_id info args =
   let len = Array.length args in
   let rec instrec filter ctxt i = match filter, ctxt with
   | [], [] ->
@@ -242,7 +253,7 @@ let make_evar_instance_array info args =
   | true :: filter, (id, _, _) :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
-      if isVarId id c then instrec filter ctxt (succ i)
+      if test_id id c then instrec filter ctxt (succ i)
       else (id, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
@@ -250,13 +261,18 @@ let make_evar_instance_array info args =
   match Filter.repr (evar_filter info) with
   | None ->
     let map i (id, _, _) =
-      if (i < len) then (id, Array.unsafe_get args i)
+      if (i < len) then
+        let c = Array.unsafe_get args i in
+        if test_id id c then None else Some (id,c)
       else instance_mismatch ()
     in
-    List.map_i map 0 (evar_context info)
+    List.map_filter_i map (evar_context info)
   | Some filter ->
     instrec filter (evar_context info) 0
 
+let make_evar_instance_array info args =
+  evar_instance_array isVarId info args
+
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
   match inst with
@@ -580,6 +596,7 @@ type evar_map = {
   last_mods  : Evar.Set.t;
   metas      : clbinding Metamap.t;
   effects    : Declareops.side_effects;
+  evar_names : Id.t EvMap.t * existential_key Idmap.t;
 }
 
 (*** Lifting primitive from EvarMap. ***)
@@ -594,9 +611,23 @@ let progress_evar_map d1 d2 =
 
 let add d e i = match i.evar_body with
 | Evar_empty ->
-  { d with undf_evars = EvMap.add e i d.undf_evars; }
+  let evar_names =
+    let (evtoid,idtoev as x) = d.evar_names in
+    if EvMap.mem e evtoid then
+      x
+    else
+      let id = evar_ident_info i in
+      let id = Namegen.next_ident_away_from id
+        (fun id -> Idmap.mem id idtoev) in
+    (EvMap.add e id evtoid, Idmap.add id e idtoev) in
+  { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
 | Evar_defined _ ->
-  { d with defn_evars = EvMap.add e i d.defn_evars; }
+  let evar_names =
+    let (evtoid,idtoev as x) = d.evar_names in
+    try let id = EvMap.find e evtoid in
+        (EvMap.remove e evtoid, Idmap.remove id idtoev)
+    with Not_found -> x in
+  { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
@@ -742,6 +773,7 @@ let empty = {
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
   effects    = Declareops.no_seff;
+  evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
 }
 
 let from_env ?ctx e = 
@@ -772,6 +804,15 @@ let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 
 let evar_source evk d = (find d evk).evar_source
 
+let evar_ident evk evd =
+  try EvMap.find evk (fst evd.evar_names)
+  with Not_found ->
+    (* Unnamed (non-dependent) evar *)
+    Id.of_string (string_of_existential evk)
+
+let evar_key id evd =
+  Idmap.find id (snd evd.evar_names)
+
 let define_aux def undef evk body =
   let oldinfo =
     try EvMap.find evk undef
@@ -792,7 +833,12 @@ let define evk body evd =
   | [] ->  evd.last_mods
   | _ -> Evar.Set.add evk evd.last_mods
   in
-  { evd with defn_evars; undf_evars; last_mods; }
+  let evar_names =
+    let (evtoid,idtoev) = evd.evar_names in
+    let id = EvMap.find evk evtoid in
+    (EvMap.remove evk evtoid, Idmap.remove id idtoev)
+  in
+  { evd with defn_evars; undf_evars; last_mods; evar_names }
 
 let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) 
     ?(filter=Filter.identity) ?candidates ?(store=Store.empty) evd =
@@ -810,7 +856,32 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole))
     evar_candidates = candidates;
     evar_extra = store; }
   in
-  { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; }
+  let evar_names =
+    let (evtoid,idtoev) = evd.evar_names in
+    let id = evar_ident_info evar_info in
+    let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
+    (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+  in
+  { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names }
+
+let restrict evk evk' filter ?candidates evd =
+  let evar_info = EvMap.find evk evd.undf_evars in
+  let evar_info' =
+    { evar_info with evar_filter = filter;
+      evar_candidates = candidates;
+      evar_extra = Store.empty } in
+  let evar_names =
+    let (evtoid,idtoev) = evd.evar_names in
+    let id = EvMap.find evk evtoid in
+    (EvMap.add evk' id (EvMap.remove evk evtoid),
+     Idmap.add id evk' (Idmap.remove id idtoev))
+  in
+  let ctxt = Filter.filter_list filter (evar_context evar_info) in
+  let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
+  let body = mkEvar(evk',id_inst) in
+  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+  { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
+    defn_evars; evar_names }
 
 (* extracts conversion problems that satisfy predicate p *)
 (* Note: conv_pbs not satisying p are stored back in reverse order *)
@@ -1273,7 +1344,9 @@ let set_metas evd metas = {
   conv_pbs = evd.conv_pbs;
   last_mods = evd.last_mods;
   metas;
-  effects = evd.effects; }
+  effects = evd.effects;
+  evar_names = evd.evar_names;
+}
 
 let meta_list evd = metamap_to_list evd.metas
 
@@ -1406,6 +1479,11 @@ let subst_defined_metas bl c =
     | _ -> map_constr substrec c
   in try Some (substrec c) with Not_found -> None
 
+let evar_source_of_meta mv evd =
+  match meta_name evd mv with
+  | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
+  | Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
+
 (*******************************************************************)
 type open_constr = evar_map * constr
 
@@ -1633,23 +1711,24 @@ let pr_evar_map_gen with_univs pr_evars sigma =
   in
   evs ++ svs ++ cstrs ++ metas
 
-let pr_evar_list l =
+let pr_evar_list sigma l =
   let pr (ev, evi) =
     h 0 (str (string_of_existential ev) ++
-      str "==" ++ pr_evar_info evi)
+      str "==" ++ pr_evar_info evi ++
+      str " {" ++ pr_id (evar_ident ev sigma) ++ str "}")
   in
   h 0 (prlist_with_sep fnl pr l)
 
 let pr_evar_by_depth depth sigma = match depth with
 | None ->
   (* Print all evars *)
-  str"EVARS:"++brk(0,1)++pr_evar_list (to_list sigma)++fnl()
+  str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
 | Some n ->
   (* Print all evars *)
   str"UNDEFINED EVARS:"++
   (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
   brk(0,1)++
-  pr_evar_list (evar_dependency_closure n sigma)++fnl()
+  pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
 
 let pr_evar_by_filter filter sigma =
   let defined = Evar.Map.filter filter sigma.defn_evars in
@@ -1657,12 +1736,12 @@ let pr_evar_by_filter filter sigma =
   let prdef =
     if Evar.Map.is_empty defined then mt ()
     else str "DEFINED EVARS:" ++ brk (0, 1) ++
-      pr_evar_list (Evar.Map.bindings defined)
+      pr_evar_list sigma (Evar.Map.bindings defined)
   in
   let prundef =
     if Evar.Map.is_empty undefined then mt ()
     else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
-      pr_evar_list (Evar.Map.bindings undefined)
+      pr_evar_list sigma (Evar.Map.bindings undefined)
   in
   prdef ++ prundef
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 28e978edf..0d88415e2 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -224,6 +224,9 @@ val existential_opt_value : evar_map -> existential -> constr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
+val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info ->
+  'a array -> (Id.t * 'a) list
+
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
 
 val subst_evar_defs_light : substitution -> evar_map -> evar_map
@@ -241,10 +244,18 @@ val evar_declare :
   evar_map -> evar_map
 (** Convenience function. Just a wrapper around {!add}. *)
 
+val restrict : evar -> evar -> Filter.t -> ?candidates:constr list ->
+  evar_map -> evar_map
+
 val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 (** Convenience function. Wrapper around {!find} to recover the source of an
     evar in a given evar map. *)
 
+val evar_ident : existential_key -> evar_map -> Id.t
+
+val evar_key : Id.t -> evar_map -> existential_key
+
+val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located
 (** {5 Side-effects} *)
 
 val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 73bb343ee..8a4fd65a1 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -63,9 +63,9 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
 let rec glob_constr_eq c1 c2 = match c1, c2 with
 | GRef (_, gr1, _), GRef (_, gr2, _) -> eq_gr gr1 gr2
 | GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
-| GEvar (_, ev1, arg1), GEvar (_, ev2, arg2) ->
-  Evar.equal ev1 ev2 &&
-  Option.equal (fun l1 l2 -> List.equal glob_constr_eq l1 l2) arg1 arg2
+| GEvar (_, id1, arg1), GEvar (_, id2, arg2) ->
+  Id.equal id1 id2 &&
+  Option.equal (fun l1 l2 -> List.equal instance_eq l1 l2) arg1 arg2
 | GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
   (b1 : bool) == b2 && Id.equal pat1 pat2
 | GApp (_, f1, arg1), GApp (_, f2, arg2) ->
@@ -134,6 +134,9 @@ and fix_recursion_order_eq o1 o2 = match o1, o2 with
   glob_constr_eq c1 c2 && Option.equal glob_constr_eq o1 o2
 | _ -> false
 
+and instance_eq (x1,c1) (x2,c2) =
+  Id.equal x1 x2 && glob_constr_eq c1 c2
+
 let map_glob_constr_left_to_right f = function
   | GApp (loc,g,args) ->
       let comp1 = f g in
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 8e1b51a7d..245c7f943 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -120,7 +120,8 @@ let hdchar env c =
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
 	let id = match lna.(i) with Name id -> id | _ -> assert false in
 	lowercase_first_char id
-    | Meta _ | Evar _ | Case (_, _, _, _) -> "y"
+    | Evar _ (* We could do better... *)
+    | Meta _ | Case (_, _, _, _) -> "y"
   in
   hdrec 0 c
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 5828e7f43..420666356 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -157,7 +157,7 @@ let pattern_of_constr sigma t =
           | Evar_kinds.MatchingVar (b,id) ->
               ctx := (id,None,existential_type sigma ev)::!ctx;
               assert (not b); PMeta (Some id)
-          | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
+          | Evar_kinds.GoalEvar _ -> PEvar (evk,Array.map pattern_of_constr ctxt)
           | _ -> PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6d98602b5..f26d2d638 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -386,6 +386,8 @@ let is_GHole = function
   | GHole _ -> true
   | _ -> false
 
+let evars = ref Id.Map.empty
+
 let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
   let pretype_type = pretype_type resolve_tc in
@@ -405,13 +407,17 @@ 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, evk, instopt) ->
+  | GEvar (loc, id, instopt) ->
       (* 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 =
+        try Evd.evar_key id !evdref
+        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 -> failwith "Evar subtitutions not implemented" in
+        | Some inst -> error "Non-identity subtitutions of existential variables not implemented" 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
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index ceb01fd95..a00fec30e 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,9 +1,9 @@
 Locusops
 Termops
+Namegen
 Evd
 Reductionops
 Vnorm
-Namegen
 Inductiveops
 Nativenorm
 Retyping
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b4c578abb..91447573f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -28,7 +28,7 @@ open Pretype_errors
 (* Errors *)
 
 type reduction_tactic_error =
-    InvalidAbstraction of env * constr * (env * Type_errors.type_error)
+    InvalidAbstraction of env * Evd.evar_map * constr * (env * Type_errors.type_error)
 
 exception ReductionTacticError of reduction_tactic_error
 
@@ -1112,7 +1112,7 @@ let pattern_occs loccs_trm env sigma c =
     let _ = Typing.type_of env sigma abstr_trm in
     applist(abstr_trm, List.map snd loccs_trm)
   with Type_errors.TypeError (env',t) ->
-    raise (ReductionTacticError (InvalidAbstraction (env,abstr_trm,(env',t))))
+    raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
 
 (* Used in several tactics. *)
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 6d12d5d44..db59787a1 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -17,7 +17,7 @@ open Locus
 open Univ
 
 type reduction_tactic_error =
-    InvalidAbstraction of env * constr * (env * Type_errors.type_error)
+    InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error)
 
 exception ReductionTacticError of reduction_tactic_error
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index a3bd06ed5..c74ed19a8 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -497,7 +497,7 @@ let is_instance = function
   | _ -> false
 
 let is_implicit_arg = function
-| Evar_kinds.GoalEvar -> false
+| Evar_kinds.GoalEvar _ -> false
 | _ -> true
   (* match k with *)
   (*     ImplicitArg (ref, (n, id), b) -> true *)
@@ -538,10 +538,10 @@ open Evar_kinds
 type evar_filter = existential_key -> Evar_kinds.t -> bool
 
 let all_evars _ _ = true
-let all_goals _ = function GoalEvar -> true | _ -> false
+let all_goals _ = function GoalEvar _ -> true | _ -> false
 let no_goals ev evi = not (all_goals ev evi)
 let no_goals_or_obligations _ = function
-  | GoalEvar | QuestionMark _ -> false
+  | GoalEvar _ | QuestionMark _ -> false
   | _ -> true
 
 let mark_resolvability filter b sigma =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d89cde1ae..63c30eb35 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -125,11 +125,6 @@ let rec subst_meta_instances bl c =
 
 (** [env] should be the context in which the metas live *)
 
-let evar_source_of_meta mv evd =
-  match Evd.meta_name evd mv with
-  | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
-  | Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
-
 let pose_all_metas_as_evars env evd t =
   let evdref = ref evd in
   let rec aux t = match kind_of_term t with
@@ -139,7 +134,7 @@ let pose_all_metas_as_evars env evd t =
        | None ->
         let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
         let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
-        let src = evar_source_of_meta mv !evdref in
+        let src = Evd.evar_source_of_meta mv !evdref in
         let ev = Evarutil.e_new_evar evdref env ~src ty in
         evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
         ev)