Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.

9 files changed, 102 insertions, 89 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 657285de2..7d4d17c63 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -131,6 +131,8 @@ let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false
 let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false
 let isVarId sigma id c =
   match kind sigma c with Var id' -> Id.equal id id' | _ -> false
+let isRelN sigma n c =
+  match kind sigma c with Rel n' -> Int.equal n n' | _ -> false
 
 let destRel sigma c = match kind sigma c with
 | Rel p -> p
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index d6b2113d2..83536d6f8 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -114,6 +114,7 @@ val isCase : Evd.evar_map -> t -> bool
 val isProj : Evd.evar_map -> t -> bool
 val isArity : Evd.evar_map -> t -> bool
 val isVarId  : Evd.evar_map -> Id.t -> t -> bool
+val isRelN : Evd.evar_map -> int -> t -> bool
 
 val destRel : Evd.evar_map -> t -> int
 val destMeta : Evd.evar_map -> t -> metavariable
diff --git a/engine/engine.mllib b/engine/engine.mllib
index c78f37a85..1b670d366 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,10 +1,10 @@
 Logic_monad
-Namegen
 Universes
 UState
 Evd
 Sigma
 EConstr
+Namegen
 Termops
 Proofview_monad
 Evarutil
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index e94fd72f1..ce6d06f23 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -326,7 +326,7 @@ let push_var id (n, s) =
   let s = Int.Map.add n (EConstr.mkVar id) s in
   (succ n, s)
 
-let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
+let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) =
   let open EConstr in
   let open Vars in
   let map_decl f d =
@@ -354,7 +354,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
     else
       (** id_of_name_using_hdchar only depends on the rel context which is empty
           here *)
-      next_ident_away (id_of_name_using_hdchar empty_env (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) na) avoid
+      next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid
   in
   match extract_if_neq id na with
   | Some id0 when not (is_section_variable id0) ->
@@ -375,7 +375,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
       let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (subst2 subst vsubst) in
       (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc)
 
-let push_rel_context_to_named_context env typ =
+let push_rel_context_to_named_context env sigma typ =
   (* compute the instances relative to the named context and rel_context *)
   let open Context.Named.Declaration in
   let open EConstr in
@@ -390,7 +390,7 @@ let push_rel_context_to_named_context env typ =
     (* with vars of the rel context *)
     (* We do keep the instances corresponding to local definition (see above) *)
     let (subst, vsubst, _, env) =
-      Context.Rel.fold_outside push_rel_decl_to_named_context
+      Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
         (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in
     (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
 
@@ -452,7 +452,7 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-  let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
+  let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env (Sigma.to_evar_map evd) typ in
   let map c = subst2 subst vsubst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
   let instance =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 2da4f8043..da49d4e11 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -216,9 +216,9 @@ type ext_named_context =
   Id.Set.t * named_context
 
 val push_rel_decl_to_named_context :
-  rel_declaration -> ext_named_context -> ext_named_context
+  evar_map -> rel_declaration -> ext_named_context -> ext_named_context
 
-val push_rel_context_to_named_context : Environ.env -> types ->
+val push_rel_context_to_named_context : Environ.env -> evar_map -> types ->
   named_context_val * types * constr list * csubst * (identifier*constr) list
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
diff --git a/engine/namegen.ml b/engine/namegen.ml
index e56ec2877..7b7302957 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -15,12 +15,13 @@
 open Util
 open Names
 open Term
+open Environ
+open EConstr
 open Vars
 open Nametab
 open Nameops
 open Libnames
 open Globnames
-open Environ
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -84,13 +85,20 @@ let is_section_variable id =
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
-let head_name c = (* Find the head constant of a constr if any *)
+let global_of_constr = function
+| Const (c, _) -> ConstRef c
+| Ind (i, _) -> IndRef i
+| Construct (c, _) -> ConstructRef c
+| Var id -> VarRef id
+| _ -> assert false
+
+let head_name sigma c = (* Find the head constant of a constr if any *)
   let rec hdrec c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
     | Cast (c,_,_) | App (c,_) -> hdrec c
     | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
-    | Const _ | Ind _ | Construct _ | Var _ ->
+    | Const _ | Ind _ | Construct _ | Var _ as c ->
 	Some (basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
 	Some (match lna.(i) with Name id -> id | _ -> assert false)
@@ -105,9 +113,9 @@ let sort_hdchar = function
   | Prop(_) -> "P"
   | Type(_) -> "T"
 
-let hdchar env c =
+let hdchar env sigma c =
   let rec hdrec k c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
     | Cast (c,_,_) | App (c,_) -> hdrec k c
     | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
@@ -119,7 +127,7 @@ let hdchar env c =
     | Rel n ->
 	(if n<=k then "p" (* the initial term is flexible product/function *)
 	 else
-	   try match Environ.lookup_rel (n-k) env with
+	   try match lookup_rel (n-k) env with
 	     | LocalAssum (Name id,_)   | LocalDef (Name id,_,_) -> lowercase_first_char id
 	     | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
 	   with Not_found -> "y")
@@ -131,41 +139,41 @@ let hdchar env c =
   in
   hdrec 0 c
 
-let id_of_name_using_hdchar env a = function
-  | Anonymous -> Id.of_string (hdchar env a)
+let id_of_name_using_hdchar env sigma a = function
+  | Anonymous -> Id.of_string (hdchar env sigma a)
   | Name id   -> id
 
-let named_hd env a = function
-  | Anonymous -> Name (Id.of_string (hdchar env a))
+let named_hd env sigma a = function
+  | Anonymous -> Name (Id.of_string (hdchar env sigma a))
   | x         -> x
 
-let mkProd_name   env (n,a,b) = mkProd (named_hd env a n, a, b)
-let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
+let mkProd_name   env sigma (n,a,b) = mkProd (named_hd env sigma a n, a, b)
+let mkLambda_name env sigma (n,a,b) = mkLambda (named_hd env sigma a n, a, b)
 
 let lambda_name = mkLambda_name
 let prod_name = mkProd_name
 
-let prod_create   env (a,b) = mkProd (named_hd env a Anonymous, a, b)
-let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous, a, b)
+let prod_create   env sigma (a,b) = mkProd (named_hd env sigma a Anonymous, a, b)
+let lambda_create env sigma (a,b) =  mkLambda (named_hd env sigma a Anonymous, a, b)
 
-let name_assumption env = function
-    | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
-    | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
+let name_assumption env sigma = function
+    | LocalAssum (na,t) -> LocalAssum (named_hd env sigma t na, t)
+    | LocalDef (na,c,t) -> LocalDef (named_hd env sigma c na, c, t)
 
-let name_context env hyps =
+let name_context env sigma hyps =
   snd
     (List.fold_left
        (fun (env,hyps) d ->
-	  let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+	  let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps))
        (env,[]) (List.rev hyps))
 
-let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
-let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
+let mkProd_or_LetIn_name env sigma b d = mkProd_or_LetIn (name_assumption env sigma d) b
+let mkLambda_or_LetIn_name env sigma b d = mkLambda_or_LetIn (name_assumption env sigma d) b
 
-let it_mkProd_or_LetIn_name env b hyps =
-  it_mkProd_or_LetIn b (name_context env hyps)
-let it_mkLambda_or_LetIn_name env b hyps =
-  it_mkLambda_or_LetIn b (name_context env hyps)
+let it_mkProd_or_LetIn_name env sigma b hyps =
+  it_mkProd_or_LetIn b (name_context env sigma hyps)
+let it_mkLambda_or_LetIn_name env sigma b hyps =
+  it_mkLambda_or_LetIn b (name_context env sigma hyps)
 
 (**********************************************************************)
 (* Fresh names *)
@@ -185,10 +193,10 @@ let restart_subscript id =
      *** make_ident id (Some 0) *** but compatibility would be lost... *)
     forget_subscript id
 
-let visible_ids (nenv, c) =
+let visible_ids sigma (nenv, c) =
   let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in
-  let rec visible_ids n c = match kind_of_term c with
-  | Const _ | Ind _ | Construct _ | Var _ ->
+  let rec visible_ids n c = match EConstr.kind sigma c with
+  | Const _ | Ind _ | Construct _ | Var _ as c ->
     let (gseen, vseen, ids) = !accu in
     let g = global_of_constr c in
     if not (Refset_env.mem g gseen) then
@@ -218,7 +226,7 @@ let visible_ids (nenv, c) =
       | _ -> ids
       in
       accu := (gseen, vseen, ids)
-  | _ -> Constr.iter_with_binders succ visible_ids n c
+  | _ -> EConstr.iter_with_binders sigma succ visible_ids n c
   in
   let () = visible_ids 1 c in
   let (_, _, ids) = !accu in
@@ -228,9 +236,9 @@ let visible_ids (nenv, c) =
 
 (* 1- Looks for a fresh name for printing in cases pattern *)
 
-let next_name_away_in_cases_pattern env_t na avoid =
+let next_name_away_in_cases_pattern sigma env_t na avoid =
   let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
-  let visible = visible_ids env_t in
+  let visible = visible_ids sigma env_t in
   let bad id = Id.List.mem id avoid || is_constructor id
                                     || Id.Set.mem id visible in
   next_ident_away_from id bad
@@ -292,7 +300,7 @@ let next_name_away_with_default_using_types default na avoid t =
 
 let next_name_away = next_name_away_with_default default_non_dependent_string
 
-let make_all_name_different env =
+let make_all_name_different env sigma =
   (** FIXME: this is inefficient, but only used in printing *)
   let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in
   let sign = named_context_val env in
@@ -300,7 +308,7 @@ let make_all_name_different env =
   let env0 = reset_with_named_context sign env in
   Context.Rel.fold_outside
     (fun decl newenv ->
-       let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in
+       let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
        push_rel (RelDecl.set_name (Name id) decl) newenv)
@@ -311,12 +319,12 @@ let make_all_name_different env =
    looks for name of same base with lower available subscript beyond current
    subscript *)
 
-let next_ident_away_for_default_printing env_t id avoid =
-  let visible = visible_ids env_t in
+let next_ident_away_for_default_printing sigma env_t id avoid =
+  let visible = visible_ids sigma env_t in
   let bad id = Id.List.mem id avoid || Id.Set.mem id visible in
   next_ident_away_from id bad
 
-let next_name_away_for_default_printing env_t na avoid =
+let next_name_away_for_default_printing sigma env_t na avoid =
   let id = match na with
   | Name id   -> id
   | Anonymous ->
@@ -324,7 +332,7 @@ let next_name_away_for_default_printing env_t na avoid =
       (* taken into account by the function compute_displayed_name_in; *)
       (* just in case, invent a valid name *)
       default_non_dependent_ident in
-  next_ident_away_for_default_printing env_t id avoid
+  next_ident_away_for_default_printing sigma env_t id avoid
 
 (**********************************************************************)
 (* Displaying terms avoiding bound variables clashes *)
@@ -349,45 +357,45 @@ type renaming_flags =
   | RenamingForGoal
   | RenamingElsewhereFor of (Name.t list * constr)
 
-let next_name_for_display flags =
+let next_name_for_display sigma flags =
   match flags with
-  | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t
+  | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern sigma env_t
   | RenamingForGoal -> next_name_away_in_goal
-  | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
+  | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
-let compute_displayed_name_in flags avoid na c =
+let compute_displayed_name_in sigma flags avoid na c =
   match na with
-  | Anonymous when noccurn 1 c ->
+  | Anonymous when noccurn sigma 1 c ->
     (Anonymous,avoid)
   | _ ->
-    let fresh_id = next_name_for_display flags na avoid in
-    let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
+    let fresh_id = next_name_for_display sigma flags na avoid in
+    let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in
     (idopt, fresh_id::avoid)
 
-let compute_and_force_displayed_name_in flags avoid na c =
+let compute_and_force_displayed_name_in sigma flags avoid na c =
   match na with
-  | Anonymous when noccurn 1 c ->
+  | Anonymous when noccurn sigma 1 c ->
     (Anonymous,avoid)
   | _ ->
-    let fresh_id = next_name_for_display flags na avoid in
+    let fresh_id = next_name_for_display sigma flags na avoid in
     (Name fresh_id, fresh_id::avoid)
 
-let compute_displayed_let_name_in flags avoid na c =
-  let fresh_id = next_name_for_display flags na avoid in
+let compute_displayed_let_name_in sigma flags avoid na c =
+  let fresh_id = next_name_for_display sigma flags na avoid in
   (Name fresh_id, fresh_id::avoid)
 
-let rename_bound_vars_as_displayed avoid env c =
+let rename_bound_vars_as_displayed sigma avoid env c =
   let rec rename avoid env c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Prod (na,c1,c2)  ->
 	let na',avoid' =
-          compute_displayed_name_in
+          compute_displayed_name_in sigma
             (RenamingElsewhereFor (env,c2)) avoid na c2 in
 	mkProd (na', c1, rename avoid' (na' :: env) c2)
     | LetIn (na,c1,t,c2) ->
 	let na',avoid' =
-          compute_displayed_let_name_in
+          compute_displayed_let_name_in sigma
             (RenamingElsewhereFor (env,c2)) avoid na c2 in
 	mkLetIn (na',c1,t, rename avoid' (na' :: env) c2)
     | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 33ce9a34d..058b1c228 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -11,6 +11,8 @@
 open Names
 open Term
 open Environ
+open Evd
+open EConstr
 
 (*********************************************************************
    Conventional default names *)
@@ -26,27 +28,27 @@ val default_dependent_ident : Id.t     (* "x" *)
 
 val lowercase_first_char : Id.t -> string
 val sort_hdchar : sorts -> string
-val hdchar : env -> types -> string
-val id_of_name_using_hdchar : env -> types -> Name.t -> Id.t
-val named_hd : env -> types -> Name.t -> Name.t
-val head_name : types -> Id.t option
+val hdchar : env -> evar_map -> types -> string
+val id_of_name_using_hdchar : env -> evar_map -> types -> Name.t -> Id.t
+val named_hd : env -> evar_map -> types -> Name.t -> Name.t
+val head_name : evar_map -> types -> Id.t option
 
-val mkProd_name : env -> Name.t * types * types -> types
-val mkLambda_name : env -> Name.t * types * constr -> constr
+val mkProd_name : env -> evar_map -> Name.t * types * types -> types
+val mkLambda_name : env -> evar_map -> Name.t * types * constr -> constr
 
 (** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
-val prod_name : env -> Name.t * types * types -> types
-val lambda_name : env -> Name.t * types * constr -> constr
+val prod_name : env -> evar_map -> Name.t * types * types -> types
+val lambda_name : env -> evar_map -> Name.t * types * constr -> constr
 
-val prod_create : env -> types * types -> constr
-val lambda_create : env -> types * constr -> constr
-val name_assumption : env -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
-val name_context : env -> Context.Rel.t -> Context.Rel.t
+val prod_create : env -> evar_map -> types * types -> constr
+val lambda_create : env -> evar_map -> types * constr -> constr
+val name_assumption : env -> evar_map -> rel_declaration -> rel_declaration
+val name_context : env -> evar_map -> rel_context -> rel_context
 
-val mkProd_or_LetIn_name : env -> types -> Context.Rel.Declaration.t -> types
-val mkLambda_or_LetIn_name : env -> constr -> Context.Rel.Declaration.t -> constr
-val it_mkProd_or_LetIn_name   : env -> types -> Context.Rel.t -> types
-val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr
+val mkProd_or_LetIn_name : env -> evar_map -> types -> rel_declaration -> types
+val mkLambda_or_LetIn_name : env -> evar_map -> constr -> rel_declaration -> constr
+val it_mkProd_or_LetIn_name   : env -> evar_map -> types -> rel_context -> types
+val it_mkLambda_or_LetIn_name : env -> evar_map -> constr -> rel_context -> constr
 
 (*********************************************************************
    Fresh names *)
@@ -98,16 +100,16 @@ type renaming_flags =
   | RenamingForGoal (** avoid all globals (as in intro) *)
   | RenamingElsewhereFor of (Name.t list * constr)
 
-val make_all_name_different : env -> env
+val make_all_name_different : env -> evar_map -> env
 
 val compute_displayed_name_in :
-  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val compute_and_force_displayed_name_in :
-  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val compute_displayed_let_name_in :
-  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val rename_bound_vars_as_displayed :
-  Id.t list -> Name.t list -> types -> types
+  evar_map -> Id.t list -> Name.t list -> types -> types
 
 (**********************************************************************)
 (* Naming strategy for arguments in Prop when eliminating inductive types *)
diff --git a/engine/termops.ml b/engine/termops.ml
index ff1a0d9de..d8e712abc 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -115,7 +115,7 @@ let pr_evar_suggested_name evk sigma =
   | _,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
+      Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous
   in
   let names = EvMap.mapi base_id (undefined_map sigma) in
   let id = EvMap.find evk names in
@@ -316,7 +316,7 @@ let print_env_short env =
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
     str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
 
-let pr_evar_constraints pbs =
+let pr_evar_constraints sigma pbs =
   let pr_evconstr (pbty, env, t1, t2) =
     let env =
       (** We currently allow evar instances to refer to anonymous de
@@ -326,10 +326,10 @@ let pr_evar_constraints pbs =
           stop depending on anonymous variables, they can be used to
           indicate independency. Also, this depends on a strategy for
           naming/renaming. *)
-      Namegen.make_all_name_different env
+      Namegen.make_all_name_different env sigma
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      print_constr_env env Evd.empty (EConstr.of_constr t1) ++ spc () ++
+      print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
@@ -346,7 +346,7 @@ let pr_evar_map_gen with_univs pr_evars sigma =
     if List.is_empty conv_pbs then mt ()
     else
     str "CONSTRAINTS:" ++ brk (0, 1) ++
-      pr_evar_constraints conv_pbs ++ fnl ()
+      pr_evar_constraints sigma conv_pbs ++ fnl ()
   and metas =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
diff --git a/engine/termops.mli b/engine/termops.mli
index 512bb05ff..0dd5d96fb 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -288,7 +288,7 @@ val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
 val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
+val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.std_ppcmds
 val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
 val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
   evar_map -> Pp.std_ppcmds