diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index bbad005c..83ba05bb 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: classops.ml 9257 2006-10-21 17:28:28Z herbelin $ *) +(* $Id: classops.ml 10840 2008-04-23 21:29:34Z herbelin $ *) open Util open Pp -open Options +open Flags open Names open Libnames open Nametab @@ -44,7 +44,7 @@ type coe_typ = global_reference type coe_info_typ = { coe_value : constr; coe_type : types; - coe_strength : strength; + coe_strength : locality; coe_is_identity : bool; coe_param : int } @@ -290,7 +290,7 @@ let add_coercion_in_graph (ic,source,target) = if (!ambig_paths <> []) && is_verbose () then ppnl (message_ambig !ambig_paths) -type coercion = coe_typ * strength * bool * cl_typ * cl_typ * int +type coercion = coe_typ * locality * bool * cl_typ * cl_typ * int (* Calcul de l'arit้ d'une classe *) @@ -304,7 +304,7 @@ let class_params = function | CL_SECVAR sp -> reference_arity_length (VarRef sp) | CL_IND sp -> reference_arity_length (IndRef sp) -(* add_class : cl_typ -> strength option -> bool -> unit *) +(* add_class : cl_typ -> locality_flag option -> bool -> unit *) let add_class cl = add_new_class cl { cl_param = class_params cl } @@ -366,12 +366,14 @@ let coercion_identity v = v.coe_is_identity (* For printing purpose *) let get_coercion_value v = v.coe_value +let pr_cl_index n = int n + let classes () = Bijint.dom !class_tab let coercions () = Gmap.rng !coercion_tab let inheritance_graph () = Gmap.to_list !inheritance_graph -let coercion_of_qualid qid = - let ref = Nametab.global qid in +let coercion_of_reference r = + let ref = Nametab.global r in if not (coercion_exists ref) then errorlabstrm "try_add_coercion" (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion"); @@ -380,7 +382,7 @@ let coercion_of_qualid qid = module CoercionPrinting = struct type t = coe_typ - let encode = coercion_of_qualid + let encode = coercion_of_reference let subst = subst_coe_typ let printer x = pr_global_env Idset.empty x let key = Goptions.SecondaryTable ("Printing","Coercion") |