Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

1 files changed, 16 insertions, 2 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index d66b77b5..978f33b6 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -17,6 +17,7 @@
 open Util
 open Names
 open Term
+open Constr
 open Environ
 open EConstr
 open Vars
@@ -28,6 +29,18 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
+(** General evar naming using intro patterns  *)
+type intro_pattern_naming_expr =
+  | IntroIdentifier of Id.t
+  | IntroFresh of Id.t
+  | IntroAnonymous
+
+let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
+| IntroAnonymous, IntroAnonymous -> true
+| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
+| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
+| _ -> false
+
 (**********************************************************************)
 (* Conventional names *)
 
@@ -124,8 +137,9 @@ let lowercase_first_char id = (* First character of a constr *)
         s ^ Unicode.lowercase_first_char s'
 
 let sort_hdchar = function
-  | Prop(_) -> "P"
-  | Type(_) -> "T"
+  | Prop -> "P"
+  | Set -> "S"
+  | Type _ -> "T"
 
 let hdchar env sigma c =
   let rec hdrec k c =