From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:56:25 +0000 Subject: Modulification of identifier git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tacintern.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'tactics/tacintern.mli') diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index 69a708d23..5f302f1b9 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -24,8 +24,8 @@ open Nametab Conversion from [raw_tactic_expr] to [glob_tactic_expr] *) type glob_sign = { - ltacvars : identifier list * identifier list; - ltacrecvars : (identifier * ltac_constant) list; + ltacvars : Id.t list * Id.t list; + ltacrecvars : (Id.t * ltac_constant) list; gsigma : Evd.evar_map; genv : Environ.env } @@ -40,7 +40,7 @@ val make_empty_glob_sign : unit -> glob_sign val glob_tactic : raw_tactic_expr -> glob_tactic_expr val glob_tactic_env : - identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr + Id.t list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr (** Low-level variants *) @@ -55,7 +55,7 @@ val intern_constr_with_bindings : glob_sign -> constr_expr * constr_expr bindings -> glob_constr_and_expr * glob_constr_and_expr bindings -val intern_hyp : glob_sign -> identifier Loc.located -> identifier Loc.located +val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located (** Adds a globalization function for extra generic arguments *) -- cgit v1.2.3