diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/decls.ml | 10 | ||||
| -rw-r--r-- | library/impargs.ml | 19 | ||||
| -rw-r--r-- | library/lib.ml | 27 | ||||
| -rw-r--r-- | library/lib.mli | 3 |
4 files changed, 25 insertions, 34 deletions
diff --git a/library/decls.ml b/library/decls.ml index 6e21880f1f..2952c258a5 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -14,6 +14,8 @@ open Names open Decl_kinds open Libnames +module NamedDecl = Context.Named.Declaration + (** Datas associated to section variables and local definitions *) type variable_data = @@ -46,20 +48,18 @@ let constant_kind kn = Cmap.find kn !csttab (** Miscellaneous functions. *) -open Context.Named.Declaration - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right (fun d signv -> - let id = get_id d in - let d = if variable_opacity id then LocalAssum (id, get_type d) else d in + let id = NamedDecl.get_id d in + let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val let last_section_hyps dir = Context.Named.fold_outside (fun d sec_ids -> - let id = get_id d in + let id = NamedDecl.get_id d in try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) diff --git a/library/impargs.ml b/library/impargs.ml index bce7a15cbe..07b6b2bae3 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -22,6 +22,9 @@ open Constrexpr open Termops open Namegen open Decl_kinds +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (*s Flags governing the computation of implicit arguments *) @@ -164,7 +167,6 @@ let update pos rig (na,st) = (* modified is_rigid_reference with a truncated env *) let is_flexible_reference env bound depth f = - let open Context.Named.Declaration in match kind_of_term f with | Rel n when n >= bound+depth -> (* inductive type *) false | Rel n when n >= depth -> (* previous argument *) true @@ -173,7 +175,7 @@ let is_flexible_reference env bound depth f = let cb = Environ.lookup_constant kn env in (match cb.const_body with Def _ -> true | _ -> false) | Var id -> - Environ.lookup_named id env |> is_local_def + env |> Environ.lookup_named id |> is_local_def | Ind _ | Construct _ -> false | _ -> true @@ -449,8 +451,7 @@ let compute_all_mib_implicits flags manual kn = let compute_var_implicits flags manual id = let env = Global.env () in - let open Context.Named.Declaration in - compute_semi_auto_implicits env flags manual (get_type (lookup_named id env)) + compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env)) (* Implicits of a global reference. *) @@ -515,15 +516,11 @@ let subst_implicits (subst,(req,l)) = (ImplLocal,List.smartmap (subst_implicits_decl subst) l) let impls_of_context ctx = - let map (id, impl, _, _) = match impl with - | Implicit -> Some (id, Manual, (true, true)) + let map (decl, impl) = match impl with + | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true)) | _ -> None in - let is_set (_, _, b, _) = match b with - | None -> true - | Some _ -> false - in - List.rev_map map (List.filter is_set ctx) + List.rev_map map (List.filter (fst %> is_local_assum) ctx) let adjust_side_condition p = function | LessArgsThan n -> LessArgsThan (n+p) diff --git a/library/lib.ml b/library/lib.ml index 8880a8b154..a5a9a01942 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -13,6 +13,9 @@ open Libnames open Globnames open Nameops open Libobject +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type is_type = bool (* Module Type or just Module *) type export = bool option (* None for a Module Type *) @@ -388,7 +391,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -428,12 +431,10 @@ let add_section_context ctx = sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = - let open Context.Named.Declaration in let rec aux = function - | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) -> - let (id',b,t) = to_tuple decl in + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in - (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r + (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r | (Variable (_,_,poly,ctx)::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r ctx else r @@ -443,17 +444,11 @@ let extract_hyps (secs,ohyps) = | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) -let instance_from_variable_context sign = - let rec inst_rec = function - | (id,b,None,_) :: sign -> id :: inst_rec sign - | _ :: sign -> inst_rec sign - | [] -> [] in - Array.of_list (inst_rec sign) - -let named_of_variable_context ctx = let open Context.Named.Declaration in - List.map (function id,_,None,t -> LocalAssum (id,t) - | id,_,Some b,t -> LocalDef (id,b,t)) - ctx +let instance_from_variable_context = + List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list + +let named_of_variable_context = + List.map fst let add_section_replacement f g poly hyps = match !sectab with diff --git a/library/lib.mli b/library/lib.mli index 7080b5dba7..092643c2d8 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -162,8 +162,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) -type variable_info = Names.Id.t * Decl_kinds.binding_kind * - Term.constr option * Term.types +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t |