From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 pretyping/namegen.mli | 68 ++++++++++++++++++++++++++++++++-------------------
 1 file changed, 43 insertions(+), 25 deletions(-)

(limited to 'pretyping/namegen.mli')

diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index db078026..f66bc6d8 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,23 +8,34 @@
 
 open Names
 open Term
+open Context
 open Environ
 
+(*********************************************************************
+   Conventional default names *)
+
+val default_prop_ident : Id.t          (* "H" *)
+val default_small_ident : Id.t         (* "H" *)
+val default_type_ident : Id.t          (* "X" *)
+val default_non_dependent_ident : Id.t (* "H" *)
+val default_dependent_ident : Id.t     (* "x" *)
+
 (*********************************************************************
    Generating "intuitive" names from their type *)
 
-val lowercase_first_char : identifier -> string
+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 -> identifier
-val named_hd : env -> types -> name -> name
+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 mkProd_name : env -> name * types * types -> types
-val mkLambda_name : env -> name * types * constr -> constr
+val mkProd_name : env -> Name.t * types * types -> types
+val mkLambda_name : env -> Name.t * types * constr -> constr
 
 (** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
-val prod_name : env -> name * types * types -> types
-val lambda_name : env -> name * types * constr -> constr
+val prod_name : env -> Name.t * types * types -> types
+val lambda_name : env -> Name.t * types * constr -> constr
 
 val prod_create : env -> types * types -> constr
 val lambda_create : env -> types * constr -> constr
@@ -40,45 +51,52 @@ val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
    Fresh names *)
 
 (** Avoid clashing with a name satisfying some predicate *)
-val next_ident_away_from : identifier -> (identifier -> bool) -> identifier
+val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t
 
 (** Avoid clashing with a name of the given list *)
-val next_ident_away : identifier -> identifier list -> identifier
+val next_ident_away : Id.t -> Id.t list -> Id.t
 
 (** Avoid clashing with a name already used in current module *)
-val next_ident_away_in_goal : identifier -> identifier list -> identifier
+val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
 
 (** Avoid clashing with a name already used in current module 
    but tolerate overwriting section variables, as in goals *)
-val next_global_ident_away : identifier -> identifier list -> identifier
+val next_global_ident_away : Id.t -> Id.t list -> Id.t
 
 (** Avoid clashing with a constructor name already used in current module *)
-val next_name_away_in_cases_pattern : name -> identifier list -> identifier
+val next_name_away_in_cases_pattern : (Termops.names_context * constr) -> Name.t -> Id.t list -> Id.t
 
-val next_name_away  : name -> identifier list -> identifier (** default is "H" *)
-val next_name_away_with_default : string -> name -> identifier list ->
-  identifier
+(** Default is [default_non_dependent_ident] *)
+val next_name_away  : Name.t -> Id.t list -> Id.t
 
-val next_name_away_with_default_using_types : string -> name ->
-  identifier list -> types -> identifier
+val next_name_away_with_default : string -> Name.t -> Id.t list ->
+  Id.t
 
-val set_reserved_typed_name : (types -> name) -> unit
+val next_name_away_with_default_using_types : string -> Name.t ->
+  Id.t list -> types -> Id.t
+
+val set_reserved_typed_name : (types -> Name.t) -> unit
 
 (*********************************************************************
    Making name distinct for displaying *)
 
 type renaming_flags =
-  | RenamingForCasesPattern (** avoid only global constructors *)
+  | RenamingForCasesPattern of (Name.t list * constr) (** avoid only global constructors *)
   | RenamingForGoal (** avoid all globals (as in intro) *)
-  | RenamingElsewhereFor of (name list * constr)
+  | RenamingElsewhereFor of (Name.t list * constr)
 
 val make_all_name_different : env -> env
 
 val compute_displayed_name_in :
-  renaming_flags -> identifier list -> name -> constr -> name * identifier list
+  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val compute_and_force_displayed_name_in :
-  renaming_flags -> identifier list -> name -> constr -> name * identifier list
+  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val compute_displayed_let_name_in :
-  renaming_flags -> identifier list -> name -> constr -> name * identifier list
+  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val rename_bound_vars_as_displayed :
-  identifier list -> name list -> types -> types
+  Id.t list -> Name.t list -> types -> types
+
+(**********************************************************************)
+(* Naming strategy for arguments in Prop when eliminating inductive types *)
+
+val use_h_based_elimination_names : unit -> bool
-- 
cgit v1.2.3