diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
| commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
| tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /tactics/tacintern.mli | |
| parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) | |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacintern.mli')
| -rw-r--r-- | tactics/tacintern.mli | 8 |
1 files changed, 4 insertions, 4 deletions
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 *) |