diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:52:54 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:52:54 +0000 |
| commit | c3ca134628ad4d9ef70a13b65c48ff17c737238f (patch) | |
| tree | 136b4efbc3aefe76dcd2fa772141c774343f46df /plugins/funind/indfun_common.mli | |
| parent | 6946bbbf2390024b3ded7654814104e709cce755 (diff) | |
Modulification of name
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 10 |
1 files changed, 5 insertions, 5 deletions
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 |