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.
---
 engine/eConstr.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 657285de2d..7d4d17c630 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
-- 
cgit v1.2.3