diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 6 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 11 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 2 |
3 files changed, 5 insertions, 14 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 49147dfd7a..9a628b3fde 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -370,8 +370,8 @@ 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 +380,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") diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 049c936415..829c5f4048 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -31,8 +31,8 @@ let dl = dummy_loc (****************************************************************************) (* Tools for printing of Cases *) -let encode_inductive qid = - let indsp = global_inductive qid in +let encode_inductive r = + let indsp = inductive_of_reference r in let constr_lengths = mis_constr_nargs indsp in (indsp,constr_lengths) @@ -108,13 +108,6 @@ module PrintingCasesLet = module PrintingIf = Goptions.MakeRefTable(PrintingCasesIf) module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet) -let force_let ci = - let indsp = ci.ci_ind in - let lc = mis_constr_nargs indsp in PrintingLet.active (indsp,lc) -let force_if ci = - let indsp = ci.ci_ind in - let lc = mis_constr_nargs indsp in PrintingIf.active (indsp,lc) - (* Options for printing or not wildcard and synthetisable types *) open Goptions diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 445c2183df..588bc8c849 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -50,8 +50,6 @@ val lookup_index_as_renamed : env -> constr -> int -> int option val set_detype_anonymous : (loc -> int -> rawconstr) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool -val force_if : case_info -> bool -val force_let : case_info -> bool (* Utilities to transform kernel cases to simple pattern-matching problem *) |