diff options
| author | Emilio Jesus Gallego Arias | 2019-08-18 20:27:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-19 23:03:45 +0200 |
| commit | a74e055acf48583c6fece5d22c805736679376b2 (patch) | |
| tree | bc86b65608590013d7569b9585cd37029f2fa274 /library/lib.ml | |
| parent | 7f9a08b98b1637291dda687fce92198a21ffc395 (diff) | |
[api] Move handling of variable implicit data to impargs
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/library/lib.ml b/library/lib.ml index 6b01eb07e9..3f51826315 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -441,9 +441,6 @@ let empty_section_data ~poly = { let sectab = Summary.ref ([] : section_data list) ~name:"section-context" -let sec_implicits = - Summary.ref Id.Map.empty ~name:"section-implicits" - let check_same_poly p sec = if p != sec.sec_poly then user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") @@ -452,14 +449,13 @@ 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 = +let add_section_variable ~name ~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} :: s.sec_entry } in - sectab := s :: sl; - sec_implicits := Id.Map.add name kind !sec_implicits + sectab := s :: sl let add_section_context ctx = match !sectab with @@ -576,8 +572,6 @@ let section_segment_of_reference = let open GlobRef in function let variable_section_segment_of_reference gr = (section_segment_of_reference gr).abstr_ctx -let variable_section_kind id = Id.Map.get id !sec_implicits - let section_instance = let open GlobRef in function | VarRef id -> let eq = function |