diff options
| author | Pierre-Marie Pédrot | 2019-07-11 11:15:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-18 17:01:33 +0200 |
| commit | 8dbdc3aab8e1f905522ec317fcdad5df82c93087 (patch) | |
| tree | ba35718041c999dc71215949321d9c0ecc36a21d /library/lib.ml | |
| parent | c13a3b61c9b1a714c50bcf0ec371a4effe1ff627 (diff) | |
Remove dead code in Lib.
The polymorphic flag is now carried by the section rather than individual
variables, no need to pass it along.
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/library/lib.ml b/library/lib.ml index c4eed7b216..59b55cc16b 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; - poly:bool; univs:Univ.ContextSet.t; } | Context of Univ.ContextSet.t @@ -462,7 +461,7 @@ let add_section_variable ~name ~kind ~poly univs = | [] -> () (* 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;poly;univs} :: s.sec_entry } in + let s = { s with sec_entry = Variable {id=name;kind;univs} :: s.sec_entry } in sectab := s :: sl let add_section_context ctx = @@ -480,8 +479,8 @@ let is_polymorphic_univ u = List.iter (fun s -> let vars = s.sec_entry in List.iter (function - | Variable {poly;univs=(univs,_)} -> - if LSet.mem u univs then raise (PolyFound poly) + | Variable {univs=(univs,_)} -> + if LSet.mem u univs then raise (PolyFound s.sec_poly) | Context (univs,_) -> if LSet.mem u univs then raise (PolyFound true) ) vars @@ -489,12 +488,12 @@ let is_polymorphic_univ u = false with PolyFound b -> b -let extract_hyps (secs,ohyps) = +let extract_hyps poly (secs,ohyps) = let rec aux = function - | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> + | (Variable {id;kind;univs}::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 {poly;univs}::idl,hyps) -> + | (Variable {univs}::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r univs else r | (Context ctx :: idl, hyps) -> @@ -528,7 +527,7 @@ let add_section_replacement f g poly hyps = | [] -> () | s :: sl -> let () = check_same_poly poly s in - let sechyps,ctx = extract_hyps (s.sec_entry, hyps) in + let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in let ctx = Univ.ContextSet.to_context ctx in let inst = Univ.UContext.instance ctx in let nas = name_instance inst in |