diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 16:54:20 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 16:54:20 +0000 |
| commit | 889c0bbb3762f3c85663273e58a46815a9d1f8f5 (patch) | |
| tree | 3e13c101710bfb202b4f1229e23e955eafbc7311 /pretyping/classops.mli | |
| parent | 483e36a76c4a31a1711a4602be45f66e7f46760f (diff) | |
An automatic substitution of scope at functor application
For Argument Scope, we now record types (more precisely classes cl_typ)
in addition to scope list. After substitution (e.g. at functor application),
the new types are used to search for corresponding concrete scopes.
Currently, this automatic scope substitution of argument scope takes
precedence (if successful) over scope declared in the functor (even
by the user). On the opposite, the manual scope substitution
(cf last commit introducing annotation [scope foo to bar])
is done _after_ the automatic scope substitution.
TODO: if this behavior is satisfactory, document it ...
Note that Classops.find_class_type lose its env args since it was
actually unused, and is now used for Notation.find_class
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13840 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 3e6845f91..66bb5c6c6 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -50,7 +50,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c] and its arguments *) -val find_class_type : env -> evar_map -> types -> cl_typ * constr list +val find_class_type : evar_map -> types -> cl_typ * constr list (** raises [Not_found] if not convertible to a class *) val class_of : env -> evar_map -> types -> types * cl_index |