diff options
Diffstat (limited to 'intf/glob_term.mli')
| -rw-r--r-- | intf/glob_term.mli | 18 |
1 files changed, 9 insertions, 9 deletions
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) |