From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Nov 2016 00:41:31 +0100
Subject: 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.
---
 library/impargs.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index 836568b890..a63264b669 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -228,10 +228,12 @@ let rec is_rigid_head t = match kind_of_term t with
 
 (* calcule la liste des arguments implicites *)
 
-let find_displayed_name_in all avoid na (_,b as envnames_b) =
+let find_displayed_name_in all avoid na (env, b) =
+  let b = EConstr.of_constr b in
+  let envnames_b = (env, b) in
   let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in flag avoid na b
-  else compute_displayed_name_in flag avoid na b
+  if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
+  else compute_displayed_name_in Evd.empty flag avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
-- 
cgit v1.2.3