diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comCoercion.ml | 26 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 19 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
4 files changed, 26 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/himsg.ml b/vernac/himsg.ml index bff0359782..21a25ab78c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -924,7 +924,9 @@ let explain_not_match_error = function | InductiveFieldExpected _ -> strbrk "an inductive definition is expected" | DefinitionFieldExpected -> - strbrk "a definition is expected" + strbrk "a definition is expected. Hint: you can rename the \ + inductive or constructor and add a definition mapping the \ + old name to the new name" | ModuleFieldExpected -> strbrk "a module is expected" | ModuleTypeFieldExpected -> 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 = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 38ca836b32..e8d84a67a3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1568,6 +1568,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = ["Printing";"Raw";"Literals"]; + optread = (fun () -> !Constrextern.print_raw_literal); + optwrite = (fun b -> Constrextern.print_raw_literal := b) } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } |