diff options
| -rw-r--r-- | library/lib.ml | 23 | ||||
| -rw-r--r-- | library/lib.mli | 2 | ||||
| -rw-r--r-- | tactics/declare.ml | 8 |
3 files changed, 16 insertions, 17 deletions
diff --git a/library/lib.ml b/library/lib.ml index cf7f97726a..fa383ab23c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -427,7 +427,6 @@ type secentry = | Variable of { id:Names.Id.t; kind:Decl_kinds.binding_kind; - univs:Univ.ContextSet.t; } | Context of Univ.ContextSet.t @@ -454,12 +453,12 @@ let add_section ~poly () = List.iter (fun tab -> check_same_poly poly tab) !sectab; sectab := empty_section_data ~poly :: !sectab -let add_section_variable ~name ~kind ~poly univs = +let add_section_variable ~name ~kind ~poly = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | s :: sl -> List.iter (fun tab -> check_same_poly poly tab) !sectab; - let s = { s with sec_entry = Variable {id=name;kind;univs} :: s.sec_entry } in + let s = { s with sec_entry = Variable {id=name;kind} :: s.sec_entry } in sectab := s :: sl let add_section_context ctx = @@ -470,31 +469,31 @@ let add_section_context ctx = let s = { s with sec_entry = Context ctx :: s.sec_entry } in sectab := s :: sl -exception PolyFound of bool (* make this a let exception once possible *) +exception PolyFound (* make this a let exception once possible *) let is_polymorphic_univ u = try let open Univ in List.iter (fun s -> let vars = s.sec_entry in List.iter (function - | Variable {univs=(univs,_)} -> - if LSet.mem u univs then raise (PolyFound s.sec_poly) + | Variable _ -> () | Context (univs,_) -> - if LSet.mem u univs then raise (PolyFound true) + if LSet.mem u univs then raise PolyFound ) vars ) !sectab; false - with PolyFound b -> b + with PolyFound -> true let extract_hyps poly (secs,ohyps) = let rec aux = function - | (Variable {id;kind;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> + | (Variable {id;kind}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in - (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r - | (Variable {univs}::idl,hyps) -> + (decl,kind) :: l, r + | (Variable _::idl,hyps) -> let l, r = aux (idl,hyps) in - l, if poly then Univ.ContextSet.union r univs else r + l, r | (Context ctx :: idl, hyps) -> + let () = assert poly in let l, r = aux (idl, hyps) in l, Univ.ContextSet.union r ctx | [], _ -> [],Univ.ContextSet.empty diff --git a/library/lib.mli b/library/lib.mli index b985c8c2bb..bfee1b16c5 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -183,7 +183,7 @@ val variable_section_segment_of_reference : GlobRef.t -> variable_context val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit +val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit diff --git a/tactics/declare.ml b/tactics/declare.ml index b8ba62a5e5..63e9279edc 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -308,12 +308,12 @@ let declare_variable ~name ~kind d = if Decls.variable_exists name then raise (AlreadyDeclared (None, name)); - let impl,opaque,poly,univs = match d with (* Fails if not well-typed *) + let impl,opaque,poly = match d with (* Fails if not well-typed *) | SectionLocalAssum {typ;univs;poly;impl} -> let () = declare_universe_context ~poly univs in let () = Global.push_named_assum (name,typ) in let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in - impl, true, poly, univs + impl, true, poly | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) @@ -338,10 +338,10 @@ let declare_variable ~name ~kind d = } in let () = Global.push_named_def (name, se) in Decl_kinds.Explicit, de.proof_entry_opaque, - poly, univs + poly in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); - add_section_variable ~name ~kind:impl ~poly univs; + add_section_variable ~name ~kind:impl ~poly; Decls.(add_variable_data name {opaque;kind}); add_anonymous_leaf (inVariable ()); Impargs.declare_var_implicits name; |