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.

6 files changed, 52 insertions, 43 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 1ba0cafa7..ca36f4c9f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -151,9 +151,8 @@ let rec constr_expr_eq e1 e2 =
   | CHole _, CHole _ -> true
   | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) ->
     (b1 : bool) == b2 && Id.equal i1 i2
-  | CEvar (_, ev1, c1), CEvar (_, ev2, c2) ->
-    Evar.equal ev1 ev2 &&
-    Option.equal (List.equal constr_expr_eq) c1 c2
+  | CEvar (_, id1, c1), CEvar (_, id2, c2) ->
+    Id.equal id1 id2 && Option.equal (List.equal instance_eq) c1 c2
   | CSort(_,s1), CSort(_,s2) ->
     Miscops.glob_sort_eq s1 s2
   | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
@@ -226,6 +225,9 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
   List.equal (List.equal constr_expr_eq) el1 el2 &&
   List.equal (List.equal local_binder_eq) bl1 bl2
 
+and instance_eq (x1,c1) (x2,c2) =
+  Id.equal x1 x2 && constr_expr_eq c1 c2
+
 let constr_loc = function
   | CRef (Ident (loc,_),_) -> loc
   | CRef (Qualid (loc,_),_) -> loc
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ad159bb60..9a6f8b22c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -142,7 +142,7 @@ let insert_pat_alias loc p = function
 (* conversion of references                                           *)
 
 let extern_evar loc n l =
-  if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
+(*  if !print_evar_arguments then*) CEvar (loc,n,l) (*else CEvar (loc,n,None)*)
 
 (** We allow customization of the global_reference printer.
     For instance, in the debugger the tables of global references
@@ -674,7 +674,7 @@ let rec extern inctx scopes vars r =
   | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None, None)
 
   | GEvar (loc,n,l) ->
-      extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
+      extern_evar loc n (Option.map (List.map (on_snd (extern false scopes vars))) l)
 
   | GPatVar (loc,n) ->
       if !print_meta_as_hole then CHole (loc, None, None) else CPatVar (loc,n)
@@ -988,7 +988,7 @@ let extern_glob_type vars c =
 
 let loc = Loc.ghost (* for constr and pattern, locations are lost *)
 
-let extern_constr_gen goal_concl_style scopt env t =
+let extern_constr_gen goal_concl_style scopt env sigma t =
   (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
   (* i.e.: avoid using the names of goal/section/rel variables and the short *)
   (* names of global definitions of current module when computing names for *)
@@ -998,20 +998,20 @@ let extern_constr_gen goal_concl_style scopt env t =
   (* consideration; see namegen.ml for further details *)
   let avoid = if goal_concl_style then ids_of_context env else [] in
   let rel_env_names = names_of_rel_context env in
-  let r = Detyping.detype goal_concl_style avoid rel_env_names t in
+  let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in
   let vars = vars_of_env env in
   extern false (scopt,[]) vars r
 
-let extern_constr_in_scope goal_concl_style scope env t =
-  extern_constr_gen goal_concl_style (Some scope) env t
+let extern_constr_in_scope goal_concl_style scope env sigma t =
+  extern_constr_gen goal_concl_style (Some scope) env sigma t
 
-let extern_constr goal_concl_style env t =
-  extern_constr_gen goal_concl_style None env t
+let extern_constr goal_concl_style env sigma t =
+  extern_constr_gen goal_concl_style None env sigma t
 
-let extern_type goal_concl_style env t =
+let extern_type goal_concl_style env sigma t =
   let avoid = if goal_concl_style then ids_of_context env else [] in
   let rel_env_names = names_of_rel_context env in
-  let r = Detyping.detype goal_concl_style avoid rel_env_names t in
+  let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in
   extern_glob_type (vars_of_env env) r
 
 let extern_sort s = extern_glob_sort (detype_sort s)
@@ -1023,10 +1023,14 @@ let any_any_branch =
   (* | _ => _ *)
   (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,None))
 
-let rec glob_of_pat env = function
+let rec glob_of_pat env sigma = function
   | PRef ref -> GRef (loc,ref,None)
   | PVar id -> GVar (loc,id)
-  | PEvar (n,l) -> GEvar (loc,n,Some (Array.map_to_list (glob_of_pat env) l))
+  | PEvar (evk,l) ->
+      let test id = function PVar id' -> Id.equal id id' | _ -> false in
+      let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
+      let id = Evd.evar_ident evk sigma in
+      GEvar (loc,id,Some (List.map (on_snd (glob_of_pat env sigma)) l))
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
@@ -1036,29 +1040,29 @@ let rec glob_of_pat env = function
       GVar (loc,id)
   | PMeta None -> GHole (loc,Evar_kinds.InternalHole, None)
   | PMeta (Some n) -> GPatVar (loc,(false,n))
-  | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef p,None),[glob_of_pat env c])
+  | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef p,None),[glob_of_pat env sigma c])
   | PApp (f,args) ->
-      GApp (loc,glob_of_pat env f,Array.map_to_list (glob_of_pat env) args)
+      GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
   | PSoApp (n,args) ->
       GApp (loc,GPatVar (loc,(true,n)),
-        List.map (glob_of_pat env) args)
+        List.map (glob_of_pat env sigma) args)
   | PProd (na,t,c) ->
-      GProd (loc,na,Explicit,glob_of_pat env t,glob_of_pat (na::env) c)
+      GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
   | PLetIn (na,t,c) ->
-      GLetIn (loc,na,glob_of_pat env t, glob_of_pat (na::env) c)
+      GLetIn (loc,na,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
   | PLambda (na,t,c) ->
-      GLambda (loc,na,Explicit,glob_of_pat env t, glob_of_pat (na::env) c)
+      GLambda (loc,na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
   | PIf (c,b1,b2) ->
-      GIf (loc, glob_of_pat env c, (Anonymous,None),
-           glob_of_pat env b1, glob_of_pat env b2)
+      GIf (loc, glob_of_pat env sigma c, (Anonymous,None),
+           glob_of_pat env sigma b1, glob_of_pat env sigma b2)
   | PCase ({cip_style=LetStyle; cip_ind_args=None},PMeta None,tm,[(0,n,b)]) ->
-      let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env b) in
-      GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env tm,b)
+      let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in
+      GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env sigma tm,b)
   | PCase (info,p,tm,bl) ->
       let mat = match bl, info.cip_ind with
 	| [], _ -> []
 	| _, Some ind ->
-	  let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env c)) bl in
+	  let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in
 	  simple_cases_matrix_of_branches ind bl'
 	| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive")
       in
@@ -1067,18 +1071,18 @@ let rec glob_of_pat env = function
       let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with
 	| PMeta None, _, _ -> (Anonymous,None),None
 	| _, Some ind, Some nargs ->
-	  return_type_of_predicate ind nargs (glob_of_pat env p)
+	  return_type_of_predicate ind nargs (glob_of_pat env sigma p)
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
       in
-      GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat)
-  | PFix f -> Detyping.detype false [] env (mkFix f)
-  | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
+      GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
+  | PFix f -> Detyping.detype false [] env sigma (mkFix f)
+  | PCoFix c -> Detyping.detype false [] env sigma (mkCoFix c)
   | PSort s -> GSort (loc,s)
 
-let extern_constr_pattern env pat =
-  extern true (None,[]) Id.Set.empty (glob_of_pat env pat)
+let extern_constr_pattern env sigma pat =
+  extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
 
-let extern_rel_context where env sign =
-  let a = detype_rel_context where [] (names_of_rel_context env) sign in
+let extern_rel_context where env sigma sign =
+  let a = detype_rel_context where [] (names_of_rel_context env) sigma sign in
   let vars = vars_of_env env in
   pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index e1acb4502..a994d8693 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -26,17 +26,18 @@ open Misctypes
 val extern_cases_pattern : Id.Set.t -> cases_pattern -> cases_pattern_expr
 val extern_glob_constr : Id.Set.t -> glob_constr -> constr_expr
 val extern_glob_type : Id.Set.t -> glob_constr -> constr_expr
-val extern_constr_pattern : names_context -> constr_pattern -> constr_expr
+val extern_constr_pattern : names_context -> Evd.evar_map ->
+  constr_pattern -> constr_expr
 
 (** If [b=true] in [extern_constr b env c] then the variables in the first
    level of quantification clashing with the variables in [env] are renamed *)
 
-val extern_constr : bool -> env -> constr -> constr_expr
-val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
+val extern_constr : bool -> env -> Evd.evar_map -> constr -> constr_expr
+val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
-val extern_type : bool -> env -> types -> constr_expr
+val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : sorts -> glob_sort
-val extern_rel_context : constr option -> env ->
+val extern_rel_context : constr option -> env -> Evd.evar_map ->
   rel_context -> local_binder list
 
 (** Printing options *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d34c43d3d..ff96340cd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1581,10 +1581,12 @@ let internalize globalenv env allow_patvar lvar c =
 	GHole (loc, k, solve)
     | CPatVar (loc, n) when allow_patvar ->
 	GPatVar (loc, n)
+    | CPatVar (loc, (false,n)) ->
+	GEvar (loc, n, None)
     | CPatVar (loc, _) ->
-	raise (InternalizationError (loc,IllegalMetavariable))
+        raise (InternalizationError (loc,IllegalMetavariable))
     | CEvar (loc, n, l) ->
-	GEvar (loc, n, Option.map (List.map (intern env)) l)
+	GEvar (loc, n, Option.map (List.map (on_snd (intern env))) l)
     | CSort (loc, s) ->
 	GSort(loc,s)
     | CCast (loc, c1, c2) ->
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 9461cebb0..1aac1c53d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -356,7 +356,7 @@ let notation_constr_of_glob_constr nenv a =
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
 let notation_constr_of_constr avoiding t =
-  let t = Detyping.detype false avoiding [] t in
+  let t = Detyping.detype false avoiding [] Evd.empty t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;
     ninterp_rec_vars = Id.Map.empty;
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 272e6c8d1..33c21eea5 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -108,7 +108,7 @@ let constr_key c =
 let revert_reserved_type t =
   try
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
-    let t = Detyping.detype false [] [] t in
+    let t = Detyping.detype false [] [] Evd.empty t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
     let filter _ pat =