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

2 files changed, 9 insertions, 9 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 8205a6b2e8..42925a4c22 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -132,9 +132,9 @@ let coercion_info coe = Gmap.find coe !coercion_tab
 
 let coercion_exists coe = Gmap.mem coe !coercion_tab
 
-(* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
+(* find_class_type : evar_map -> constr -> cl_typ * constr list *)
 
-let find_class_type env sigma t =
+let find_class_type sigma t =
   let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
   match kind_of_term t' with
     | Var id -> CL_SECVAR id, args
@@ -152,7 +152,7 @@ let subst_cl_typ subst ct = match ct with
   | CL_CONST kn ->
       let kn',t = subst_con subst kn in
 	if kn' == kn then ct else
-         fst (find_class_type (Global.env()) Evd.empty t)
+         fst (find_class_type Evd.empty t)
   | CL_IND (kn,i) ->
       let kn' = subst_ind subst kn in
 	if kn' == kn then ct else
@@ -167,12 +167,12 @@ let subst_coe_typ subst t = fst (subst_global subst t)
 let class_of env sigma t =
   let (t, n1, i, args) =
     try
-      let (cl,args) = find_class_type env sigma t in
+      let (cl,args) = find_class_type sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, args)
     with Not_found ->
       let t = Tacred.hnf_constr env sigma t in
-      let (cl, args) = find_class_type env sigma t in
+      let (cl, args) = find_class_type sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, args)
   in
@@ -180,7 +180,7 @@ let class_of env sigma t =
 
 let inductive_class_of ind = fst (class_info (CL_IND ind))
 
-let class_args_of env sigma c = snd (find_class_type env sigma c)
+let class_args_of env sigma c = snd (find_class_type sigma c)
 
 let string_of_class = function
   | CL_FUN -> "Funclass"
@@ -209,14 +209,14 @@ let lookup_path_to_sort_from_class s =
 
 let apply_on_class_of env sigma t cont =
   try
-    let (cl,args) = find_class_type env sigma t in
+    let (cl,args) = find_class_type sigma t in
     let (i, { cl_param = n1 } ) = class_info cl in
     if List.length args <> n1 then raise Not_found;
     t, cont i
   with Not_found ->
     (* Is it worth to be more incremental on the delta steps? *)
     let t = Tacred.hnf_constr env sigma t in
-    let (cl, args) = find_class_type env sigma t in
+    let (cl, args) = find_class_type sigma t in
     let (i, { cl_param = n1 } ) = class_info cl in
     if List.length args <> n1 then raise Not_found;
     t, cont i
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 3e6845f91d..66bb5c6c6a 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