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 /pretyping/glob_ops.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 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 2e8908cfb..730332514 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -24,7 +24,7 @@ val glob_sort_eq : glob_sort -> glob_sort -> bool val cases_pattern_loc : cases_pattern -> Loc.t -val cases_predicate_names : tomatch_tuples -> name list +val cases_predicate_names : tomatch_tuples -> Name.t list (** Apply one argument to a glob_constr *) val mkGApp : Loc.t -> glob_constr -> glob_constr -> glob_constr @@ -46,6 +46,6 @@ val loc_of_glob_constr : glob_constr -> Loc.t Take the current alias as parameter, @raise Not_found if translation is impossible *) -val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern +val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern -val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr +val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr |