From f03aaf12eb7d89fa4caa59873e114c8cd125b950 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 10 Sep 2015 11:47:21 +0200 Subject: Assertion checking that invariant enforced by 0f8d1b92 always holds. When reifying a 31-bit integer after a VM computation, we check that no bit outside the 31 LSB is set to 1. --- kernel/environ.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 109e3830c2..bf12d6c6dc 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -584,7 +584,10 @@ let dispatch = Array.init 31 (fun n -> mkConstruct (digit_ind, nth_digit_plus_one i (30-n))) in - mkApp(mkConstruct(ind, 1), array_of_int tag) + (* We check that no bit above 31 is set to one. This assertion used to + fail in the VM, and led to conversion tests failing at Qed. *) + assert (Int.equal (tag lsr 31) 0); + mkApp(mkConstruct(ind, 1), array_of_int tag) in (* subfunction which dispatches the compiling information of an -- cgit v1.2.3 From 4838a3a3c25cc9f7583dd62e4585460aca8ee961 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 21 Sep 2015 11:55:32 +0200 Subject: Forcing i > Set for global universes (incomplete) --- kernel/environ.ml | 39 +++++++++++++++++++++++++++------------ 1 file changed, 27 insertions(+), 12 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 109e3830c2..c433c07898 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -181,26 +181,41 @@ let fold_named_context_reverse f ~init env = (* Universe constraints *) -let add_constraints c env = - if Univ.Constraint.is_empty c then - env - else - let s = env.env_stratification in +let map_universes f env = + let s = env.env_stratification in { env with env_stratification = - { s with env_universes = Univ.merge_constraints c s.env_universes } } + { s with env_universes = f s.env_universes } } + +let add_constraints c env = + if Univ.Constraint.is_empty c then env + else map_universes (Univ.merge_constraints c) env let check_constraints c env = Univ.check_constraints c env.env_stratification.env_universes -let set_engagement c env = (* Unsafe *) - { env with env_stratification = - { env.env_stratification with env_engagement = c } } - let push_constraints_to_env (_,univs) env = add_constraints univs env -let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env -let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env +let add_universes strict ctx g = + let g = Array.fold_left (fun g v -> Univ.add_universe v strict g) + g (Univ.Instance.to_array (Univ.UContext.instance ctx)) + in + Univ.merge_constraints (Univ.UContext.constraints ctx) g + +let push_context ?(strict=false) ctx env = + map_universes (add_universes strict ctx) env + +let add_universes_set strict ctx g = + let g = Univ.LSet.fold (fun v g -> Univ.add_universe v strict g) + (Univ.ContextSet.levels ctx) g + in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g + +let push_context_set ?(strict=false) ctx env = + map_universes (add_universes_set strict ctx) env + +let set_engagement c env = (* Unsafe *) + { env with env_stratification = + { env.env_stratification with env_engagement = c } } (* Global constants *) -- cgit v1.2.3 From cc69a4697633e14fc00c9bd0858b38120645464b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:00:49 +0200 Subject: Univs: module constraints move to universe contexts as they might declare new universes (e.g. with). --- kernel/environ.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index c433c07898..429aba4f75 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -197,8 +197,10 @@ let push_constraints_to_env (_,univs) env = add_constraints univs env let add_universes strict ctx g = - let g = Array.fold_left (fun g v -> Univ.add_universe v strict g) - g (Univ.Instance.to_array (Univ.UContext.instance ctx)) + let g = Array.fold_left + (* Be lenient, module typing reintroduces universes and constraints due to includes *) + (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in Univ.merge_constraints (Univ.UContext.constraints ctx) g @@ -206,8 +208,9 @@ let push_context ?(strict=false) ctx env = map_universes (add_universes strict ctx) env let add_universes_set strict ctx g = - let g = Univ.LSet.fold (fun v g -> Univ.add_universe v strict g) - (Univ.ContextSet.levels ctx) g + let g = Univ.LSet.fold + (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (Univ.ContextSet.levels ctx) g in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = -- cgit v1.2.3 From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- kernel/environ.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 1cc07c0ab8..09fe64d77b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -188,10 +188,10 @@ let map_universes f env = let add_constraints c env = if Univ.Constraint.is_empty c then env - else map_universes (Univ.merge_constraints c) env + else map_universes (UGraph.merge_constraints c) env let check_constraints c env = - Univ.check_constraints c env.env_stratification.env_universes + UGraph.check_constraints c env.env_stratification.env_universes let push_constraints_to_env (_,univs) env = add_constraints univs env @@ -199,19 +199,19 @@ let push_constraints_to_env (_,univs) env = let add_universes strict ctx g = let g = Array.fold_left (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in - Univ.merge_constraints (Univ.UContext.constraints ctx) g + UGraph.merge_constraints (Univ.UContext.constraints ctx) g let push_context ?(strict=false) ctx env = map_universes (add_universes strict ctx) env let add_universes_set strict ctx g = let g = Univ.LSet.fold - (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g - in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g + in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = map_universes (add_universes_set strict ctx) env -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- kernel/environ.ml | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 09fe64d77b..da540bb051 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -24,7 +24,6 @@ open Errors open Util open Names open Term -open Context open Vars open Declarations open Pre_env @@ -70,7 +69,7 @@ let empty_context env = (* Rel context *) let lookup_rel n env = - lookup_rel n env.env_rel_context + Context.Rel.lookup n env.env_rel_context let evaluable_rel n env = match lookup_rel n env with @@ -81,7 +80,7 @@ let nb_rel env = env.env_nb_rel let push_rel = push_rel -let push_rel_context ctxt x = Context.fold_rel_context push_rel ctxt ~init:x +let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in @@ -120,7 +119,7 @@ let map_named_val f (ctxt,ctxtv) = in (map ctxt, ctxtv) -let empty_named_context = empty_named_context +let empty_named_context = Context.Named.empty let push_named = push_named let push_named_context = List.fold_right push_named @@ -130,11 +129,11 @@ let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named id env = Context.lookup_named id env.env_named_context -let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt +let lookup_named id env = Context.Named.lookup id env.env_named_context +let lookup_named_val id (ctxt,_) = Context.Named.lookup id ctxt let eq_named_context_val c1 c2 = - c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2) + c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) (* A local const is evaluable if it is defined *) @@ -153,7 +152,7 @@ let reset_with_named_context (ctxt,ctxtv) env = { env with env_named_context = ctxt; env_named_vals = ctxtv; - env_rel_context = empty_rel_context; + env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0 } @@ -176,7 +175,7 @@ let fold_named_context f env ~init = in fold_right env let fold_named_context_reverse f ~init env = - Context.fold_named_context_reverse f ~init:init (named_context env) + Context.Named.fold_inside f ~init:init (named_context env) (* Universe constraints *) @@ -389,11 +388,11 @@ let add_mind kn mib env = let lookup_constant_variables c env = let cmap = lookup_constant c env in - Context.vars_of_named_context cmap.const_hyps + Context.Named.to_vars cmap.const_hyps let lookup_inductive_variables (kn,i) env = let mis = lookup_mind kn env in - Context.vars_of_named_context mis.mind_hyps + Context.Named.to_vars mis.mind_hyps let lookup_constructor_variables (ind,_) env = lookup_inductive_variables ind env @@ -427,7 +426,7 @@ let global_vars_set env constr = contained in the types of the needed variables. *) let really_needed env needed = - Context.fold_named_context_reverse + Context.Named.fold_inside (fun need (id,copt,t) -> if Id.Set.mem id need then let globc = @@ -443,9 +442,9 @@ let really_needed env needed = let keep_hyps env needed = let really_needed = really_needed env needed in - Context.fold_named_context + Context.Named.fold_outside (fun (id,_,_ as d) nsign -> - if Id.Set.mem id really_needed then add_named_decl d nsign + if Id.Set.mem id really_needed then Context.Named.add d nsign else nsign) (named_context env) ~init:empty_named_context -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/environ.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 429aba4f75..cd376b69eb 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- kernel/environ.ml | 64 ++++++++++++++++++++++++++----------------------------- 1 file changed, 30 insertions(+), 34 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 847e1d08f9..1089dff92c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -72,9 +72,8 @@ let lookup_rel n env = Context.Rel.lookup n env.env_rel_context let evaluable_rel n env = - match lookup_rel n env with - | (_,Some _,_) -> true - | _ -> false + let open Context.Rel.Declaration in + lookup_rel n env |> is_local_def let nb_rel env = env.env_nb_rel @@ -83,7 +82,8 @@ let push_rel = push_rel let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = - let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in + let open Context.Rel.Declaration in + let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt let fold_rel_context f env ~init = @@ -107,17 +107,8 @@ let named_vals_of_val = snd (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) -let map_named_val f (ctxt,ctxtv) = - let rec map ctx = match ctx with - | [] -> [] - | (id, body, typ) :: rem -> - let body' = Option.smartmap f body in - let typ' = f typ in - let rem' = map rem in - if body' == body && typ' == typ && rem' == rem then ctx - else (id, body', typ') :: rem' - in - (map ctxt, ctxtv) +let map_named_val f = + on_fst (Context.Named.map f) let empty_named_context = Context.Named.empty @@ -138,10 +129,10 @@ let eq_named_context_val c1 c2 = (* A local const is evaluable if it is defined *) let named_type id env = - let (_,_,t) = lookup_named id env in t + lookup_named id env |> Context.Named.Declaration.get_type let named_body id env = - let (_,b,_) = lookup_named id env in b + lookup_named id env |> Context.Named.Declaration.get_value let evaluable_named id env = match named_body id env with @@ -426,15 +417,16 @@ let global_vars_set env constr = contained in the types of the needed variables. *) let really_needed env needed = + let open Context.Named.Declaration in Context.Named.fold_inside - (fun need (id,copt,t) -> - if Id.Set.mem id need then + (fun need decl -> + if Id.Set.mem (get_id decl) need then let globc = - match copt with - | None -> Id.Set.empty - | Some c -> global_vars_set env c in + match decl with + | LocalAssum _ -> Id.Set.empty + | LocalDef (_,c,_) -> global_vars_set env c in Id.Set.union - (global_vars_set env t) + (global_vars_set env (get_type decl)) (Id.Set.union globc need) else need) ~init:needed @@ -443,8 +435,9 @@ let really_needed env needed = let keep_hyps env needed = let really_needed = really_needed env needed in Context.Named.fold_outside - (fun (id,_,_ as d) nsign -> - if Id.Set.mem id really_needed then Context.Named.add d nsign + (fun d nsign -> + let open Context.Named.Declaration in + if Id.Set.mem (get_id d) really_needed then Context.Named.add d nsign else nsign) (named_context env) ~init:empty_named_context @@ -494,11 +487,12 @@ let compile_constant_body = Cbytegen.compile_constant_body false exception Hyp_not_found let apply_to_hyp (ctxt,vals) id f = + let open Context.Named.Declaration in let rec aux rtail ctxt vals = match ctxt, vals with - | (idc,c,ct as d)::ctxt, v::vals -> - if Id.equal idc id then - (f ctxt d rtail)::ctxt, v::vals + | d::ctxt, v::vals -> + if Id.equal (get_id d) id then + (f ctxt d rtail)::ctxt, v::vals else let ctxt',vals' = aux (d::rtail) ctxt vals in d::ctxt', v::vals' @@ -507,10 +501,11 @@ let apply_to_hyp (ctxt,vals) id f = in aux [] ctxt vals let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = + let open Context.Named.Declaration in let rec aux ctxt vals = match ctxt,vals with - | (idc,c,ct as d)::ctxt, v::vals -> - if Id.equal idc id then + | d::ctxt, v::vals -> + if Id.equal (get_id d) id then let sign = ctxt,vals in push_named_context_val (f d sign) sign else @@ -521,10 +516,11 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = in aux ctxt vals let insert_after_hyp (ctxt,vals) id d check = + let open Context.Named.Declaration in let rec aux ctxt vals = match ctxt, vals with - | (idc,c,ct)::ctxt', v::vals' -> - if Id.equal idc id then begin + | decl::ctxt', v::vals' -> + if Id.equal (get_id decl) id then begin check ctxt; push_named_context_val d (ctxt,vals) end else @@ -537,12 +533,12 @@ let insert_after_hyp (ctxt,vals) id d check = (* To be used in Logic.clear_hyps *) let remove_hyps ids check_context check_value (ctxt, vals) = + let open Context.Named.Declaration in let rec remove_hyps ctxt vals = match ctxt, vals with | [], [] -> [], [] | d :: rctxt, (nid, v) :: rvals -> - let (id, _, _) = d in let ans = remove_hyps rctxt rvals in - if Id.Set.mem id ids then ans + if Id.Set.mem (get_id d) ids then ans else let (rctxt', rvals') = ans in let d' = check_context d in -- cgit v1.2.3 From 4f041384cb27f0d24fa14b272884b4b7f69cacbe Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 15 Feb 2016 11:55:43 +0100 Subject: CLEANUP: Simplifying the changes done in "kernel/*" ... ... ... ... ... ... ... ... ... ... ... ... ... ... --- kernel/environ.ml | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 1089dff92c..d8493d9baf 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -27,6 +27,7 @@ open Term open Vars open Declarations open Pre_env +open Context.Rel.Declaration (* The type of environments. *) @@ -72,8 +73,7 @@ let lookup_rel n env = Context.Rel.lookup n env.env_rel_context let evaluable_rel n env = - let open Context.Rel.Declaration in - lookup_rel n env |> is_local_def + is_local_def (lookup_rel n env) let nb_rel env = env.env_nb_rel @@ -82,7 +82,6 @@ let push_rel = push_rel let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = - let open Context.Rel.Declaration in let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt @@ -128,11 +127,13 @@ let eq_named_context_val c1 c2 = (* A local const is evaluable if it is defined *) +open Context.Named.Declaration + let named_type id env = - lookup_named id env |> Context.Named.Declaration.get_type + get_type (lookup_named id env) let named_body id env = - lookup_named id env |> Context.Named.Declaration.get_value + get_value (lookup_named id env) let evaluable_named id env = match named_body id env with @@ -417,7 +418,6 @@ let global_vars_set env constr = contained in the types of the needed variables. *) let really_needed env needed = - let open Context.Named.Declaration in Context.Named.fold_inside (fun need decl -> if Id.Set.mem (get_id decl) need then @@ -436,7 +436,6 @@ let keep_hyps env needed = let really_needed = really_needed env needed in Context.Named.fold_outside (fun d nsign -> - let open Context.Named.Declaration in if Id.Set.mem (get_id d) really_needed then Context.Named.add d nsign else nsign) (named_context env) @@ -487,7 +486,6 @@ let compile_constant_body = Cbytegen.compile_constant_body false exception Hyp_not_found let apply_to_hyp (ctxt,vals) id f = - let open Context.Named.Declaration in let rec aux rtail ctxt vals = match ctxt, vals with | d::ctxt, v::vals -> @@ -501,7 +499,6 @@ let apply_to_hyp (ctxt,vals) id f = in aux [] ctxt vals let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = - let open Context.Named.Declaration in let rec aux ctxt vals = match ctxt,vals with | d::ctxt, v::vals -> @@ -516,7 +513,6 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = in aux ctxt vals let insert_after_hyp (ctxt,vals) id d check = - let open Context.Named.Declaration in let rec aux ctxt vals = match ctxt, vals with | decl::ctxt', v::vals' -> @@ -533,7 +529,6 @@ let insert_after_hyp (ctxt,vals) id d check = (* To be used in Logic.clear_hyps *) let remove_hyps ids check_context check_value (ctxt, vals) = - let open Context.Named.Declaration in let rec remove_hyps ctxt vals = match ctxt, vals with | [], [] -> [], [] | d :: rctxt, (nid, v) :: rvals -> -- cgit v1.2.3