diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh | 6 | ||||
| -rw-r--r-- | dev/include_printers | 1 | ||||
| -rw-r--r-- | dev/top_printers.dbg | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 10 | ||||
| -rw-r--r-- | dev/top_printers.mli | 1 |
5 files changed, 18 insertions, 1 deletions
diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh new file mode 100644 index 0000000000..bc8aa33565 --- /dev/null +++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then + + unicoq_CI_REF=detype-anonymous + unicoq_CI_GITURL=https://github.com/maximedenes/unicoq + +fi diff --git a/dev/include_printers b/dev/include_printers index 90088e40bf..d077075eeb 100644 --- a/dev/include_printers +++ b/dev/include_printers @@ -11,6 +11,7 @@ #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context *) ppaucontext;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; #install_printer (* univ set *) ppuniverse_set;; diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index a6ecec7e33..82f2e79549 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -62,6 +62,7 @@ install_printer Top_printers.ppuni_level install_printer Top_printers.ppuniverse_set install_printer Top_printers.ppuniverse_instance install_printer Top_printers.ppuniverse_context +install_printer Top_printers.ppaucontext install_printer Top_printers.ppuniverse_context_set install_printer Top_printers.ppuniverse_subst install_printer Top_printers.ppuniverse_opt_subst diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 816316487c..2859b56cbe 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -27,7 +27,6 @@ open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false -let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found) (* std_ppcmds *) let pp x = Pp.pp_with !Topfmt.std_ft x @@ -236,6 +235,15 @@ let ppnamedcontextval e = let sigma = Evd.from_env env in pp (pr_named_context env sigma (named_context_of_val e)) +let ppaucontext auctx = + let nas = AUContext.names auctx in + let prlev l = match Level.var_index l with + | Some n -> Name.print nas.(n) + | None -> prlev l + in + pp (pr_universe_context prlev (AUContext.repr auctx)) + + let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]") diff --git a/dev/top_printers.mli b/dev/top_printers.mli index cb32d2294c..2aa1808322 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -137,6 +137,7 @@ val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *) val ppuniverse_set : Univ.LSet.t -> unit val ppuniverse_instance : Univ.Instance.t -> unit val ppuniverse_context : Univ.UContext.t -> unit +val ppaucontext : Univ.AUContext.t -> unit val ppuniverse_context_set : Univ.ContextSet.t -> unit val ppuniverse_subst : Univ.universe_subst -> unit val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit |