diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comCoercion.ml | 26 | ||||
| -rw-r--r-- | vernac/dune | 2 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 19 |
3 files changed, 17 insertions, 30 deletions
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 15d8ebc4b5..86b15739f9 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -237,24 +237,24 @@ let open_coercion i o = cache_coercion o let discharge_coercion (_, c) = - if c.coercion_local then None + if c.coe_local then None else let n = try - let ins = Lib.section_instance c.coercion_type in + let ins = Lib.section_instance c.coe_value in Array.length (snd ins) with Not_found -> 0 in let nc = { c with - coercion_params = n + c.coercion_params; - coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj; + coe_param = n + c.coe_param; + coe_is_projection = Option.map Lib.discharge_proj_repr c.coe_is_projection; } in Some nc let classify_coercion obj = - if obj.coercion_local then Dispose else Substitute obj + if obj.coe_local then Dispose else Substitute obj -let inCoercion : coercion -> obj = +let inCoercion : coe_info_typ -> obj = declare_object {(default_object "COERCION") with open_function = simple_open open_coercion; cache_function = cache_coercion; @@ -269,13 +269,13 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps | _ -> None in let c = { - coercion_type = coef; - coercion_local = local; - coercion_is_id = isid; - coercion_is_proj = isproj; - coercion_source = cls; - coercion_target = clt; - coercion_params = ps; + coe_value = coef; + coe_local = local; + coe_is_identity = isid; + coe_is_projection = isproj; + coe_source = cls; + coe_target = clt; + coe_param = ps; } in Lib.add_anonymous_leaf (inCoercion c) diff --git a/vernac/dune b/vernac/dune index ba361b1377..7319b1353c 100644 --- a/vernac/dune +++ b/vernac/dune @@ -1,7 +1,7 @@ (library (name vernac) (synopsis "Coq's Vernacular Language") - (public_name coq.vernac) + (public_name coq-core.vernac) (wrapped false) (libraries tactics parsing)) diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 79a0cdf8d1..ec6e3b44ba 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -976,15 +976,11 @@ open Coercionops let print_coercion_value v = Printer.pr_global v.coe_value -let print_class i = - let cl,_ = class_info_from_index i in - pr_class cl - let print_path ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ str"] : ") ++ - print_class i ++ str" >-> " ++ print_class j + pr_class i ++ str" >-> " ++ pr_class j let _ = Coercionops.install_path_printer print_path @@ -997,25 +993,16 @@ let print_classes () = let print_coercions () = pr_sequence print_coercion_value (coercions()) -let index_of_class cl = - try - fst (class_info cl) - with Not_found -> - user_err ~hdr:"index_of_class" - (pr_class cl ++ spc() ++ str "not a defined class.") - let print_path_between cls clt = - let i = index_of_class cls in - let j = index_of_class clt in let p = try - lookup_path_between_class (i,j) + lookup_path_between_class (cls, clt) with Not_found -> user_err ~hdr:"index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path ((i,j),p) + print_path ((cls, clt), p) let print_canonical_projections env sigma grefs = let match_proj_gref ((x,y),c) gr = |