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 /intf/notation_term.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 'intf/notation_term.mli')
| -rw-r--r-- | intf/notation_term.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/intf/notation_term.mli b/intf/notation_term.mli index d7bd73588..2b1286940 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -22,14 +22,14 @@ open Glob_term type notation_constr = (** Part common to [glob_constr] and [cases_pattern] *) | NRef of global_reference - | NVar of identifier + | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t - | NList of identifier * identifier * notation_constr * notation_constr * bool + | 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 - | NBinderList of identifier * identifier * notation_constr * notation_constr + | NBinderList of Id.t * Id.t * notation_constr * notation_constr | NLetIn of name * notation_constr * notation_constr | NCases of case_style * notation_constr option * (notation_constr * (name * (inductive * name list) option)) list * @@ -38,7 +38,7 @@ type notation_constr = notation_constr * notation_constr | NIf of notation_constr * (name * notation_constr option) * notation_constr * notation_constr - | NRec of fix_kind * identifier array * + | NRec of fix_kind * Id.t array * (name * notation_constr option * notation_constr) list array * notation_constr array * notation_constr array | NSort of glob_sort @@ -71,5 +71,5 @@ type notation_var_internalization_type = (** This characterizes to what a notation is interpreted to *) type interpretation = - (identifier * (subscopes * notation_var_instance_type)) list * + (Id.t * (subscopes * notation_var_instance_type)) list * notation_constr |