From 836b9faa8797a2802c189e782469f8d2e467d894 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:15:05 +0200 Subject: Univs: fix evar_map leaks bugs in Function The evar_map's that are used to typecheck terms must now always be initialized with the global universe graphs using Evd.from_env, so any failure to initialize and thread evar_map's correctly results in errors. --- plugins/funind/indfun_common.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'plugins/funind/indfun_common.ml') diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1c409500ef..35bd1c36da 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -180,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; @@ -195,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 @@ -203,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 -- cgit v1.2.3 From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- plugins/funind/indfun_common.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/indfun_common.ml') diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 35bd1c36da..aa47e26192 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -149,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 -- cgit v1.2.3 From b98e4857a13a4014c65882af5321ebdb09f41890 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 17:40:10 +0100 Subject: Rename Ephemeron -> CEphemeron. Fixes compilation of Coq with OCaml 4.03 beta 1. --- plugins/funind/indfun_common.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/indfun_common.ml') diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index aa47e26192..2449678a13 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -163,7 +163,7 @@ let save with_clean id const (locality,_,kind) hook = (locality, ConstRef kn) in if with_clean then Pfedit.delete_current_proof (); - Ephemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); + CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id -- cgit v1.2.3