diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
commit | 3c47248abc27aa9c64120db30dcb0d7bf945bc70 (patch) | |
tree | 0dd3a804e1924862390a7f78abc9a8a119127f9c /library/lib.ml | |
parent | ceb68d1d643ac65f500e0201f61e73cf22e6e2fb (diff) | |
parent | 1bc1cba7a759a285131a3ed6ea8979716700b856 (diff) |
Merge remote-tracking branch 'github/pr/283' into trunk
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
Diffstat (limited to 'library/lib.ml')
-rw-r--r-- | library/lib.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/library/lib.ml b/library/lib.ml index 749cc4ff3..13921610d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -391,7 +391,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -399,7 +399,7 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = - | Variable of (Names.Id.t * Decl_kinds.binding_kind * + | Variable of (Names.Id.t * Decl_kinds.implicit_status * Decl_kinds.polymorphic * Univ.universe_context_set) | Context of Univ.universe_context_set @@ -416,12 +416,12 @@ let check_same_poly p vars = if List.exists pred vars then error "Cannot mix universe polymorphic and monomorphic declarations in sections." -let add_section_variable id impl poly ctx = +let add_section_variable id impl ~polymorphic ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; - sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + List.iter (fun tab -> check_same_poly polymorphic (pi1 tab)) !sectab; + sectab := (Variable (id,impl,polymorphic,ctx)::vars,repl,abs)::sl let add_section_context ctx = match !sectab with @@ -450,11 +450,11 @@ let instance_from_variable_context = let named_of_variable_context = List.map fst -let add_section_replacement f g poly hyps = +let add_section_replacement f g ~polymorphic hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> - let () = check_same_poly poly vars in + let () = check_same_poly polymorphic vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in @@ -462,13 +462,13 @@ let add_section_replacement f g poly hyps = sectab := (vars,f (Univ.UContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl -let add_section_kn poly kn = +let add_section_kn ~polymorphic kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f poly + add_section_replacement f f ~polymorphic -let add_section_constant poly kn = +let add_section_constant ~polymorphic kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f poly + add_section_replacement f f ~polymorphic let replacement_context () = pi2 (List.hd !sectab) |