diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 24 |
1 files changed, 15 insertions, 9 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f8ec05fdb..161e0c535 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1591,13 +1591,14 @@ let vernac_declare_reduction ~atts s r = let vernac_global_check c = let env = Global.env() in let sigma = Evd.from_env env in - let c,ctx = interp_constr env sigma c in + let c,uctx = interp_constr env sigma c in let senv = Global.safe_env() in - let cstrs = snd (UState.context_set ctx) in - let senv = Safe_typing.add_constraints cstrs senv in + let uctx = UState.context_set uctx in + let senv = Safe_typing.push_context_set false uctx senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - Feedback.msg_notice (print_safe_judgment env sigma j) + Feedback.msg_notice (print_safe_judgment env sigma j ++ + pr_universe_ctx_set sigma uctx) let get_nth_goal n = @@ -1656,13 +1657,13 @@ let vernac_print ~atts env sigma = | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) | PrintDebugGC -> msg_notice (Mltop.print_gc ()) | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) - | PrintGraph -> msg_notice (Prettyp.print_graph()) + | PrintGraph -> msg_notice (Prettyp.print_graph env sigma) | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) | PrintCoercionPaths (cls,clt) -> - msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) + msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) | PrintUniverses (b, dst) -> let univ = Global.universes () in @@ -1696,7 +1697,7 @@ let vernac_print ~atts env sigma = let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in - msg_notice (Printer.pr_assumptionset (Global.env ()) nassums) + msg_notice (Printer.pr_assumptionset env sigma nassums) | PrintStrategy r -> print_strategy r let global_module r = @@ -2268,5 +2269,10 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = comments on the PR *) let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; - interp ?verbosely ?proof ~st cmd; - Vernacstate.freeze_interp_state `No + try + interp ?verbosely ?proof ~st cmd; + Vernacstate.freeze_interp_state `No + with exn -> + let exn = CErrors.push exn in + Vernacstate.invalidate_cache (); + iraise exn |