diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-27 11:37:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-27 11:37:07 +0000 |
| commit | 264658d653e4c12b1739504f898f136396fb8ea4 (patch) | |
| tree | 608c46ded3a9e490836b631a274eee5f66c33b6a /interp | |
| parent | d66a59f8398ce5df4127b2cb5cc2d35b803ceba2 (diff) | |
Export compute_arguments_scope pour utilisation local a la construction des inductifs et points fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5585 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/symbols.ml | 6 | ||||
| -rw-r--r-- | interp/symbols.mli | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/interp/symbols.ml b/interp/symbols.ml index 7a2f2e3c9..37a206c00 100644 --- a/interp/symbols.ml +++ b/interp/symbols.ml @@ -413,17 +413,17 @@ let find_class t = | Sort _ -> CL_SORT | _ -> raise Not_found -let rec compute_ref_arguments_scope t = +let rec compute_arguments_scope t = match kind_of_term (Reductionops.whd_betaiotazeta t) with | Prod (_,t,u) -> let sc = try Some (find_class_scope (find_class t)) with Not_found -> None in - sc :: compute_ref_arguments_scope u + sc :: compute_arguments_scope u | _ -> [] let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in - declare_arguments_scope ref (compute_ref_arguments_scope t) + declare_arguments_scope ref (compute_arguments_scope t) (********************************) (* Encoding notations as string *) diff --git a/interp/symbols.mli b/interp/symbols.mli index 1add7570e..ce5fcdd26 100644 --- a/interp/symbols.mli +++ b/interp/symbols.mli @@ -128,6 +128,8 @@ val find_arguments_scope : global_reference -> scope_name option list val declare_class_scope : scope_name -> Classops.cl_typ -> unit val declare_ref_arguments_scope : global_reference -> unit +val compute_arguments_scope : Term.types -> scope_name option list + (* Building notation key *) type symbol = |