diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 738ade8c..aa47e261 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -109,7 +109,9 @@ let const_of_id id = qualid_of_reference (Libnames.Ident (Loc.ghost,id)) in try Constrintern.locate_reference princ_ref - with Not_found -> Errors.error ("cannot find "^ Id.to_string id) + with Not_found -> + Errors.errorlabstrm "IndFun.const_of_id" + (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = match (Term.kind_of_term t) with @@ -147,7 +149,7 @@ let get_locality = function | Global -> false let save with_clean id const (locality,_,kind) hook = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in @@ -178,9 +180,10 @@ let get_proof_clean do_reduce = let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () - and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () - in + and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in + let old_printuniverses = !Constrextern.print_universes in + Constrextern.print_universes := true; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -193,6 +196,7 @@ let with_full_print f a = Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; + Constrextern.print_universes := old_printuniverses; Dumpglob.continue (); res with @@ -201,6 +205,7 @@ let with_full_print f a = Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; + Constrextern.print_universes := old_printuniverses; Dumpglob.continue (); raise reraise |