diff options
84 files changed, 378 insertions, 344 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index e9dae6421..28faa2ce6 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -109,7 +109,7 @@ let rec constr_expr_eq e1 e2 = List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) -> - name_eq na1 na2 && + Name.equal na1 na2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) -> @@ -132,14 +132,14 @@ let rec constr_expr_eq e1 e2 = List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 | CLetTuple (_, n1, (m1, e1), t1, b1), CLetTuple (_, n2, (m2, e2), t2, b2) -> - List.equal (eq_located name_eq) n1 n2 && - Option.equal (eq_located name_eq) m1 m2 && + List.equal (eq_located Name.equal) n1 n2 && + Option.equal (eq_located Name.equal) m1 m2 && Option.equal constr_expr_eq e1 e2 && constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CIf (_, e1, (n1, r1), t1, f1), CIf (_, e2, (n2, r2), t2, f2) -> constr_expr_eq e1 e2 && - Option.equal (eq_located name_eq) n1 n2 && + Option.equal (eq_located Name.equal) n1 n2 && Option.equal constr_expr_eq r1 r2 && constr_expr_eq t1 t2 && constr_expr_eq f1 f2 @@ -176,7 +176,7 @@ and args_eq (a1,e1) (a2,e2) = and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) = constr_expr_eq e1 e2 && - Option.equal (eq_located name_eq) n1 n2 && + Option.equal (eq_located Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq (_, p1, e1) (_, p2, e2) = @@ -185,7 +185,7 @@ and branch_expr_eq (_, p1, e1) (_, p2, e2) = and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) = (** Don't care about the [binder_kind] *) - List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2 + List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) = (eq_located Id.equal id1 id2) && @@ -210,10 +210,10 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with and local_binder_eq l1 l2 = match l1, l2 with | LocalRawDef (n1, e1), LocalRawDef (n2, e2) -> - eq_located name_eq n1 n2 && constr_expr_eq e1 e2 + eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 | LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) -> (** Don't care about the [binder_kind] *) - List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2 + List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 49dea9f31..d857a5b60 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -48,9 +48,9 @@ val mkIdentC : Id.t -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr -val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr -val mkLetInC : name located * constr_expr * constr_expr -> constr_expr -val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr +val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr +val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr +val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr @@ -69,17 +69,17 @@ val coerce_reference_to_id : reference -> Id.t val coerce_to_id : constr_expr -> Id.t located (** Destruct terms of the form [CRef (Ident _)]. *) -val coerce_to_name : constr_expr -> name located +val coerce_to_name : constr_expr -> Name.t located (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *) (** {6 Binder manipulation} *) val default_binder_kind : binder_kind -val names_of_local_binders : local_binder list -> name located list +val names_of_local_binders : local_binder list -> Name.t located list (** Retrieve a list of binding names from a list of binders. *) -val names_of_local_assums : local_binder list -> name located list +val names_of_local_assums : local_binder list -> Name.t located list (** Same as [names_of_local_binders], but does not take the [let] bindings into account. *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8d44bc531..a4a74059e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -66,7 +66,7 @@ type var_internalization_data = type internalization_env = (var_internalization_data) Id.Map.t -type glob_binder = (name * binding_kind * glob_constr option * glob_constr) +type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) let interning_grammar = ref false diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 0e4d0c651..83cc1dcad 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -70,7 +70,7 @@ val compute_internalization_env : env -> var_internalization_type -> type ltac_sign = Id.t list * unbound_ltac_var_map -type glob_binder = (name * binding_kind * glob_constr option * glob_constr) +type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) (** {6 Internalization performs interpretation of global names and notations } *) @@ -148,9 +148,9 @@ val interp_reference : ltac_sign -> reference -> glob_constr (** Interpret binders *) -val interp_binder : evar_map -> env -> name -> constr_expr -> types +val interp_binder : evar_map -> env -> Name.t -> constr_expr -> types -val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types +val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types (** Interpret contexts: returns extended env and context *) diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 2c5ad7408..66be2ae5a 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -34,23 +34,23 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t -> Id.t list -> Id.t list val free_vars_of_binders : - ?bound:Id.Set.t -> Names.Id.t list -> local_binder list -> Id.Set.t * Names.Id.t list + ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list (** Returns the generalizable free ids in left-to-right order with the location of their first occurence *) val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t -> - glob_constr -> (Names.Id.t * Loc.t) list + glob_constr -> (Id.t * Loc.t) list -val make_fresh : Names.Id.Set.t -> Environ.env -> Id.t -> Id.t +val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Names.Id.Set.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> - Constrexpr.constr_expr * Names.Id.Set.t + Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) -> + Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Names.Id.Set.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> - Constrexpr.constr_expr * Names.Id.Set.t) -> + (Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) -> + Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t diff --git a/interp/notation.mli b/interp/notation.mli index 8b2d8aa0f..4a28ce255 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -95,7 +95,7 @@ val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) - val uninterp_prim_token : glob_constr -> scope_name * prim_token val uninterp_prim_token_cases_pattern : - cases_pattern -> name * scope_name * prim_token + cases_pattern -> Name.t * scope_name * prim_token val uninterp_prim_token_ind_pattern : inductive -> cases_pattern list -> scope_name * prim_token diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index a7e591383..9dcd24127 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -150,14 +150,14 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1) | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) - when name_eq na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> + when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) - when name_eq na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> + when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 | GHole _, GHole _ -> true | GSort (_,s1), GSort (_,s2) -> glob_sort_eq s1 s2 - | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when name_eq na1 na2 -> + | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> on_true_do (f b1 b2 & f c1 c2) add na1 | (GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 35c9a8e1c..d46657b5c 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -30,7 +30,7 @@ val eq_glob_constr : glob_constr -> glob_constr -> bool (** Re-interpret a notation as a [glob_constr], taking care of binders *) val glob_constr_of_notation_constr_with_binders : Loc.t -> - ('a -> name -> 'a * name) -> + ('a -> Name.t -> 'a * Name.t) -> ('a -> notation_constr -> glob_constr) -> 'a -> notation_constr -> glob_constr diff --git a/interp/reserve.mli b/interp/reserve.mli index 305480840..de72a410d 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -14,4 +14,4 @@ open Notation_term val declare_reserved_type : Id.t located list -> notation_constr -> unit val find_reserved_type : Id.t -> notation_constr -val anonymize_if_reserved : name -> glob_constr -> glob_constr +val anonymize_if_reserved : Name.t -> glob_constr -> glob_constr diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index a67e59185..68a65c5c7 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -67,16 +67,16 @@ type constr_expr = | CCoFix of Loc.t * Id.t located * cofix_expr list | CProdN of Loc.t * binder_expr list * constr_expr | CLambdaN of Loc.t * binder_expr list * constr_expr - | CLetIn of Loc.t * name located * constr_expr * constr_expr + | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr | CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list | CCases of Loc.t * case_style * constr_expr option * case_expr list * branch_expr list - | CLetTuple of Loc.t * name located list * (name located option * constr_expr option) * + | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) * constr_expr * constr_expr - | CIf of Loc.t * constr_expr * (name located option * constr_expr option) + | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option) * constr_expr * constr_expr | CHole of Loc.t * Evar_kinds.t option | CPatVar of Loc.t * (bool * patvar) @@ -89,13 +89,13 @@ type constr_expr = | CDelimiters of Loc.t * string * constr_expr and case_expr = - constr_expr * (name located option * cases_pattern_expr option) + constr_expr * (Name.t located option * cases_pattern_expr option) and branch_expr = Loc.t * cases_pattern_expr list located list * constr_expr and binder_expr = - name located list * binder_kind * constr_expr + Name.t located list * binder_kind * constr_expr and fix_expr = Id.t located * (Id.t located option * recursion_order_expr) * @@ -111,15 +111,15 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder = - | LocalRawDef of name located * constr_expr - | LocalRawAssum of name located list * binder_kind * constr_expr + | LocalRawDef of Name.t located * constr_expr + | LocalRawAssum of Name.t located list * binder_kind * constr_expr and constr_notation_substitution = constr_expr list * (** for constr subterms *) constr_expr list list * (** for recursive notations *) local_binder list list (** for binders subexpressions *) -type typeclass_constraint = name located * binding_kind * constr_expr +type typeclass_constraint = Name.t located * binding_kind * constr_expr and typeclass_context = typeclass_constraint list diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index 596f6b889..1541d4e46 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -19,7 +19,7 @@ type obligation_definition_status = Define of bool | Expand type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) - | BinderType of name + | BinderType of Name.t | QuestionMark of obligation_definition_status | CasesType | InternalHole diff --git a/intf/glob_term.mli b/intf/glob_term.mli index b8d6564a6..315b11517 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -23,8 +23,8 @@ open Misctypes locs here refers to the ident's location, not whole pat *) type cases_pattern = - | PatVar of Loc.t * name - | PatCstr of Loc.t * constructor * cases_pattern list * name + | PatVar of Loc.t * Name.t + | PatCstr of Loc.t * constructor * cases_pattern list * Name.t (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) type glob_constr = @@ -33,23 +33,23 @@ type glob_constr = | GEvar of Loc.t * existential_key * glob_constr list option | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list - | GLambda of Loc.t * name * binding_kind * glob_constr * glob_constr - | GProd of Loc.t * name * binding_kind * glob_constr * glob_constr - | GLetIn of Loc.t * name * glob_constr * glob_constr + | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GLetIn of Loc.t * Name.t * glob_constr * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) - | GLetTuple of Loc.t * name list * (name * glob_constr option) * + | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr - | GIf of Loc.t * glob_constr * (name * glob_constr option) * glob_constr * glob_constr + | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr | GRec of Loc.t * fix_kind * Id.t array * glob_decl list array * glob_constr array * glob_constr array | GSort of Loc.t * glob_sort | GHole of (Loc.t * Evar_kinds.t) | GCast of Loc.t * glob_constr * glob_constr cast_type -and glob_decl = name * binding_kind * glob_constr option * glob_constr +and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr and fix_recursion_order = | GStructRec @@ -61,7 +61,7 @@ and fix_kind = | GCoFix of int and predicate_pattern = - name * (Loc.t * inductive * name list) option + Name.t * (Loc.t * inductive * Name.t list) option (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) and tomatch_tuple = (glob_constr * predicate_pattern) diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 2b1286940..411b14f1f 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -27,19 +27,19 @@ type notation_constr = | NHole of Evar_kinds.t | NList of Id.t * Id.t * notation_constr * notation_constr * bool (** Part only in [glob_constr] *) - | NLambda of name * notation_constr * notation_constr - | NProd of name * notation_constr * notation_constr + | NLambda of Name.t * notation_constr * notation_constr + | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr - | NLetIn of name * notation_constr * notation_constr + | NLetIn of Name.t * notation_constr * notation_constr | NCases of case_style * notation_constr option * - (notation_constr * (name * (inductive * name list) option)) list * + (notation_constr * (Name.t * (inductive * Name.t list) option)) list * (cases_pattern list * notation_constr) list - | NLetTuple of name list * (name * notation_constr option) * + | NLetTuple of Name.t list * (Name.t * notation_constr option) * notation_constr * notation_constr - | NIf of notation_constr * (name * notation_constr option) * + | NIf of notation_constr * (Name.t * notation_constr option) * notation_constr * notation_constr | NRec of fix_kind * Id.t array * - (name * notation_constr option * notation_constr) list array * + (Name.t * notation_constr option * notation_constr) list array * notation_constr array * notation_constr array | NSort of glob_sort | NPatVar of patvar diff --git a/intf/pattern.mli b/intf/pattern.mli index 5c0dfbd5d..cec3fe87d 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -65,9 +65,9 @@ type constr_pattern = | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of patvar * constr_pattern list - | PLambda of name * constr_pattern * constr_pattern - | PProd of name * constr_pattern * constr_pattern - | PLetIn of name * constr_pattern * constr_pattern + | PLambda of Name.t * constr_pattern * constr_pattern + | PProd of Name.t * constr_pattern * constr_pattern + | PLetIn of Name.t * constr_pattern * constr_pattern | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 08063cf2a..1d7e9374f 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -79,8 +79,8 @@ type 'a match_pattern = (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = - | Hyp of name located * 'a match_pattern - | Def of name located * 'a match_pattern * 'a match_pattern + | Hyp of Name.t located * 'a match_pattern + | Def of Name.t located * 'a match_pattern * 'a match_pattern (* Type of a Match rule for Match Context and Match *) type ('a,'t) match_rule = @@ -112,9 +112,9 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacAssert of ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option * intro_pattern_expr located option * 'trm - | TacGeneralize of ('trm with_occurrences * name) list + | TacGeneralize of ('trm with_occurrences * Name.t) list | TacGeneralizeDep of 'trm - | TacLetTac of name * 'trm * 'nam clause_expr * letin_flag * + | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * intro_pattern_expr located option (* Derived basic tactics *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8088ba92a..52120d73c 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -19,7 +19,7 @@ open Libnames (** Vernac expressions, produced by the parser *) type lident = Id.t located -type lname = name located +type lname = Name.t located type lstring = string located type lreference = reference @@ -317,7 +317,7 @@ type vernac_expr = | VernacDeclareImplicits of locality_flag * reference or_by_notation * (explicitation * bool * bool) list list | VernacArguments of locality_flag * reference or_by_notation * - ((name * bool * (Loc.t * string) option * bool * bool) list) list * + ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list * int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list | VernacArgumentsScope of locality_flag * reference or_by_notation * diff --git a/kernel/closure.ml b/kernel/closure.ml index 934701f43..1630cff38 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -335,9 +335,9 @@ and fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs diff --git a/kernel/closure.mli b/kernel/closure.mli index d7a775fde..3a9603a37 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -111,9 +111,9 @@ type fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs @@ -157,7 +157,7 @@ val mk_atom : constr -> fconstr val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : - (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr + (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr (** Global and local constant cache *) type clos_infos diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 6b793ce2f..bc721dce3 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -136,7 +136,7 @@ let subst_const_body sub cb = { (* Hash-consing of [constant_body] *) let hcons_rel_decl ((n,oc,t) as d) = - let n' = hcons_name n + let n' = Name.hcons n and oc' = Option.smartmap hcons_constr oc and t' = hcons_types t in if n' == n && oc' == oc && t' == t then d else (n',oc',t') diff --git a/kernel/modops.ml b/kernel/modops.ml index e7afec2a0..e13586689 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -39,7 +39,7 @@ type signature_mismatch_error = | InductiveNumbersFieldExpected of int | InductiveParamsNumberField of int | RecordFieldExpected of bool - | RecordProjectionsExpected of name list + | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases | NoTypeConstraintExpected diff --git a/kernel/modops.mli b/kernel/modops.mli index c90425fd7..cfd839456 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -66,7 +66,7 @@ type signature_mismatch_error = | InductiveNumbersFieldExpected of int | InductiveParamsNumberField of int | RecordFieldExpected of bool - | RecordProjectionsExpected of name list + | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases | NoTypeConstraintExpected diff --git a/kernel/names.ml b/kernel/names.ml index c6f5f891c..12df0a3c8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -74,16 +74,46 @@ struct end + +module Name = +struct + type t = Name of Id.t | Anonymous + + let equal n1 n2 = match n1, n2 with + | Anonymous, Anonymous -> true + | Name id1, Name id2 -> String.equal id1 id2 + | _ -> false + + module Self_Hashcons = + struct + type _t = t + type t = _t + type u = Id.t -> Id.t + let hashcons hident = function + | Name id -> Name (hident id) + | n -> n + let equal n1 n2 = + n1 == n2 || + match (n1,n2) with + | (Name id1, Name id2) -> id1 == id2 + | (Anonymous,Anonymous) -> true + | _ -> false + let hash = Hashtbl.hash + end + + module Hname = Hashcons.Make(Self_Hashcons) + + let hcons = Hashcons.simple_hcons Hname.generate Id.hcons + +end + +type name = Name.t = Name of Id.t | Anonymous +(** Alias, to import constructors. *) + (** {6 Various types based on identifiers } *) -type name = Name of Id.t | Anonymous type variable = Id.t -let name_eq n1 n2 = match n1, n2 with -| Anonymous, Anonymous -> true -| Name id1, Name id2 -> String.equal id1 id2 -| _ -> false - type module_ident = Id.t module ModIdmap = Id.Map @@ -448,22 +478,6 @@ let eq_egr e1 e2 = match e1, e2 with (** {6 Hash-consing of name objects } *) -module Hname = Hashcons.Make( - struct - type t = name - type u = Id.t -> Id.t - let hashcons hident = function - | Name id -> Name (hident id) - | n -> n - let equal n1 n2 = - n1 == n2 || - match (n1,n2) with - | (Name id1, Name id2) -> id1 == id2 - | (Anonymous,Anonymous) -> true - | _ -> false - let hash = Hashtbl.hash - end) - module Hmod = Hashcons.Make( struct type t = module_path @@ -526,7 +540,6 @@ module Hconstruct = Hashcons.Make( let hash = Hashtbl.hash end) -let hcons_name = Hashcons.simple_hcons Hname.generate Id.hcons let hcons_mp = Hashcons.simple_hcons Hmod.generate (Dir_path.hcons,MBId.hcons,String.hcons) let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,Dir_path.hcons,String.hcons) @@ -631,3 +644,9 @@ let label_of_id = Label.of_id let eq_label = Label.equal (** / End of compatibility layer for [Label] *) + +(** Compatibility layer for [Name] *) + +let name_eq = Name.equal + +(** / End of compatibility layer for [Name] *) diff --git a/kernel/names.mli b/kernel/names.mli index 947b9e3fd..a51ac0ad8 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -55,14 +55,25 @@ sig end -(** {6 Various types based on identifiers } *) +module Name : +sig + type t = Name of Id.t | Anonymous + (** A name is either undefined, either an identifier. *) + + val equal : t -> t -> bool + (** Equality over names. *) + + val hcons : t -> t + (** Hashconsing over names. *) -type name = Name of Id.t | Anonymous +end + +(** {6 Type aliases} *) + +type name = Name.t = Name of Id.t | Anonymous type variable = Id.t type module_ident = Id.t -val name_eq : name -> name -> bool - (** {6 Directory paths = section names paths } *) module Dir_path : @@ -100,8 +111,6 @@ sig end -module ModIdmap : Map.S with type key = module_ident - (** {6 Names of structure elements } *) module Label : @@ -164,6 +173,8 @@ sig end +module ModIdmap : Map.S with type key = module_ident + (** {6 The module part of the kernel name } *) type module_path = @@ -290,7 +301,6 @@ val eq_egr : evaluable_global_reference -> evaluable_global_reference (** {6 Hash-consing } *) -val hcons_name : name -> name val hcons_con : constant -> constant val hcons_mind : mutual_inductive -> mutual_inductive val hcons_ind : inductive -> inductive @@ -439,3 +449,8 @@ val string_of_mbid : mod_bound_id -> string val debug_string_of_mbid : mod_bound_id -> string (** @deprecated Same as [MBId.debug_to_string]. *) + +(** {5 Names} *) + +val name_eq : name -> name -> bool +(** @deprecated Same as [Name.equal]. *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c15681b04..11ae7c863 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -198,7 +198,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 check (fun mib -> let nparamdecls = List.length mib.mind_params_ctxt in let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in - snd (List.chop nparamdecls names)) (List.equal name_eq) + snd (List.chop nparamdecls names)) (List.equal Name.equal) (fun x -> RecordProjectionsExpected x); end; (* we first check simple things *) diff --git a/kernel/term.ml b/kernel/term.ml index ced5c6fc5..9cb38e33d 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -95,7 +95,7 @@ let family_of_sort = function the same order (i.e. last argument first) *) type 'constr pexistential = existential_key * 'constr array type ('constr, 'types) prec_declaration = - name array * 'types array * 'constr array + Name.t array * 'types array * 'constr array type ('constr, 'types) pfixpoint = (int array * int) * ('constr, 'types) prec_declaration type ('constr, 'types) pcofixpoint = @@ -110,9 +110,9 @@ type ('constr, 'types) kind_of_term = | Evar of 'constr pexistential | Sort of sorts | Cast of 'constr * cast_kind * 'types - | Prod of name * 'types * 'types - | Lambda of name * 'types * 'constr - | LetIn of name * 'constr * 'types * 'constr + | Prod of Name.t * 'types * 'types + | Lambda of Name.t * 'types * 'constr + | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array | Const of constant | Ind of inductive @@ -126,7 +126,7 @@ type ('constr, 'types) kind_of_term = type constr = (constr,constr) kind_of_term type existential = existential_key * constr array -type rec_declaration = name array * constr array * constr array +type rec_declaration = Name.t array * constr array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -250,8 +250,8 @@ let kind_of_term c = c type ('constr, 'types) kind_of_type = | SortType of sorts | CastType of 'types * 'types - | ProdType of name * 'types * 'types - | LetInType of name * 'constr * 'types * 'types + | ProdType of Name.t * 'types * 'types + | LetInType of Name.t * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array let kind_of_type = function @@ -670,7 +670,7 @@ type types = constr type strategy = types option type named_declaration = Id.t * constr option * types -type rel_declaration = name * constr option * types +type rel_declaration = Name.t * constr option * types let map_named_declaration f (id, (v : strategy), ty) = (id, Option.map f v, f ty) let map_rel_declaration = map_named_declaration @@ -688,7 +688,7 @@ let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = Id.equal i1 i2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) = - name_eq n1 n2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2 + Name.equal n1 n2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2 (***************************************************************************) (* Type of local contexts (telescopes) *) @@ -1432,7 +1432,7 @@ let hcons_constr = hcons_construct, hcons_ind, hcons_con, - hcons_name, + Name.hcons, Id.hcons) let hcons_types = hcons_constr diff --git a/kernel/term.mli b/kernel/term.mli index 17c55f069..b20e0a1d0 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -103,7 +103,7 @@ type cast_kind = VMcast | DEFAULTcast | REVERTcast val mkCast : constr * cast_kind * constr -> constr (** Constructs the product [(x:t1)t2] *) -val mkProd : name * types * types -> types +val mkProd : Name.t * types * types -> types val mkNamedProd : Id.t -> types -> types -> types (** non-dependent product [t1 -> t2], an alias for @@ -113,11 +113,11 @@ val mkNamedProd : Id.t -> types -> types -> types val mkArrow : types -> types -> constr (** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *) -val mkLambda : name * types * constr -> constr +val mkLambda : Name.t * types * constr -> constr val mkNamedLambda : Id.t -> types -> constr -> constr (** Constructs the product [let x = t1 : t2 in t3] *) -val mkLetIn : name * constr * types * constr -> constr +val mkLetIn : Name.t * constr * types * constr -> constr val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr (** [mkApp (f,[| t_1; ...; t_n |]] constructs the application @@ -164,7 +164,7 @@ val mkCase : case_info * constr * constr * constr array -> constr where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) -type rec_declaration = name array * types array * constr array +type rec_declaration = Name.t array * types array * constr array type fixpoint = (int array * int) * rec_declaration val mkFix : fixpoint -> constr @@ -189,7 +189,7 @@ val mkCoFix : cofixpoint -> constr the same order (i.e. last argument first) *) type 'constr pexistential = existential_key * 'constr array type ('constr, 'types) prec_declaration = - name array * 'types array * 'constr array + Name.t array * 'types array * 'constr array type ('constr, 'types) pfixpoint = (int array * int) * ('constr, 'types) prec_declaration type ('constr, 'types) pcofixpoint = @@ -202,9 +202,9 @@ type ('constr, 'types) kind_of_term = | Evar of 'constr pexistential | Sort of sorts | Cast of 'constr * cast_kind * 'types - | Prod of name * 'types * 'types - | Lambda of name * 'types * 'constr - | LetIn of name * 'constr * 'types * 'constr + | Prod of Name.t * 'types * 'types + | Lambda of Name.t * 'types * 'constr + | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array | Const of constant | Ind of inductive @@ -223,8 +223,8 @@ val kind_of_term : constr -> (constr, types) kind_of_term type ('constr, 'types) kind_of_type = | SortType of sorts | CastType of 'types * 'types - | ProdType of name * 'types * 'types - | LetInType of name * 'constr * 'types * 'types + | ProdType of Name.t * 'types * 'types + | LetInType of Name.t * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array val kind_of_type : types -> (constr, types) kind_of_type @@ -281,13 +281,13 @@ val destSort : constr -> sorts val destCast : constr -> constr * cast_kind * constr (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) -val destProd : types -> name * types * types +val destProd : types -> Name.t * types * types (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) -val destLambda : constr -> name * types * constr +val destLambda : constr -> Name.t * types * constr (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) -val destLetIn : constr -> name * constr * types * constr +val destLetIn : constr -> Name.t * constr * types * constr (** Destructs an application *) val destApp : constr -> constr * constr array @@ -338,7 +338,7 @@ val destCoFix : constr -> cofixpoint purpose) *) type named_declaration = Id.t * constr option * types -type rel_declaration = name * constr option * types +type rel_declaration = Name.t * constr option * types val map_named_declaration : (constr -> constr) -> named_declaration -> named_declaration @@ -399,24 +399,24 @@ val appvectc : constr -> constr array -> constr (** [prodn n l b] = [forall (x_1:T_1)...(x_n:T_n), b] where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) -val prodn : int -> (name * constr) list -> constr -> constr +val prodn : int -> (Name.t * constr) list -> constr -> constr (** [compose_prod l b] @return [forall (x_1:T_1)...(x_n:T_n), b] where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [decompose_prod]. *) -val compose_prod : (name * constr) list -> constr -> constr +val compose_prod : (Name.t * constr) list -> constr -> constr (** [lamn n l b] @return [fun (x_1:T_1)...(x_n:T_n) => b] where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) -val lamn : int -> (name * constr) list -> constr -> constr +val lamn : int -> (Name.t * constr) list -> constr -> constr (** [compose_lam l b] @return [fun (x_1:T_1)...(x_n:T_n) => b] where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [it_destLam] *) -val compose_lam : (name * constr) list -> constr -> constr +val compose_lam : (Name.t * constr) list -> constr -> constr (** [to_lambda n l] @return [fun (x_1:T_1)...(x_n:T_n) => T] @@ -441,20 +441,20 @@ val it_mkProd_or_LetIn : types -> rel_context -> types (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *) -val decompose_prod : constr -> (name*constr) list * constr +val decompose_prod : constr -> (Name.t*constr) list * constr (** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *) -val decompose_lam : constr -> (name*constr) list * constr +val decompose_lam : constr -> (Name.t*constr) list * constr (** Given a positive integer n, transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *) -val decompose_prod_n : int -> constr -> (name * constr) list * constr +val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr (** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *) -val decompose_lam_n : int -> constr -> (name * constr) list * constr +val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr (** Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 6d4b42026..4c2799df8 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -48,14 +48,14 @@ type type_error = | WrongCaseInfo of inductive * case_info | NumberBranches of unsafe_judgment * int | IllFormedBranch of constr * constructor * constr * constr - | Generalization of (name * types) * unsafe_judgment + | Generalization of (Name.t * types) * unsafe_judgment | ActualType of unsafe_judgment * types | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment array | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * name array * int * env * unsafe_judgment array + | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array | IllTypedRecBody of - int * name array * unsafe_judgment array * types array + int * Name.t array * unsafe_judgment array * types array exception TypeError of env * type_error diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 1967018f6..531ad0b9e 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -49,14 +49,14 @@ type type_error = | WrongCaseInfo of inductive * case_info | NumberBranches of unsafe_judgment * int | IllFormedBranch of constr * constructor * constr * constr - | Generalization of (name * types) * unsafe_judgment + | Generalization of (Name.t * types) * unsafe_judgment | ActualType of unsafe_judgment * types | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment array | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * name array * int * env * unsafe_judgment array + | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array | IllTypedRecBody of - int * name array * unsafe_judgment array * types array + int * Name.t array * unsafe_judgment array * types array exception TypeError of env * type_error @@ -80,7 +80,7 @@ val error_number_branches : env -> unsafe_judgment -> int -> 'a val error_ill_formed_branch : env -> constr -> constructor -> constr -> constr -> 'a -val error_generalization : env -> name * types -> unsafe_judgment -> 'a +val error_generalization : env -> Name.t * types -> unsafe_judgment -> 'a val error_actual_type : env -> unsafe_judgment -> types -> 'a @@ -92,9 +92,9 @@ val error_cant_apply_bad_type : unsafe_judgment -> unsafe_judgment array -> 'a val error_ill_formed_rec_body : - env -> guard_error -> name array -> int -> env -> unsafe_judgment array -> 'a + env -> guard_error -> Name.t array -> int -> env -> unsafe_judgment array -> 'a val error_ill_typed_rec_body : - env -> int -> name array -> unsafe_judgment array -> types array -> 'a + env -> int -> Name.t array -> unsafe_judgment array -> types array -> 'a val error_elim_explain : sorts_family -> sorts_family -> arity_error diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 7b3aff20d..7617e8219 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -56,17 +56,17 @@ val judge_of_apply : (** {6 Type of an abstraction. } *) val judge_of_abstraction : - env -> name -> unsafe_type_judgment -> unsafe_judgment + env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment (** {6 Type of a product. } *) val judge_of_product : - env -> name -> unsafe_type_judgment -> unsafe_type_judgment + env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment (** s Type of a let in. *) val judge_of_letin : - env -> name -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment + env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment (** {6 Type of a cast. } *) @@ -89,7 +89,7 @@ val judge_of_case : env -> case_info -> unsafe_judgment * constraints (** Typecheck general fixpoint (not checking guard conditions) *) -val type_fixpoint : env -> name array -> types array +val type_fixpoint : env -> Name.t array -> types array -> unsafe_judgment array -> constraints (** Kernel safe typing but applicable to partial proofs *) diff --git a/library/impargs.mli b/library/impargs.mli index 66d72abbb..de8d89166 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -95,7 +95,7 @@ type manual_implicits = manual_explicitation list val compute_implicits_with_manual : env -> types -> bool -> manual_implicits -> implicit_status list -val compute_implicits_names : env -> types -> name list +val compute_implicits_names : env -> types -> Name.t list (** {6 Computation of implicits (done using the global environment). } *) diff --git a/library/nameops.mli b/library/nameops.mli index 0f71d28a1..1d3275d30 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -10,7 +10,7 @@ open Names (** Identifiers and names *) val pr_id : Id.t -> Pp.std_ppcmds -val pr_name : name -> Pp.std_ppcmds +val pr_name : Name.t -> Pp.std_ppcmds val make_ident : string -> int option -> Id.t val repr_ident : Id.t -> string * int option @@ -25,15 +25,15 @@ val has_subscript : Id.t -> bool val lift_subscript : Id.t -> Id.t val forget_subscript : Id.t -> Id.t -val out_name : name -> Id.t +val out_name : Name.t -> Id.t (** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"] otherwise. *) -val name_fold : (Id.t -> 'a -> 'a) -> name -> 'a -> 'a -val name_iter : (Id.t -> unit) -> name -> unit -val name_cons : name -> Id.t list -> Id.t list -val name_app : (Id.t -> Id.t) -> name -> name -val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> name -> 'a * name +val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a +val name_iter : (Id.t -> unit) -> Name.t -> unit +val name_cons : Name.t -> Id.t list -> Id.t list +val name_app : (Id.t -> Id.t) -> Name.t -> Name.t +val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t val pr_lab : Label.t -> Pp.std_ppcmds diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 0677fa8df..59768f5a6 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -79,7 +79,7 @@ let make_constr_action Gram.action (fun (v:reference) -> make (CRef v :: constrs, constrlists, binders) tl) | ETName -> - Gram.action (fun (na:Loc.t * name) -> + Gram.action (fun (na:Loc.t * Name.t) -> make (constr_expr_of_name na :: constrs, constrlists, binders) tl) | ETBigint -> Gram.action (fun (v:Bigint.bigint) -> @@ -130,7 +130,7 @@ let make_cases_pattern_action Gram.action (fun (v:reference) -> make (CPatAtom (Loc.ghost,Some v) :: env, envlist, hasbinders) tl) | ETName -> - Gram.action (fun (na:Loc.t * name) -> + Gram.action (fun (na:Loc.t * Name.t) -> make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl) | ETBigint -> Gram.action (fun (v:Bigint.bigint) -> diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index a5f99a40b..8ccc3ebef 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -160,7 +160,7 @@ module Prim : open Libnames val preident : string Gram.entry val ident : Id.t Gram.entry - val name : name located Gram.entry + val name : Name.t located Gram.entry val identref : Id.t located Gram.entry val pattern_ident : Id.t Gram.entry val pattern_identref : Id.t located Gram.entry @@ -198,7 +198,7 @@ module Constr : val binders : local_binder list Gram.entry (* list of binder *) val open_binders : local_binder list Gram.entry val binders_fixannot : (local_binder list * (Id.t located option * recursion_order_expr)) Gram.entry - val typeclass_constraint : (name located * bool * constr_expr) Gram.entry + val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry val record_declaration : constr_expr Gram.entry val appl_arg : (constr_expr * explicitation located option) Gram.entry end diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 966ebff40..5b7f0b4c7 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -11,7 +11,7 @@ open Pp open Tacexpr type 'it statement = - {st_label:name; + {st_label:Name.t; st_it:'it} type thesis_kind = diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index fb7e5c29a..107b65366 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -28,10 +28,10 @@ val proof_instr: Decl_expr.raw_proof_instr -> unit val tcl_change_info : Decl_mode.pm_info -> tactic val execute_cases : - Names.name -> + Name.t -> Decl_mode.per_info -> (Term.constr -> Proof_type.tactic) -> - (Names.Id.Set.elt * (Term.constr option * Term.constr list) list) list -> + (Id.Set.elt * (Term.constr option * Term.constr list) list) list -> Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic val tree_of_pats : @@ -44,8 +44,8 @@ val add_branch : val append_branch : Id.t *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> - (Names.Id.Set.t * Decl_mode.split_tree) option -> - (Names.Id.Set.t * Decl_mode.split_tree) option + (Id.Set.t * Decl_mode.split_tree) option -> + (Id.Set.t * Decl_mode.split_tree) option val append_tree : Id.t * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> @@ -58,7 +58,7 @@ val build_dep_clause : Term.types Decl_expr.statement list -> Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types val register_dep_subcase : - Names.Id.t * (int * int) -> + Id.t * (int * int) -> Environ.env -> Decl_mode.per_info -> Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind @@ -69,41 +69,41 @@ val thesis_for : Term.constr -> val close_previous_case : Proof.proof -> unit val pop_stacks : - (Names.Id.t * + (Id.t * (Term.constr option * Term.constr list) list) list -> - (Names.Id.t * + (Id.t * (Term.constr option * Term.constr list) list) list val push_head : Term.constr -> - Names.Id.Set.t -> - (Names.Id.t * + Id.Set.t -> + (Id.t * (Term.constr option * Term.constr list) list) list -> - (Names.Id.t * + (Id.t * (Term.constr option * Term.constr list) list) list val push_arg : Term.constr -> - (Names.Id.t * + (Id.t * (Term.constr option * Term.constr list) list) list -> - (Names.Id.t * + (Id.t * (Term.constr option * Term.constr list) list) list val hrec_for: - Names.Id.t -> + Id.t -> Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> - Names.Id.t -> Term.constr + Id.t -> Term.constr val consider_match : bool -> - (Names.Id.Set.elt*bool) list -> - Names.Id.Set.elt list -> + (Id.Set.elt*bool) list -> + Id.Set.elt list -> (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> Proof_type.tactic val init_tree: - Names.Id.Set.t -> - Names.inductive -> + Id.Set.t -> + inductive -> int option * Declarations.wf_paths -> (int -> (int option * Declarations.recarg Rtree.t) array -> - (Names.Id.Set.t * Decl_mode.split_tree) option) -> + (Id.Set.t * Decl_mode.split_tree) option) -> Decl_mode.split_tree diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 1c70908b6..bd8d549a2 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -79,7 +79,7 @@ val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast val anonymous_name : Id.t val dummy_name : Id.t -val id_of_name : name -> Id.t +val id_of_name : Name.t -> Id.t val id_of_mlid : ml_ident -> Id.t val tmp_id : ml_ident -> ml_ident diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index b69715fc9..1a97689b5 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -38,7 +38,7 @@ val error_MPfile_as_mod : module_path -> bool -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit -val msg_non_implicit : global_reference -> int -> name -> string +val msg_non_implicit : global_reference -> int -> Name.t -> string val error_non_implicit : string -> 'a val info_file : string -> unit diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9678fb547..f549adf7a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -169,7 +169,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = begin try let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in - let new_x : name = get_name (Termops.ids_of_context env) x in + let new_x : Name.t = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (x,None,t) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b @@ -198,7 +198,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = try let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in - let new_x : name = get_name (Termops.ids_of_context env) x in + let new_x : Name.t = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (x,Some v,t) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index cf7d8e8fe..8acd24c88 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -22,9 +22,9 @@ let observe strm = type binder_type = - | Lambda of name - | Prod of name - | LetIn of name + | Lambda of Name.t + | Prod of Name.t + | LetIn of Name.t type glob_context = (binder_type*glob_constr) list @@ -138,7 +138,7 @@ let apply_args ctxt body args = let need_convert avoid bt = List.exists (need_convert_id avoid) (ids_of_binder bt) in - let next_name_away (na:name) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = + let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = match na with | Name id when List.mem id avoid -> let new_id = Namegen.next_ident_away id avoid in @@ -1186,7 +1186,7 @@ and compute_cst_params_from_app acc (params,rtl) = compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * bool) list array) csts = +let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1222,13 +1222,13 @@ let rec rebuild_return_type rt = Constrexpr.CProdN(loc,n,rebuild_return_type t') | Constrexpr.CLetIn(loc,na,t,t') -> Constrexpr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Names.Anonymous], + | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous], Constrexpr.Default Decl_kinds.Explicit,rt], Constrexpr.CSort(Loc.ghost,GType None)) let do_build_inductive - funnames (funsargs: (Names.name * glob_constr * bool) list list) + funnames (funsargs: (Name.t * glob_constr * bool) list list) returned_types (rtl:glob_constr list) = let _time1 = System.get_time () in @@ -1257,7 +1257,7 @@ let do_build_inductive let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = funargs in List.fold_right @@ -1323,7 +1323,7 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = (snd (List.chop nrel_params funargs)) in List.fold_right diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 87fcb1022..101be24fd 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -1,5 +1,4 @@ - - +open Names (* [build_inductive parametrize funnames funargs returned_types bodies] @@ -8,8 +7,8 @@ *) val build_inductive : - Names.Id.t list -> (* The list of function name *) - (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *) + Id.t list -> (* The list of function name *) + (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) unit diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 55d793e03..0f10636f0 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,8 +1,9 @@ +open Names open Glob_term open Misctypes (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) -val get_pattern_id : cases_pattern -> Names.Id.t list +val get_pattern_id : cases_pattern -> Id.t list (* [pattern_to_term pat] returns a glob_constr corresponding to [pat]. [pat] must not contain occurences of anonymous pattern @@ -14,11 +15,11 @@ val pattern_to_term : cases_pattern -> glob_constr In each of them the location is Util.Loc.ghost *) val mkGRef : Globnames.global_reference -> glob_constr -val mkGVar : Names.Id.t -> glob_constr +val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr -val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr -val mkGProd : Names.name * glob_constr * glob_constr -> glob_constr -val mkGLetIn : Names.name * glob_constr * glob_constr -> glob_constr +val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr +val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr +val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr val mkGSort : glob_sort -> glob_constr val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) @@ -27,15 +28,15 @@ val mkGCast : glob_constr* glob_constr -> glob_constr Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) -val glob_decompose_prod : glob_constr -> (Names.name*glob_constr) list * glob_constr +val glob_decompose_prod : glob_constr -> (Name.t*glob_constr) list * glob_constr val glob_decompose_prod_or_letin : - glob_constr -> (Names.name*glob_constr option*glob_constr option) list * glob_constr -val glob_decompose_prod_n : int -> glob_constr -> (Names.name*glob_constr) list * glob_constr + glob_constr -> (Name.t*glob_constr option*glob_constr option) list * glob_constr +val glob_decompose_prod_n : int -> glob_constr -> (Name.t*glob_constr) list * glob_constr val glob_decompose_prod_or_letin_n : int -> glob_constr -> - (Names.name*glob_constr option*glob_constr option) list * glob_constr -val glob_compose_prod : glob_constr -> (Names.name*glob_constr) list -> glob_constr + (Name.t*glob_constr option*glob_constr option) list * glob_constr +val glob_compose_prod : glob_constr -> (Name.t*glob_constr) list -> glob_constr val glob_compose_prod_or_letin: glob_constr -> - (Names.name*glob_constr option*glob_constr option) list -> glob_constr + (Name.t*glob_constr option*glob_constr option) list -> glob_constr val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) @@ -57,7 +58,7 @@ val glob_make_or_list : glob_constr list -> glob_constr (* Replace the var mapped in the glob_constr/context *) -val change_vars : Names.Id.t Names.Id.Map.t -> glob_constr -> glob_constr +val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr @@ -69,27 +70,27 @@ val change_vars : Names.Id.t Names.Id.Map.t -> glob_constr -> glob_constr [avoid] with the variables appearing in the result. *) val alpha_pat : - Names.Id.Map.key list -> + Id.Map.key list -> Glob_term.cases_pattern -> - Glob_term.cases_pattern * Names.Id.Map.key list * - Names.Id.t Names.Id.Map.t + Glob_term.cases_pattern * Id.Map.key list * + Id.t Id.Map.t (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt conventions and does not share bound variables with avoid *) -val alpha_rt : Names.Id.t list -> glob_constr -> glob_constr +val alpha_rt : Id.t list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) -val alpha_br : Names.Id.t list -> - Loc.t * Names.Id.t list * Glob_term.cases_pattern list * +val alpha_br : Id.t list -> + Loc.t * Id.t list * Glob_term.cases_pattern list * Glob_term.glob_constr -> - Loc.t * Names.Id.t list * Glob_term.cases_pattern list * + Loc.t * Id.t list * Glob_term.cases_pattern list * Glob_term.glob_constr (* Reduction function *) val replace_var_by_term : - Names.Id.t -> + Id.t -> Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr @@ -97,7 +98,7 @@ val replace_var_by_term : (* [is_free_in id rt] checks if [id] is a free variable in [rt] *) -val is_free_in : Names.Id.t -> glob_constr -> bool +val is_free_in : Id.t -> glob_constr -> bool val are_unifiable : cases_pattern -> cases_pattern -> bool @@ -109,10 +110,10 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool ids_of_pat : cases_pattern -> Id.Set.t returns the set of variables appearing in a pattern *) -val ids_of_pat : cases_pattern -> Names.Id.Set.t +val ids_of_pat : cases_pattern -> Id.Set.t (* TODO: finish this function (Fix not treated) *) -val ids_of_glob_constr: glob_constr -> Names.Id.Set.t +val ids_of_glob_constr: glob_constr -> Id.Set.t (* removing let_in construction in a glob_constr diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 7d0f5a00e..d9f0f51ce 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -16,12 +16,12 @@ val msgnl : std_ppcmds -> unit val invalid_argument : string -> 'a val fresh_id : Id.t list -> string -> Id.t -val fresh_name : Id.t list -> string -> name -val get_name : Id.t list -> ?default:string -> name -> name +val fresh_name : Id.t list -> string -> Name.t +val get_name : Id.t list -> ?default:string -> Name.t -> Name.t val array_get_start : 'a array -> 'a array -val id_of_name : name -> Id.t +val id_of_name : Name.t -> Id.t val locate_ind : Libnames.reference -> inductive val locate_constant : Libnames.reference -> constant @@ -36,10 +36,10 @@ val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val chop_rlambda_n : int -> Glob_term.glob_constr -> - (name*Glob_term.glob_constr*bool) list * Glob_term.glob_constr + (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr val chop_rprod_n : int -> Glob_term.glob_constr -> - (name*Glob_term.glob_constr) list * Glob_term.glob_constr + (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr val def_of_const : Term.constr -> Term.constr val eq : Term.constr Lazy.t diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 089493079..30c60b52b 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -543,8 +543,8 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = calls of branch 1 with all rec calls of branch 2. *) (* TODO: reecrire cette heuristique (jusqu'a merge_types) *) let rec merge_rec_hyps shift accrec - (ltyp:(Names.name * glob_constr option * glob_constr option) list) - filter_shift_stable : (Names.name * glob_constr option * glob_constr option) list = + (ltyp:(Name.t * glob_constr option * glob_constr option) list) + filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = let mergeonehyp t reldecl = match reldecl with | (nme,x,Some (GApp(_,i,args) as ind)) @@ -560,7 +560,7 @@ let rec merge_rec_hyps shift accrec | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable -let build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift = +let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift = List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec @@ -584,9 +584,9 @@ let prnt_prod_or_letin nm letbdy typ = let rec merge_types shift accrec1 - (ltyp1:(name * glob_constr option * glob_constr option) list) - (concl1:glob_constr) (ltyp2:(name * glob_constr option * glob_constr option) list) concl2 - : (name * glob_constr option * glob_constr option) list * glob_constr = + (ltyp1:(Name.t * glob_constr option * glob_constr option) list) + (concl1:glob_constr) (ltyp2:(Name.t * glob_constr option * glob_constr option) list) concl2 + : (Name.t * glob_constr option * glob_constr option) list * glob_constr = let _ = prstr "MERGE_TYPES\n" in let _ = prstr "ltyp 1 : " in let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 7b77afd07..e662cd41d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -353,8 +353,8 @@ type ('a,'b) journey_info_tac = (* journey_info : specifies the actions to do on the different term constructors during the travelling of the term *) type journey_info = - { letiN : ((name*constr*types*constr),constr) journey_info_tac; - lambdA : ((name*types*constr),constr) journey_info_tac; + { letiN : ((Name.t*constr*types*constr),constr) journey_info_tac; + lambdA : ((Name.t*types*constr),constr) journey_info_tac; casE : ((constr infos -> tactic) -> constr infos -> tactic) -> ((case_info * constr * constr * constr array),constr) journey_info_tac; otherS : (unit,constr) journey_info_tac; diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml index 3e2c8ade7..da7e57766 100644 --- a/plugins/xml/acic.ml +++ b/plugins/xml/acic.ml @@ -68,9 +68,9 @@ type aconstr = | AEvar of id * existential_key * aconstr list | ASort of id * sorts | ACast of id * aconstr * aconstr - | AProds of (id * name * aconstr) list * aconstr - | ALambdas of (id * name * aconstr) list * aconstr - | ALetIns of (id * name * aconstr) list * aconstr + | AProds of (id * Name.t * aconstr) list * aconstr + | ALambdas of (id * Name.t * aconstr) list * aconstr + | ALetIns of (id * Name.t * aconstr) list * aconstr | AApp of id * aconstr list | AConst of id * explicit_named_substitution * uri | AInd of id * explicit_named_substitution * uri * int diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index fca402c58..b7ecb2461 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -15,7 +15,7 @@ open Util open Libobject (*i*) -let empty_name_table = (Refmap.empty : name list list Refmap.t) +let empty_name_table = (Refmap.empty : Name.t list list Refmap.t) let name_table = ref empty_name_table let _ = @@ -26,7 +26,7 @@ let _ = type req = | ReqLocal - | ReqGlobal of global_reference * name list list + | ReqGlobal of global_reference * Name.t list list let load_rename_args _ (_, (_, (r, names))) = name_table := Refmap.add r names !name_table diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index 1b1f7576d..09b8859e6 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -11,10 +11,10 @@ open Globnames open Environ open Term -val rename_arguments : bool -> global_reference -> name list list -> unit +val rename_arguments : bool -> global_reference -> Name.t list list -> unit (** [Not_found] is raised is no names are defined for [r] *) -val arguments_names : global_reference -> name list list +val arguments_names : global_reference -> Name.t list list val rename_type_of_constant : env -> constant -> types val rename_type_of_inductive : env -> inductive -> types diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 17fb5503c..71c9325d7 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -114,7 +114,7 @@ type 'a rhs = type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; - alias_stack : name list; + alias_stack : Name.t list; eqn_loc : Loc.t; used : bool ref } @@ -122,12 +122,12 @@ type 'a matrix = 'a equation list (* 1st argument of IsInd is the original ind before extracting the summary *) type tomatch_type = - | IsInd of types * inductive_type * name list + | IsInd of types * inductive_type * Name.t list | NotInd of constr option * types type tomatch_status = - | Pushed of ((constr * tomatch_type) * int list * name) - | Alias of (name * constr * (constr * types)) + | Pushed of ((constr * tomatch_type) * int list * Name.t) + | Alias of (Name.t * constr * (constr * types)) | NonDepAlias | Abstract of int * rel_declaration diff --git a/pretyping/cases.mli b/pretyping/cases.mli index d1ca69dcd..d9f9b9d76 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -74,7 +74,7 @@ type 'a rhs = type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; - alias_stack : name list; + alias_stack : Name.t list; eqn_loc : Loc.t; used : bool ref } @@ -82,12 +82,12 @@ type 'a matrix = 'a equation list (* 1st argument of IsInd is the original ind before extracting the summary *) type tomatch_type = - | IsInd of types * inductive_type * name list + | IsInd of types * inductive_type * Name.t list | NotInd of constr option * types type tomatch_status = - | Pushed of ((constr * tomatch_type) * int list * name) - | Alias of (name * constr * (constr * types)) + | Pushed of ((constr * tomatch_type) * int list * Name.t) + | Alias of (Name.t * constr * (constr * types)) | NonDepAlias | Abstract of int * rel_declaration diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index cb71e1aa6..a84bbcc54 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -41,7 +41,7 @@ type cbv_value = | VAL of int * constr | STACK of int * cbv_value * cbv_stack | CBN of constr * cbv_value subs - | LAM of int * (name * constr) list * constr * cbv_value subs + | LAM of int * (Name.t * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array | CONSTR of constructor * cbv_value array diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 08e52ff72..66aef4d14 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -27,7 +27,7 @@ type cbv_value = | VAL of int * constr | STACK of int * cbv_value * cbv_stack | CBN of constr * cbv_value subs - | LAM of int * (name * constr) list * constr * cbv_value subs + | LAM of int * (Name.t * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array | CONSTR of constructor * cbv_value array diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 001f3b5a6..d9d82faa2 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -323,7 +323,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | GLambda (_,x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = - if List.for_all (name_eq Anonymous) nl then None + if List.for_all (Name.equal Anonymous) nl then None else Some (dl,indsp,nl) in n, aliastyp, Some typ in diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 1e31e04d4..3a8f54904 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -54,7 +54,7 @@ val synthetize_type : unit -> bool (** Utilities to transform kernel cases to simple pattern-matching problem *) -val it_destRLambda_or_LetIn_names : int -> glob_constr -> name list * glob_constr +val it_destRLambda_or_LetIn_names : int -> glob_constr -> Name.t list * glob_constr val simple_cases_matrix_of_branches : inductive -> (int * int * glob_constr) list -> cases_clauses val return_type_of_predicate : diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index b056cd260..9c6f1ad47 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -157,7 +157,7 @@ val mk_valcon : constr -> val_constraint val split_tycon : Loc.t -> env -> evar_map -> type_constraint -> - evar_map * (name * type_constraint * type_constraint) + evar_map * (Name.t * type_constraint * type_constraint) val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : int -> type_constraint -> type_constraint diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 8722516bb..4c18aec19 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -294,8 +294,8 @@ type instance_status = instance_constraint * instance_typing_status (* Clausal environments *) type clbinding = - | Cltyp of name * constr freelisted - | Clval of name * (constr freelisted * instance_status) * constr freelisted + | Cltyp of Name.t * constr freelisted + | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted let map_clb f = function | Cltyp (na,cfl) -> Cltyp (na,map_fl f cfl) @@ -650,7 +650,7 @@ let meta_with_name evd id = Metamap.fold (fun n clb (l1,l2 as l) -> let (na',def) = clb_name clb in - if name_eq na na' then if def then (n::l1,l2) else (n::l1,n::l2) + if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) else l) evd.metas ([],[]) in match mvnodef, mvl with diff --git a/pretyping/evd.mli b/pretyping/evd.mli index a73dbdcdc..86ec47d3e 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -68,8 +68,8 @@ type instance_status = instance_constraint * instance_typing_status (** Clausal environments *) type clbinding = - | Cltyp of name * constr freelisted - | Clval of name * (constr freelisted * instance_status) * constr freelisted + | Cltyp of Name.t * constr freelisted + | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted val map_clb : (constr -> constr) -> clbinding -> clbinding @@ -216,10 +216,10 @@ val meta_fvalue : evar_map -> metavariable -> constr freelisted * instance_st val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option val meta_type : evar_map -> metavariable -> types val meta_ftype : evar_map -> metavariable -> types freelisted -val meta_name : evar_map -> metavariable -> name +val meta_name : evar_map -> metavariable -> Name.t val meta_with_name : evar_map -> Id.t -> metavariable val meta_declare : - metavariable -> types -> ?name:name -> evar_map -> evar_map + metavariable -> types -> ?name:Name.t -> evar_map -> evar_map val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 2e8908cfb..730332514 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -24,7 +24,7 @@ val glob_sort_eq : glob_sort -> glob_sort -> bool val cases_pattern_loc : cases_pattern -> Loc.t -val cases_predicate_names : tomatch_tuples -> name list +val cases_predicate_names : tomatch_tuples -> Name.t list (** Apply one argument to a glob_constr *) val mkGApp : Loc.t -> glob_constr -> glob_constr -> glob_constr @@ -46,6 +46,6 @@ val loc_of_glob_constr : glob_constr -> Loc.t Take the current alias as parameter, @raise Not_found if translation is impossible *) -val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern +val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern -val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr +val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index cbfd78deb..8009524de 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -291,7 +291,7 @@ let next_name_away_for_default_printing env_t na avoid = type renaming_flags = | RenamingForCasesPattern | RenamingForGoal - | RenamingElsewhereFor of (name list * constr) + | RenamingElsewhereFor of (Name.t list * constr) let next_name_for_display flags = match flags with diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index 6702c9f70..6c982451a 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -16,15 +16,15 @@ open Environ 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 -> Id.t -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 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 @@ -53,16 +53,16 @@ val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t 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 -> Id.t list -> Id.t +val next_name_away_in_cases_pattern : Name.t -> Id.t list -> Id.t -val next_name_away : name -> Id.t list -> Id.t (** default is "H" *) -val next_name_away_with_default : string -> name -> Id.t list -> +val next_name_away : Name.t -> Id.t list -> Id.t (** default is "H" *) +val next_name_away_with_default : string -> Name.t -> Id.t list -> Id.t -val next_name_away_with_default_using_types : string -> name -> +val next_name_away_with_default_using_types : string -> Name.t -> Id.t list -> types -> Id.t -val set_reserved_typed_name : (types -> name) -> unit +val set_reserved_typed_name : (types -> Name.t) -> unit (********************************************************************* Making name distinct for displaying *) @@ -70,15 +70,15 @@ val set_reserved_typed_name : (types -> name) -> unit type renaming_flags = | RenamingForCasesPattern (** 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 -> Id.t list -> name -> constr -> name * Id.t list + 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 -> constr -> name * Id.t list + 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 -> constr -> name * Id.t list + renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list val rename_bound_vars_as_displayed : - Id.t list -> name list -> types -> types + Id.t list -> Name.t list -> types -> types diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index d784fc0ed..c1e91ca2f 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -39,11 +39,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with | PSoApp (id1, arg1), PSoApp (id2, arg2) -> Id.equal id1 id2 && List.equal constr_pattern_eq arg1 arg2 | PLambda (v1, t1, b1), PLambda (v2, t2, b2) -> - name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 + Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PProd (v1, t1, b1), PProd (v2, t2, b2) -> - name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 + Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) -> - name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 + Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PSort s1, PSort s2 -> glob_sort_eq s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> @@ -73,7 +73,7 @@ and cofixpoint_eq (i1, r1) (i2, r2) = rec_declaration_eq r1 r2 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = - Array.equal name_eq n1 n2 && + Array.equal Name.equal n1 n2 && Array.equal eq_constr c1 c2 && Array.equal eq_constr r1 r2 diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cced783f5..ad6922dbe 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -28,9 +28,9 @@ type pretype_error = | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option | CannotFindWellTypedAbstraction of constr * constr list - | WrongAbstractionType of name * constr * types * types - | AbstractionOverMeta of name * name - | NonLinearUnification of name * constr + | WrongAbstractionType of Name.t * constr * types * types + | AbstractionOverMeta of Name.t * Name.t + | NonLinearUnification of Name.t * constr (* Pretyping *) | VarNotFound of Id.t | UnexpectedType of constr * constr diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index aa0b65e4f..558f3d5bb 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -30,9 +30,9 @@ type pretype_error = | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option | CannotFindWellTypedAbstraction of constr * constr list - | WrongAbstractionType of name * constr * types * types - | AbstractionOverMeta of name * name - | NonLinearUnification of name * constr + | WrongAbstractionType of Name.t * constr * types * types + | AbstractionOverMeta of Name.t * Name.t + | NonLinearUnification of Name.t * constr (** Pretyping *) | VarNotFound of Id.t | UnexpectedType of constr * constr @@ -82,7 +82,7 @@ val error_number_branches_loc : val error_ill_typed_rec_body_loc : Loc.t -> env -> Evd.evar_map -> - int -> name array -> unsafe_judgment array -> types array -> 'b + int -> Name.t array -> unsafe_judgment array -> types array -> 'b val error_not_a_type_loc : Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b @@ -108,7 +108,7 @@ val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> constr -> constr list -> 'b val error_wrong_abstraction_type : env -> Evd.evar_map -> - name -> constr -> types -> types -> 'b + Name.t -> constr -> types -> types -> 'b val error_abstraction_over_meta : env -> Evd.evar_map -> metavariable -> metavariable -> 'b diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 72d43fabd..777e6c1d8 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -36,7 +36,7 @@ open Reductionops type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; - s_PROJKIND : (name * bool) list; + s_PROJKIND : (Name.t * bool) list; s_PROJ : constant option list } let structure_table = ref (Indmap.empty : struc_typ Indmap.t) @@ -46,7 +46,7 @@ let projection_table = ref Cmap.empty is the inductive always (fst constructor) ? It seems so... *) type struc_tuple = - inductive * constructor * (name * bool) list * constant option list + inductive * constructor * (Name.t * bool) list * constant option list let load_structure i (_,(ind,id,kl,projs)) = let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 538e6d540..6afba15bf 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -22,11 +22,11 @@ open Library type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; - s_PROJKIND : (name * bool) list; + s_PROJKIND : (Name.t * bool) list; s_PROJ : constant option list } type struc_tuple = - inductive * constructor * (name * bool) list * constant option list + inductive * constructor * (Name.t * bool) list * constant option list val declare_structure : struc_tuple -> unit diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 4263aec53..60c111370 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -154,9 +154,9 @@ val hnf_lam_app : env -> evar_map -> constr -> constr -> constr val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr -val splay_prod : env -> evar_map -> constr -> (name * constr) list * constr -val splay_lam : env -> evar_map -> constr -> (name * constr) list * constr -val splay_arity : env -> evar_map -> constr -> (name * constr) list * sorts +val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr +val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr +val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts val sort_of_arity : env -> evar_map -> constr -> sorts val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr diff --git a/pretyping/termops.ml b/pretyping/termops.ml index f48734be7..f5be89689 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -838,7 +838,7 @@ let add_vname vars = function (*************************) (* Names environments *) (*************************) -type names_context = name list +type names_context = Name.t list let add_name n nl = n::nl let lookup_name_of_rel p names = try List.nth names (p-1) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 051a77883..3e0f0e0eb 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -37,9 +37,9 @@ val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds (** about contexts *) -val push_rel_assum : name * types -> env -> env -val push_rels_assum : (name * types) list -> env -> env -val push_named_rec_types : name array * types array * 'a -> env -> env +val push_rel_assum : Name.t * types -> env -> env +val push_rels_assum : (Name.t * types) list -> env -> env +val push_named_rec_types : Name.t array * types array * 'a -> env -> env val lookup_rel_id : Id.t -> rel_context -> int * constr option * types (** Associates the contents of an identifier in a [rel_context]. Raise @@ -54,8 +54,8 @@ val extended_rel_vect : int -> rel_context -> constr array (** iterators/destructors on terms *) val mkProd_or_LetIn : rel_declaration -> types -> types val mkProd_wo_LetIn : rel_declaration -> types -> types -val it_mkProd : types -> (name * types) list -> types -val it_mkLambda : constr -> (name * types) list -> constr +val it_mkProd : types -> (Name.t * types) list -> types +val it_mkLambda : constr -> (Name.t * types) list -> constr val it_mkProd_or_LetIn : types -> rel_context -> types val it_mkProd_wo_LetIn : types -> rel_context -> types val it_mkLambda_or_LetIn : constr -> rel_context -> constr @@ -69,7 +69,7 @@ val it_named_context_quantifier : (** {6 Generic iterators on constr} *) val map_constr_with_named_binders : - (name -> 'a -> 'a) -> + (Name.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_binders_left_to_right : (rel_declaration -> 'a -> 'a) -> @@ -225,9 +225,9 @@ val adjust_app_array_size : constr -> constr array -> constr -> constr array -> (constr * constr array * constr * constr array) (** name contexts *) -type names_context = name list -val add_name : name -> names_context -> names_context -val lookup_name_of_rel : int -> names_context -> name +type names_context = Name.t list +val add_name : Name.t -> names_context -> names_context +val lookup_name_of_rel : int -> names_context -> Name.t val lookup_rel_of_name : Id.t -> names_context -> int val empty_names_context : names_context val ids_of_rel_context : rel_context -> Id.t list @@ -240,11 +240,11 @@ val env_rel_context_chop : int -> env -> env * rel_context (** Set of local names *) val vars_of_env: env -> Id.Set.t -val add_vname : Id.Set.t -> name -> Id.Set.t +val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) val process_rel_context : (rel_declaration -> env -> env) -> env -> env -val assums_of_rel_context : rel_context -> (name * constr) list +val assums_of_rel_context : rel_context -> (Name.t * constr) list val lift_rel_context : int -> rel_context -> rel_context val substl_rel_context : constr list -> rel_context -> rel_context val smash_rel_context : rel_context -> rel_context (** expand lets in context *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index b5c710da2..0fe13ef9c 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -58,7 +58,7 @@ type typeclass = { cl_props : rel_context; (* The method implementaions as projections. *) - cl_projs : (name * (direction * int option) option * constant option) list; + cl_projs : (Name.t * (direction * int option) option * constant option) list; } module Gmap = Fmap.Make(RefOrdered) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 72b3bbd27..5e2b9b78d 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -37,7 +37,7 @@ type typeclass = { Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (name * (direction * int option) option * constant option) list; + cl_projs : (Name.t * (direction * int option) option * constant option) list; } type instance diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 7343140d2..95498b8d8 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -33,7 +33,7 @@ val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_metaid : Id.t -> std_ppcmds val pr_lident : Id.t located -> std_ppcmds -val pr_lname : name located -> std_ppcmds +val pr_lname : Name.t located -> std_ppcmds val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds val pr_com_at : int -> std_ppcmds @@ -43,7 +43,7 @@ val pr_sep_com : constr_expr -> std_ppcmds val pr_id : Id.t -> std_ppcmds -val pr_name : name -> std_ppcmds +val pr_name : Name.t -> std_ppcmds val pr_qualid : qualid -> std_ppcmds val pr_patvar : patvar -> std_ppcmds diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 7a3395f1b..2747abe60 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -19,7 +19,7 @@ open Misctypes (** A Pretty-Printer for the Calculus of Inductive Constructions. *) -val assumptions_for_print : name list -> Termops.names_context +val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds diff --git a/proofs/logic.ml b/proofs/logic.ml index ba85be766..c48882c1a 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -26,7 +26,7 @@ type refiner_error = (* Errors raised by the refiner *) | BadType of constr * constr * constr - | UnresolvedBindings of name list + | UnresolvedBindings of Name.t list | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr diff --git a/proofs/logic.mli b/proofs/logic.mli index e87adb165..40feb5c56 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -39,7 +39,7 @@ type refiner_error = (*i Errors raised by the refiner i*) | BadType of constr * constr * constr - | UnresolvedBindings of name list + | UnresolvedBindings of Name.t list | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 2ba1b315b..8afee3418 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -46,7 +46,7 @@ val db_pattern_rule : (** Prints a matched hypothesis *) val db_matched_hyp : - debug_info -> env -> Id.t * constr option * constr -> name -> unit + debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit (** Prints the matched conclusion *) val db_matched_concl : debug_info -> env -> constr -> unit @@ -56,7 +56,7 @@ val db_mc_pattern_success : debug_info -> unit (** Prints a failure message for an hypothesis pattern *) val db_hyp_pattern_failure : - debug_info -> env -> name * constr_pattern match_pattern -> unit + debug_info -> env -> Name.t * constr_pattern match_pattern -> unit (** Prints a matching failure message for a rule *) val db_matching_failure : debug_info -> unit diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 7813f5326..b6ce3e30c 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -14,4 +14,4 @@ open Locus val instantiate : int -> Tacinterp.interp_sign * Glob_term.glob_constr -> (Id.t * hyp_location_flag, unit) location -> tactic -val let_evar : name -> Term.types -> tactic +val let_evar : Name.t -> Term.types -> tactic diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 47fd9aac2..b4491770e 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -54,11 +54,11 @@ val h_cofix : Id.t option -> tactic val h_cut : constr -> tactic val h_generalize : constr list -> tactic -val h_generalize_gen : (constr Locus.with_occurrences * name) list -> tactic +val h_generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic val h_generalize_dep : ?with_let:bool -> constr -> tactic -val h_let_tac : letin_flag -> name -> constr -> Locus.clause -> +val h_let_tac : letin_flag -> Name.t -> constr -> Locus.clause -> intro_pattern_expr located option -> tactic -val h_let_pat_tac : letin_flag -> name -> evar_map * constr -> +val h_let_pat_tac : letin_flag -> Name.t -> evar_map * constr -> Locus.clause -> intro_pattern_expr located option -> tactic diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 69a4db463..1367bb87a 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -86,7 +86,7 @@ val is_equality_type : testing_function val match_with_nottype : (constr * constr) matching_function val is_nottype : testing_function -val match_with_forall_term : (name * constr * constr) matching_function +val match_with_forall_term : (Name.t * constr * constr) matching_function val is_forall_term : testing_function val match_with_imp_term : (constr * constr) matching_function diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 041edd250..84040722e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -363,16 +363,16 @@ val cut_in_parallel : constr list -> tactic val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic val forward : tactic option -> intro_pattern_expr located option -> constr -> tactic -val letin_tac : (bool * intro_pattern_expr located) option -> name -> +val letin_tac : (bool * intro_pattern_expr located) option -> Name.t -> constr -> types option -> clause -> tactic -val letin_pat_tac : (bool * intro_pattern_expr located) option -> name -> +val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t -> evar_map * constr -> types option -> clause -> tactic -val assert_tac : name -> types -> tactic -val assert_by : name -> types -> tactic -> tactic -val pose_proof : name -> constr -> tactic +val assert_tac : Name.t -> types -> tactic +val assert_by : Name.t -> types -> tactic -> tactic +val pose_proof : Name.t -> constr -> tactic val generalize : constr list -> tactic -val generalize_gen : ((occurrences * constr) * name) list -> tactic +val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic val unify : ?state:Names.transparent_state -> constr -> constr -> tactic diff --git a/toplevel/classes.ml b/toplevel/classes.ml index a5805b637..21838bf68 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -221,7 +221,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props in let (loc, mid) = get_id loc_mid in List.iter (fun (n, _, x) -> - if name_eq n (Name mid) then + if Name.equal n (Name mid) then Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x) k.cl_projs; c :: props, rest' diff --git a/toplevel/command.mli b/toplevel/command.mli index a9898329a..618dd2019 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -125,20 +125,20 @@ type recursive_preentry = val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * Impargs.manual_implicits * int option) list + recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * Impargs.manual_implicits * int option) list + recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : - recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> + recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : - recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> + recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index 3c7000cb0..d6bc90bc3 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -28,7 +28,7 @@ val start_proof_com : goal_kind -> val start_proof_with_initialization : goal_kind -> (bool * lemma_possible_guards * tactic list option) option -> - (Id.t * (types * (name list * Impargs.manual_explicitation list))) list + (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit (** A hook the next three functions pass to cook_proof *) diff --git a/toplevel/record.ml b/toplevel/record.ml index 12b87b67a..17b07005e 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -120,7 +120,7 @@ let warning_or_error coe indsp err = Flags.if_verbose msg_warning (hov 0 st) type field_status = - | NoProjection of name + | NoProjection of Name.t | Projection of constr exception NotDefinable of record_error diff --git a/toplevel/record.mli b/toplevel/record.mli index e7e3330b8..9e3781fd5 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -21,7 +21,7 @@ open Globnames val declare_projections : inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t -> coercion_flag list -> manual_explicitation list list -> rel_context -> - (name * bool) list * constant option list + (Name.t * bool) list * constant option list val declare_structure : Decl_kinds.recursivity_kind -> bool (**infer?*) -> Id.t -> Id.t -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2a9af66ff..5c2d8604c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -907,7 +907,7 @@ let vernac_declare_arguments local r l nargs flags = let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in let names, rest = List.hd names, List.tl names in let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in - if List.exists (fun na -> not (List.equal name_eq na names)) rest then + if List.exists (fun na -> not (List.equal Name.equal na names)) rest then error "All arguments lists must declare the same names."; if not (List.distinct (List.filter ((!=) Anonymous) names)) then error "Arguments names must be distinct."; @@ -950,7 +950,7 @@ let vernac_declare_arguments local r l nargs flags = let some_renaming_specified = try let names = Arguments_renaming.arguments_names sr in - not (List.equal (List.equal name_eq) names names_decl) + not (List.equal (List.equal Name.equal) names names_decl) with Not_found -> false in let some_renaming_specified, implicits = match l with |