diff options
74 files changed, 482 insertions, 411 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index bd86f4bd2..fcb429aef 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -18,6 +18,9 @@ open Environ open Evd open Sigma.Notations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let safe_evar_value sigma ev = try Some (Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None @@ -161,11 +164,11 @@ let is_ground_term evd t = not (has_undefined_evars evd t) let is_ground_env evd env = - let open Context.Rel.Declaration in + let open RelDecl in let is_ground_rel_decl = function | LocalDef (_,b,_) -> is_ground_term evd b | _ -> true in - let open Context.Named.Declaration in + let open NamedDecl in let is_ground_named_decl = function | LocalDef (_,b,_) -> is_ground_term evd b | _ -> true in @@ -249,11 +252,10 @@ let non_instantiated sigma = (************************) let make_pure_subst evi args = - let open Context.Named.Declaration in snd (List.fold_right (fun decl (args,l) -> match args with - | a::rest -> (rest, (get_id decl, a)::l) + | a::rest -> (rest, (NamedDecl.get_id decl, a)::l) | _ -> anomaly (Pp.str "Instance does not match its signature")) (evar_filtered_context evi) (Array.rev_to_list args,[])) @@ -327,10 +329,10 @@ let push_var id (n, s) = let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = let open Context.Named.Declaration in let replace_var_named_declaration id0 id decl = - let id' = get_id decl in + let id' = NamedDecl.get_id decl in let id' = if Id.equal id0 id' then id else id' in let vsubst = [id0 , mkVar id] in - decl |> set_id id' |> map_constr (replace_vars vsubst) + decl |> NamedDecl.set_id id' |> NamedDecl.map_constr (replace_vars vsubst) in let extract_if_neq id = function | Anonymous -> None @@ -551,8 +553,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = let () = Id.Map.iter check ri in (* No dependency at all, we can keep this ev's context hyp *) (ri, true::filter) - with Depends id -> let open Context.Named.Declaration in - (Id.Map.add (get_id h) id ri, false::filter)) + with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter)) ctxt (Array.to_list l) (Id.Map.empty,[]) in (* Check if some rid to clear in the context of ev has dependencies in the type of ev and adjust the source of the dependency *) @@ -591,10 +592,9 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = let terms = List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in let nhyps = - let open Context.Named.Declaration in let check_context decl = - let err = OccurHypInSimpleClause (Some (get_id decl)) in - map_constr (check_and_clear_in_constr env evdref err ids global) decl + let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in + NamedDecl.map_constr (check_and_clear_in_constr env evdref err ids global) decl in let check_value vk = match force_lazy_val vk with | None -> vk @@ -633,8 +633,8 @@ let process_dependent_evar q acc evm is_dependent e = hypotheses), they are all dependent. *) queue_term q true evi.evar_concl; List.iter begin fun decl -> - let open Context.Named.Declaration in - queue_term q true (get_type decl); + let open NamedDecl in + queue_term q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () | LocalDef (_,b,_) -> queue_term q true b @@ -688,9 +688,8 @@ let undefined_evars_of_term evd t = evrec Evar.Set.empty t let undefined_evars_of_named_context evd nc = - let open Context.Named.Declaration in Context.Named.fold_outside - (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) + (NamedDecl.fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) nc ~init:Evar.Set.empty diff --git a/engine/evd.ml b/engine/evd.ml index 6ba8a5112..499551406 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -16,7 +16,9 @@ open Vars open Termops open Environ open Globnames -open Context.Named.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (** Generic filters *) module Filter : @@ -226,7 +228,7 @@ let evar_instance_array test_id info args = if i < len then let c = Array.unsafe_get args i in if test_id d c then instrec filter ctxt (succ i) - else (get_id d, c) :: instrec filter ctxt (succ i) + else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in @@ -235,7 +237,7 @@ let evar_instance_array test_id info args = let map i d = if (i < len) then let c = Array.unsafe_get args i in - if test_id d c then None else Some (get_id d, c) + if test_id d c then None else Some (NamedDecl.get_id d, c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -243,7 +245,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array (isVarId % get_id) info args + evar_instance_array (isVarId % NamedDecl.get_id) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -681,7 +683,7 @@ let restrict evk filter ?candidates evd = evar_extra = Store.empty } in let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in let ctxt = Filter.filter_list filter (evar_context evar_info) in - let id_inst = Array.map_of_list (mkVar % get_id) ctxt in + let id_inst = Array.map_of_list (mkVar % NamedDecl.get_id) ctxt in let body = mkEvar(evk',id_inst) in let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; @@ -746,7 +748,7 @@ let evars_of_named_context nc = List.fold_right (fun decl s -> Option.fold_left (fun s t -> Evar.Set.union s (evars_of_term t)) - (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl)) + (Evar.Set.union s (evars_of_term (NamedDecl.get_type decl))) (NamedDecl.get_value decl)) nc Evar.Set.empty let evars_of_filtered_evar_info evi = @@ -1283,8 +1285,8 @@ let pr_meta_map mmap = prlist pr_meta_binding (metamap_to_list mmap) let pr_decl (decl,ok) = - let id = get_id decl in - match get_value decl with + let id = NamedDecl.get_id decl in + match NamedDecl.get_value decl with | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ print_constr c ++ str (if ok then ")" else "}") @@ -1401,9 +1403,8 @@ let print_env_short env = let pr_body n = function | None -> pr_name n | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in - let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in - let pr_rel_decl decl = let open Context.Rel.Declaration in - pr_body (get_name decl) (get_value decl) in + let pr_named_decl decl = pr_body (Name (NamedDecl.get_id decl)) (NamedDecl.get_value decl) in + let pr_rel_decl decl = pr_body (RelDecl.get_name decl) (RelDecl.get_value decl) in let nc = List.rev (named_context env) in let rc = List.rev (rel_context env) in str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++ diff --git a/engine/namegen.ml b/engine/namegen.ml index 638adea5d..1497dbda8 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -24,6 +24,8 @@ open Environ open Termops open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (**********************************************************************) (* Conventional names *) @@ -295,10 +297,10 @@ let make_all_name_different env = let avoid = ref (ids_of_named_context (named_context env)) in process_rel_context (fun decl newenv -> - let na = named_hd newenv (get_type decl) (get_name decl) in + let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in avoid := id::!avoid; - push_rel (set_name (Name id) decl) newenv) + push_rel (RelDecl.set_name (Name id) decl) newenv) env (* 5- Looks for next fresh name outside a list; avoids also to use names that diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 10cfbe58f..4d9386b9d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -21,6 +21,8 @@ open Libobject open Nameops open Misctypes open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*i*) let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" @@ -198,7 +200,7 @@ let combine_params avoid fn applied needed = List.partition (function (t, Some (loc, ExplByName id)) -> - let is_id (_, decl) = match get_name decl with + let is_id (_, decl) = match RelDecl.get_name decl with | Name id' -> Id.equal id id' | Anonymous -> false in @@ -242,7 +244,7 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, decl) -> - let id' = next_name_away_from (get_name decl) avoid in + let id' = next_name_away_from (RelDecl.get_name decl) avoid in (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) let destClassApp cl = diff --git a/interp/notation.ml b/interp/notation.ml index 3e3523d76..6279622bf 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -20,6 +20,9 @@ open Notation_term open Glob_term open Glob_ops open Ppextend +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (*i*) (*s A scope is a set of notations; it includes @@ -686,7 +689,6 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) = let n = try let vars = Lib.variable_section_segment_of_reference r in - let open Context.Named.Declaration in vars |> List.map fst |> List.filter is_local_assum |> List.length with Not_found (* Not a ref defined in this section *) -> 0 in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 134599150..db09e5ed7 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -21,6 +21,8 @@ open Declarations open Environ open Univ +module NamedDecl = Context.Named.Declaration + (*s Cooking the constants. *) let pop_dirpath p = match DirPath.repr p with @@ -202,8 +204,7 @@ let cook_constant env { from = cb; info } = in let const_hyps = Context.Named.fold_outside (fun decl hyps -> - let open Context.Named.Declaration in - List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl'))) + List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index acd73d97d..3177b5fae 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -22,6 +22,8 @@ open Declarations open Pre_env open Cbytegen +module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" @@ -189,18 +191,14 @@ and slot_for_fv env fv = let nv = Pre_env.lookup_named_val id env in begin match force_lazy_val nv with | None -> - let open Context.Named in - let open Declaration in - env.env_named_context |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun + env.env_named_context |> Context.Named.lookup id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> let rv = Pre_env.lookup_rel_val i env in begin match force_lazy_val rv with | None -> - let open Context.Rel in - let open Declaration in - env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVuniv_var idu -> diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 211e5e062..8943de404 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -9,7 +9,8 @@ open Declarations open Mod_subst open Util -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -94,7 +95,7 @@ let is_opaque cb = match cb.const_body with (** {7 Constant substitutions } *) let subst_rel_declaration sub = - map_constr (subst_mps sub) + RelDecl.map_constr (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) @@ -146,7 +147,7 @@ let subst_const_body sub cb = themselves. But would it really bring substantial gains ? *) let hcons_rel_decl = - map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons + RelDecl.map_type Term.hcons_types % RelDecl.map_value Term.hcons_constr % RelDecl.map_name Names.Name.hcons let hcons_rel_context l = List.smartmap hcons_rel_decl l diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index bd91c689d..dce4e9307 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -18,6 +18,9 @@ open Reduction open Inductive open Type_errors +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y let conv_leq_vecti env v1 v2 = @@ -73,8 +76,7 @@ let judge_of_type u = let judge_of_relative env n = try - let open Context.Rel.Declaration in - env |> lookup_rel n |> get_type |> lift n + env |> lookup_rel n |> RelDecl.get_type |> lift n with Not_found -> error_unbound_rel env n @@ -92,9 +94,8 @@ let judge_of_variable env id = let check_hyps_inclusion env f c sign = Context.Named.fold_outside (fun decl () -> - let open Context.Named.Declaration in - let id = get_id decl in - let ty1 = get_type decl in + let id = NamedDecl.get_id decl in + let ty1 = NamedDecl.get_type decl in try let ty2 = named_type id env in if not (eq_constr ty2 ty1) then raise Exit diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index e2f43b93e..3864df6c9 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1832,10 +1832,9 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named))) and compile_rel env sigma univ auxdefs n = - let open Context.Rel in - let n = length env.env_rel_context - n in - let open Declaration in - match lookup n env.env_rel_context with + let n = Context.Rel.length env.env_rel_context - n in + let open Context.Rel.Declaration in + match Context.Rel.lookup n env.env_rel_context with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 91b40be7e..366f9a0a6 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -14,6 +14,8 @@ open Pre_env open Nativevalues open Nativeinstr +module RelDecl = Context.Rel.Declaration + (** This file defines the lambda code generation phase of the native compiler *) exception NotClosed @@ -727,8 +729,7 @@ let optimize lam = let lambda_of_constr env sigma c = set_global_env env; let env = Renv.make () in - let open Context.Rel.Declaration in - let ids = List.rev_map get_name !global_env.env_rel_context in + let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env sigma c in (* if Flags.vm_draw_opt () then begin diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 5afefeebd..fefc3222d 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -17,7 +17,8 @@ open Util open Names open Term open Declarations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* The type of environments. *) @@ -127,7 +128,7 @@ let env_of_rel n env = let push_named_context_val d (ctxt,vals) = let rval = ref VKnone in - Context.Named.add d ctxt, (get_id d,rval)::vals + Context.Named.add d ctxt, (NamedDecl.get_id d,rval)::vals let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); @@ -135,7 +136,7 @@ let push_named d env = let rval = ref VKnone in { env_globals = env.env_globals; env_named_context = Context.Named.add d env.env_named_context; - env_named_vals = (get_id d, rval) :: env.env_named_vals; + env_named_vals = (NamedDecl.get_id d, rval) :: env.env_named_vals; env_rel_context = env.env_rel_context; env_rel_val = env.env_rel_val; env_nb_rel = env.env_nb_rel; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 09f7bd75c..f176ca579 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -62,6 +62,8 @@ open Names open Declarations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** {6 Safe environments } Fields of [safe_environment] : @@ -361,7 +363,7 @@ let check_required current_libs needed = cost too much. *) let safe_push_named d env = - let id = get_id d in + let id = NamedDecl.get_id d in let _ = try let _ = Environ.lookup_named id env in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 749b5dbaf..e59a17d12 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -22,6 +22,8 @@ open Entries open Typeops open Fast_typeops +module NamedDecl = Context.Named.Declaration + let constrain_type env j poly subst = function | `None -> if not poly then (* Old-style polymorphism *) @@ -254,13 +256,12 @@ let global_vars_set_constant_type env = function ctx ~init:Id.Set.empty let record_aux env s_ty s_bo suggested_expr = - let open Context.Named.Declaration in let in_ty = keep_hyps env s_ty in let v = String.concat " " (CList.map_filter (fun decl -> - let id = get_id decl in - if List.exists (Id.equal id % get_id) in_ty then None + let id = NamedDecl.get_id decl in + if List.exists (Id.equal id % NamedDecl.get_id) in_ty then None else Some (Id.to_string id)) (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr) @@ -269,9 +270,8 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = - let open Context.Named.Declaration in let check declared inferred = - let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in + let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Idset.diff inferred_set declared_set) in @@ -283,12 +283,12 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in let sort evn l = List.filter (fun decl -> - let id = get_id decl in - List.exists (Names.Id.equal id % get_id) l) + let id = NamedDecl.get_id decl in + List.exists (Names.Id.equal id % NamedDecl.get_id) l) (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (named_context env) in match ctx with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: @@ -482,8 +482,7 @@ let translate_local_def mb env id centry = | Undef _ -> () | Def _ -> () | OpaqueDef lc -> - let open Context.Named.Declaration in - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (named_context env) in let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Opaqueproof.force_proof (opaque_tables env) lc) in diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0059111c0..24018ab31 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -20,6 +20,9 @@ open Inductive open Type_errors open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y let conv_leq_vecti env v1 v2 = @@ -79,7 +82,7 @@ let judge_of_type u = let judge_of_relative env n = try - let typ = get_type (lookup_rel n env) in + let typ = RelDecl.get_type (lookup_rel n env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> @@ -102,7 +105,7 @@ let check_hyps_inclusion env c sign = Context.Named.fold_outside (fun d1 () -> let open Context.Named.Declaration in - let id = get_id d1 in + let id = NamedDecl.get_id d1 in try let d2 = lookup_named id env in conv env (get_type d2) (get_type d1); diff --git a/kernel/vars.ml b/kernel/vars.ml index 2ca749d50..b27e27fda 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -8,7 +8,8 @@ open Names open Esubst -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*********************) (* Occurring *) @@ -160,14 +161,15 @@ let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c -let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r -let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r -let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r +let substnl_decl laml k r = RelDecl.map_constr (fun c -> substnl laml k c) r +let substl_decl laml r = RelDecl.map_constr (fun c -> substnl laml 0 c) r +let subst1_decl lam r = RelDecl.map_constr (fun c -> subst1 lam c) r (* Build a substitution from an instance, inserting missing let-ins *) let subst_of_rel_context_instance sign l = let rec aux subst sign l = + let open RelDecl in match sign, l with | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args' | LocalDef (_,c,_)::sign', args' -> diff --git a/library/decls.ml b/library/decls.ml index 6e21880f1..2952c258a 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 cda1a662b..e922ab773 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 @@ -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,13 +516,11 @@ let subst_implicits (subst,(req,l)) = (ImplLocal,List.smartmap (subst_implicits_decl subst) l) let impls_of_context ctx = - let open Context.Named.Declaration in let map (decl, impl) = match impl with - | Implicit -> Some (get_id decl, Manual, (true, true)) + | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true)) | _ -> None in - let is_set = is_local_assum % fst in - List.rev_map map (List.filter is_set ctx) + List.rev_map map (List.filter (is_local_assum % fst) ctx) let adjust_side_condition p = function | LessArgsThan n -> LessArgsThan (n+p) diff --git a/library/lib.ml b/library/lib.ml index 7fc3e0d9c..412772e8a 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 *) @@ -428,9 +431,8 @@ 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) -> + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r | (Variable (_,_,poly,ctx)::idl,hyps) -> @@ -443,8 +445,7 @@ let extract_hyps (secs,ohyps) = in aux (secs,ohyps) let instance_from_variable_context = - let open Context.Named.Declaration in - Array.of_list % List.map get_id % List.filter is_local_assum % List.map fst + Array.of_list % List.map NamedDecl.get_id % List.filter is_local_assum % List.map fst let named_of_variable_context = List.map fst diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml index 30aeba3bb..c5b26e6d5 100644 --- a/ltac/evar_tactics.ml +++ b/ltac/evar_tactics.ml @@ -18,6 +18,8 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (* The instantiate tactic *) let instantiate_evar evk (ist,rawc) sigma = @@ -48,7 +50,7 @@ let instantiate_tac n c ido = | _ -> error "Please be more specific: in type or value?") | InHypTypeOnly -> - evar_list (get_type decl) + evar_list (NamedDecl.get_type decl) | InHypValueOnly -> (match decl with | LocalDef (_,body,_) -> evar_list body diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 7acad20d2..ad052cdd1 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -36,6 +36,9 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration + (** Typeclass-based generalized rewriting. *) (** Constants used by the tactic. *) @@ -1527,7 +1530,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let rec insert_dependent env decl accu hyps = match hyps with | [] -> List.rev_append accu [decl] | ndecl :: rem -> - if occur_var_in_decl env (get_id ndecl) decl then + if occur_var_in_decl env (NamedDecl.get_id ndecl) decl then List.rev_append accu (decl :: hyps) else insert_dependent env decl (ndecl :: accu) rem @@ -1537,17 +1540,17 @@ let assert_replacing id newt tac = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let ctx = Environ.named_context env in - let after, before = List.split_when (Id.equal id % get_id) ctx in + let after, before = List.split_when (Id.equal id % NamedDecl.get_id) ctx in let nc = match before with | [] -> assert false - | d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem + | d :: rem -> insert_dependent env (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Refine.refine ~unsafe:false { run = begin fun sigma -> let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in let map d = - let n = get_id d in + let n = NamedDecl.get_id d in if Id.equal n id then ev' else mkVar n in let (e, _) = destEvar ev in @@ -2088,9 +2091,8 @@ let setoid_proof ty fn fallback = begin try let rel, _, _ = decompose_app_rel env sigma concl in - let open Context.Rel.Declaration in let (sigma, t) = Typing.type_of env sigma rel in - let car = get_type (List.hd (fst (Reduction.dest_prod env t))) in + let car = RelDecl.get_type (List.hd (fst (Reduction.dest_prod env t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel with e -> Proofview.tclZERO e diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 6a28723b8..8e6c7a70d 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -32,6 +32,9 @@ open Misctypes open Sigma.Notations open Context.Named.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* Strictness option *) let clear ids { it = goal; sigma } = @@ -247,7 +250,7 @@ let close_previous_case pts = let filter_hyps f gls = let filter_aux id = - let id = get_id id in + let id = NamedDecl.get_id id in if f id then tclIDTAC else @@ -357,8 +360,7 @@ let enstack_subsubgoals env se stack gls= let nlast=succ last in let (llast,holes,metas) = meta_aux nlast (mkMeta nlast :: lenv) q in - let open Context.Rel.Declaration in - (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in + (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in let (nlast,holes,nmetas) = meta_aux se.se_last_meta [] (List.rev rc) in let refiner = applist (appterm,List.rev holes) in @@ -822,7 +824,7 @@ let define_tac id args body gls = let cast_tac id_or_thesis typ gls = match id_or_thesis with | This id -> - Proofview.V82.of_tactic (pf_get_hyp gls id |> set_id id |> set_type typ |> convert_hyp) gls + Proofview.V82.of_tactic (pf_get_hyp gls id |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 58744b575..b34a36492 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -15,7 +15,8 @@ open Tacmach open Util open Declarations open Globnames -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration let qflag=ref true @@ -141,7 +142,7 @@ let build_atoms gl metagen side cciterm = end; let v = ind_hyps 0 i l gl in let g i _ decl = - build_rec env polarity (lift i (get_type decl)) in + build_rec env polarity (lift i (RelDecl.get_type decl)) in let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) @@ -152,7 +153,7 @@ let build_atoms gl metagen side cciterm = let var=mkMeta (metagen true) in let v =(ind_hyps 1 i l gl).(0) in let g i _ decl = - build_rec (var::env) polarity (lift i (get_type decl)) in + build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in @@ -225,7 +226,7 @@ let build_formula side nam typ gl metagen= | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in + let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index ffb63af07..7ffc78928 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -19,7 +19,8 @@ open Formula open Sequent open Globnames open Locus -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -36,12 +37,12 @@ let wrap n b continue seq gls= match nc with []->anomaly (Pp.str "Not the expected number of hyps") | nd::q-> - let id = get_id nd in + let id = NamedDecl.get_id nd in if occur_var env id (pf_concl gls) || List.exists (occur_var_in_decl env id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in + add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b0ffc775b..f47ab2616 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -16,6 +16,8 @@ open Libnames open Globnames open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* let msgnl = Pp.msgnl *) (* @@ -307,7 +309,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun)) + (Termops.pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -938,7 +940,7 @@ let generalize_non_dep hyp g = ((* observe_tac "thin" *) (thin to_revert)) g -let id_of_decl decl = Nameops.out_name (get_name decl) +let id_of_decl decl = Nameops.out_name (RelDecl.get_name decl) let var_of_decl decl = mkVar (id_of_decl decl) let revert idl = tclTHEN @@ -1072,7 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (Name new_id) ) in - let fresh_decl = map_name fresh_id in + let fresh_decl = RelDecl.map_name fresh_id in let princ_info : elim_scheme = { princ_info with params = List.map fresh_decl princ_info.params; @@ -1119,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ) in observe (str "full_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) + prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl))) full_params ); observe (str "princ_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) + prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl))) princ_params ); observe (str "fbody_with_full_params := " ++ @@ -1165,7 +1167,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let pte_to_fix,rev_info = List.fold_left_i (fun i (acc_map,acc_info) decl -> - let pte = get_name decl in + let pte = RelDecl.get_name decl in let infos = info_array.(i) in let type_args,_ = decompose_prod infos.types in let nargs = List.length type_args in @@ -1277,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (do_replace evd full_params (fix_info.idx + List.length princ_params) - (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params)) + (args_id@(List.map (fun decl -> Nameops.out_name (RelDecl.get_name decl)) princ_params)) (all_funs.(fix_info.num_in_block)) fix_info.num_in_block all_funs diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5e72b8672..234c3e75e 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -14,6 +14,8 @@ open Functional_principles_proofs open Misctypes open Sigma.Notations +module RelDecl = Context.Rel.Declaration + exception Toberemoved_with_rel of int*constr exception Toberemoved @@ -38,7 +40,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Name x -> let id = Namegen.next_ident_away x avoid in Hashtbl.add tbl id x; - set_name (Name id) decl :: change_predicates_names (id::avoid) predicates + RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates | Anonymous -> anomaly (Pp.str "Anonymous property binder ")) in let avoid = (Termops.ids_of_context env_with_params ) in @@ -51,7 +53,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) let change_predicate_sort i decl = let new_sort = sorts.(i) in - let args,_ = decompose_prod (get_type decl) in + let args,_ = decompose_prod (RelDecl.get_type decl) in let real_args = if princ_type_info.indarg_in_concl then List.tl args diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 02fe6ce3a..4d02c77c8 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -366,7 +366,6 @@ let add_pat_variables pat typ env : Environ.env = Context.Rel.fold_outside (fun decl (env,ctxt) -> let open Context.Rel.Declaration in - (*let _,v,t = Context.Rel.Declaration.to_tuple decl in*) match decl with | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false | LocalAssum (Name id, t) -> @@ -415,8 +414,7 @@ let rec pattern_to_term_and_type env typ = function in let constructors = Inductiveops.get_constructors env indf in let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in - let open Context.Rel.Declaration in - let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in let _,cstl = Inductiveops.dest_ind_family indf in let csta = Array.of_list cstl in let implicit_args = @@ -615,7 +613,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in let new_env = - let open Context.Named.Declaration in match n with Anonymous -> env | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env @@ -989,8 +986,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (fun acc var_as_constr arg -> if isRel var_as_constr then - let open Context.Rel.Declaration in - let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in + let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in match na with | Anonymous -> acc | Name id' -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 18817f504..51cf7f4f4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,4 +1,3 @@ -open Context.Rel.Declaration open CErrors open Util open Names @@ -13,11 +12,13 @@ open Misctypes open Decl_kinds open Sigma.Notations +module RelDecl = Context.Rel.Declaration + let is_rec_info scheme_info = let test_branche min acc decl = acc || ( let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in let free_rels_in_br = Termops.free_rels new_branche in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 26fc88a60..0178c44d0 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -23,6 +23,8 @@ open Misctypes open Termops open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* Some pretty printing function for debugging purpose *) let pr_binding prc = @@ -137,7 +139,7 @@ let generate_type evd g_to_f f graph i = let fun_ctxt,res_type = match ctxt with | [] | [_] -> anomaly (Pp.str "Not a valid context") - | decl :: fun_ctxt -> fun_ctxt, get_type decl + | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl in let rec args_from_decl i accu = function | [] -> accu @@ -148,7 +150,7 @@ let generate_type evd g_to_f f graph i = args_from_decl (succ i) (t :: accu) l in (*i We need to name the vars [res] and [fv] i*) - let filter = fun decl -> match get_name decl with + let filter = fun decl -> match RelDecl.get_name decl with | Name id -> Some id | Anonymous -> None in @@ -269,7 +271,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun decl -> List.map (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) - (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl))))) + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (RelDecl.get_type decl))))) ) branches in @@ -399,7 +401,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes | hres::res::decl::ctxt -> let res = Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) - (LocalAssum (get_name decl, get_type decl) :: ctxt) + (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt) in res ) @@ -415,7 +417,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let params_bindings,avoid = List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -425,7 +427,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -682,7 +684,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (fun decl -> List.map (fun id -> id) - (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl))) + (generate_fresh_id (Id.of_string "y") ids (nb_prod (RelDecl.get_type decl))) ) branches in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index de4210af5..d9933cf41 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -26,6 +26,8 @@ open Glob_termops open Decl_kinds open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (** {1 Utilities} *) (** {2 Useful operations on constr and glob_constr} *) @@ -137,7 +139,7 @@ let showind (id:Id.t) = let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in List.iter (fun decl -> print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":"); - prconstr (get_type decl); print_string "\n") + prconstr (RelDecl.get_type decl); print_string "\n") ib1.mind_arity_ctxt; Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1); Array.iteri @@ -460,12 +462,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in let _ = prstr "\notherprms1:\n" in let _ = - List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); - prconstr (get_type decl); prstr "\n") + List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); + prconstr (RelDecl.get_type decl); prstr "\n") otherprms1 in let _ = prstr "\notherprms2:\n" in let _ = - List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n") + List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n") otherprms2 in { ident=id; @@ -827,7 +829,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = List.fold_left (fun (acc,env) decl -> let nm = Context.Rel.Declaration.get_name decl in - let c = get_type decl in + let c = RelDecl.get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in let newenv = Environ.push_rel (LocalAssum (nm,c)) env in CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index c5c44ef20..1afc6500b 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -30,6 +30,7 @@ open Misctypes open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -1697,8 +1698,8 @@ let destructure_hyps = let rec loop = function | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) | decl::lit -> - let i = get_id decl in - begin try match destructurate_prop (get_type decl) with + let i = NamedDecl.get_id decl in + begin try match destructurate_prop (NamedDecl.get_type decl) with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> @@ -1808,13 +1809,13 @@ let destructure_hyps = match destructurate_type (pf_nf typ) with | Kapp(Nat,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) - decl)) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + decl)) (loop lit)) | Kapp(Z,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) - decl)) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + decl)) (loop lit)) | _ -> loop lit end diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index fe1073762..ff6b33c49 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -13,6 +13,8 @@ open Term open Environ open Util open Libobject + +module NamedDecl = Context.Named.Declaration (*i*) let name_table = @@ -48,8 +50,7 @@ let discharge_rename_args = function (try let vars,_,_ = section_segment_of_reference c in let c' = pop_global_reference c in - let open Context.Named.Declaration in - let var_names = List.map (Name.mk_name % get_id % fst) vars in + let var_names = List.map (Name.mk_name % NamedDecl.get_id % fst) vars in let names' = List.map (fun l -> var_names @ l) names in Some (ReqGlobal (c', names), (c', names')) with Not_found -> Some req) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fe2b0a5a1..2d8173f94 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -32,6 +32,9 @@ open Evd open Sigma.Notations open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* Pattern-matching errors *) type pattern_matching_error = @@ -605,7 +608,7 @@ let relocate_index_tomatch n1 n2 = NonDepAlias :: genrec depth rest | Abstract (i,d) :: rest -> let i = relocate_rel n1 n2 depth i in - Abstract (i, map_constr (relocate_index n1 n2 depth) d) + Abstract (i, RelDecl.map_constr (relocate_index n1 n2 depth) d) :: genrec (depth+1) rest in genrec 0 @@ -638,7 +641,7 @@ let replace_tomatch n c = | NonDepAlias :: rest -> NonDepAlias :: replrec depth rest | Abstract (i,d) :: rest -> - Abstract (i, map_constr (replace_term n c depth) d) + Abstract (i, RelDecl.map_constr (replace_term n c depth) d) :: replrec (depth+1) rest in replrec 0 @@ -663,7 +666,7 @@ let rec liftn_tomatch_stack n depth = function NonDepAlias :: liftn_tomatch_stack n depth rest | Abstract (i,d)::rest -> let i = if i<depth then i else i+n in - Abstract (i, map_constr (liftn n depth) d) + Abstract (i, RelDecl.map_constr (liftn n depth) d) ::(liftn_tomatch_stack n (depth+1) rest) let lift_tomatch_stack n = liftn_tomatch_stack n 1 @@ -731,7 +734,7 @@ let get_names env sign eqns = (* We now replace the names y1 .. yn y by the actual names *) (* xi1 .. xin xi to be found in the i-th clause of the matrix *) -let recover_initial_subpattern_names = List.map2 set_name +let recover_initial_subpattern_names = List.map2 RelDecl.set_name let recover_and_adjust_alias_names names sign = let rec aux = function @@ -756,11 +759,11 @@ let push_rels_eqn_with_names sign eqn = push_rels_eqn sign eqn let push_generalized_decl_eqn env n decl eqn = - match get_name decl with + match RelDecl.get_name decl with | Anonymous -> push_rels_eqn [decl] eqn | Name _ -> - push_rels_eqn [set_name (get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn + push_rels_eqn [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn let drop_alias_eqn eqn = { eqn with alias_stack = List.tl eqn.alias_stack } @@ -768,7 +771,7 @@ let drop_alias_eqn eqn = let push_alias_eqn alias eqn = let aliasname = List.hd eqn.alias_stack in let eqn = drop_alias_eqn eqn in - let alias = set_name aliasname alias in + let alias = RelDecl.set_name aliasname alias in push_rels_eqn [alias] eqn (**********************************************************************) @@ -1195,7 +1198,7 @@ let rec generalize_problem names pb = function | LocalDef (Anonymous,_,_) -> pb', deps | _ -> (* for better rendering *) - let d = map_type (whd_betaiota !(pb.evdref)) d in + let d = RelDecl.map_type (whd_betaiota !(pb.evdref)) d in let tomatch = lift_tomatch_stack 1 pb'.tomatch in let tomatch = relocate_index_tomatch (i+1) 1 tomatch in { pb' with @@ -1223,7 +1226,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* that had matched constructor C *) let cs_args = const_info.cs_args in let names,aliasname = get_names pb.env cs_args eqns in - let typs = List.map2 set_name names cs_args + let typs = List.map2 RelDecl.set_name names cs_args in (* We build the matrix obtained by expanding the matching on *) @@ -1273,7 +1276,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let typs' = List.map2 (fun (tm, (tmtyp,_), decl) deps -> - let na = get_name decl in + let na = RelDecl.get_name decl in let na = match curname, na with | Name _, Anonymous -> curname | Name _, Name _ -> na @@ -1658,8 +1661,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = List.map (fun a -> not (isRel a) || dependent a u || Int.Set.mem (destRel a) depvl) inst in let named_filter = - let open Context.Named.Declaration in - List.map (fun d -> dependent (mkVar (get_id d)) u) + List.map (fun d -> dependent (mkVar (NamedDecl.get_id d)) u) (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in @@ -1755,7 +1757,7 @@ let build_inversion_problem loc env sigma tms t = let sub_tms = List.map2 (fun deps (tm, (tmtyp,_), decl) -> - let na = if List.is_empty deps then Anonymous else force_name (get_name decl) in + let na = if List.is_empty deps then Anonymous else force_name (RelDecl.get_name decl) in Pushed (true,((tm,tmtyp),deps,na))) dep_sign decls in let subst = List.map (fun (na,t) -> (na,lift n t)) subst in @@ -1818,7 +1820,7 @@ let build_initial_predicate arsign pred = let rec buildrec n pred tmnames = function | [] -> List.rev tmnames,pred | (decl::realdecls)::lnames -> - let na = get_name decl in + let na = RelDecl.get_name decl in let n' = n + List.length realdecls in buildrec (n'+1) pred (force_name na::tmnames) lnames | _ -> assert false @@ -1851,7 +1853,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in LocalAssum (na, build_dependent_inductive env0 indf') - ::(List.map2 set_name realnal arsign) in + ::(List.map2 RelDecl.set_name realnal arsign) in let rec buildrec n = function | [],[] -> [] | (_,tm)::ltm, (_,x)::tmsign -> @@ -2048,7 +2050,7 @@ let constr_of_pat env evdref arsign pat avoid = let patargs, args, sign, env, n, m, avoid = List.fold_right2 (fun decl ua (patargs, args, sign, env, n, m, avoid) -> - let t = get_type decl in + let t = RelDecl.get_type decl in let pat', sign', arg', typ', argtypargs, n', avoid = let liftt = liftn (List.length sign) (succ (List.length args)) t in typ env (substl args liftt, []) ua avoid @@ -2088,8 +2090,8 @@ let constr_of_pat env evdref arsign pat avoid = (* Mark the equality as a hole *) pat', sign, lift i app, lift i apptype, realargs, n + i, avoid in - let pat', sign, patc, patty, args, z, avoid = typ env (get_type (List.hd arsign), List.tl arsign) pat avoid in - pat', (sign, patc, (get_type (List.hd arsign), args), pat'), avoid + let pat', sign, patc, patty, args, z, avoid = typ env (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in + pat', (sign, patc, (RelDecl.get_type (List.hd arsign), args), pat'), avoid (* shadows functional version *) @@ -2120,7 +2122,7 @@ let vars_of_ctx ctx = (GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)), [hole; GVar (Loc.ghost, prev)])) :: vars | _ -> - match get_name decl with + match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" | Name n -> n, GVar (Loc.ghost, n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) @@ -2297,7 +2299,7 @@ let abstract_tomatch env tomatchs tycon = let build_dependent_signature env evdref avoid tomatchs arsign = let avoid = ref avoid in let arsign = List.rev arsign in - let allnames = List.rev_map (List.map get_name) arsign in + let allnames = List.rev_map (List.map RelDecl.get_name) arsign in let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in let eqs, neqs, refls, slift, arsign' = List.fold_left2 @@ -2314,14 +2316,14 @@ let build_dependent_signature env evdref avoid tomatchs arsign = as much as possible *) let argsign = List.tl arsign in (* arguments in inverse application order *) let app_decl = List.hd arsign in (* The matched argument *) - let appn = get_name app_decl in - let appt = get_type app_decl in + let appn = RelDecl.get_name app_decl in + let appt = RelDecl.get_type app_decl in let argsign = List.rev argsign in (* arguments in application order *) let env', nargeqs, argeqs, refl_args, slift, argsign' = List.fold_left2 (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg decl -> - let name = get_name decl in - let t = get_type decl in + let name = RelDecl.get_name decl in + let t = RelDecl.get_type decl in let argt = Retyping.get_type_of env !evdref arg in let eq, refl_arg = if Reductionops.is_conv env !evdref argt t then @@ -2339,7 +2341,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign = let previd, id = let name = match kind_of_term arg with - Rel n -> get_name (lookup_rel n env) + Rel n -> RelDecl.get_name (lookup_rel n env) | _ -> name in make_prime avoid name @@ -2348,7 +2350,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign = (LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs, refl_arg :: refl_args, pred slift, - set_name (Name id) decl :: argsign')) + RelDecl.set_name (Name id) decl :: argsign')) (env, neqs, [], [], slift, []) args argsign in let eq = mk_JMeq evdref @@ -2363,13 +2365,13 @@ let build_dependent_signature env evdref avoid tomatchs arsign = succ nargeqs, refl_eq :: refl_args, pred slift, - ((set_name (Name id) app_decl :: argsign') :: arsigns)) + ((RelDecl.set_name (Name id) app_decl :: argsign') :: arsigns)) | _ -> (* Non dependent inductive or not inductive, just use a regular equality *) let decl = match arsign with [x] -> x | _ -> assert(false) in - let name = get_name decl in + let name = RelDecl.get_name decl in let previd, id = make_prime avoid name in - let arsign' = set_name (Name id) decl in + let arsign' = RelDecl.set_name (Name id) decl in let tomatch_ty = type_of_tomatch ty in let eq = mk_eq evdref (lift nar tomatch_ty) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 913e80f39..553786f58 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -153,7 +153,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env evdref x y in let dest_prod c = - let open Context.Rel.Declaration in match Reductionops.splay_prod_n env ( !evdref) 1 c with | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c | _ -> raise NoSubtacCoercion diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2f73ddd30..e745824b8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -24,6 +24,7 @@ open Globnames open Evd open Pretype_errors open Sigma.Notations +open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -962,7 +963,7 @@ let apply_on_subterm env evdref f c t = match kind_of_term t with | Evar (evk,args) when Evd.is_undefined !evdref evk -> let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in - let g decl a = if NamedDecl.is_local_assum decl then applyrec acc a else a in + let g decl a = if is_local_assum decl then applyrec acc a else a in mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) | _ -> map_constr_with_binders_left_to_right diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index f9ab75cea..29eb00c61 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -19,21 +19,21 @@ open Evarutil open Pretype_errors open Sigma.Notations +module RelDecl = Context.Rel.Declaration + let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = let evd = Sigma.Unsafe.of_evar_map evd in let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in (Sigma.to_evar_map evd, evk) let env_nf_evar sigma env = - let open Context.Rel.Declaration in process_rel_context - (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env + (fun d e -> push_rel (RelDecl.map_constr (nf_evar sigma) d) e) env let env_nf_betaiotaevar sigma env = - let open Context.Rel.Declaration in process_rel_context (fun d e -> - push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env + push_rel (RelDecl.map_constr (Reductionops.nf_betaiota sigma) d) e) env (****************************************) (* Operations on value/type constraints *) diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 4caa1e992..1f9573862 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -16,6 +16,8 @@ open Nameops open Termops open Pretype_errors +module NamedDecl = Context.Named.Declaration + (** Processing occurrences *) type occurrence_error = @@ -61,7 +63,7 @@ let proceed_with_occurrences f occs x = let map_named_declaration_with_hyploc f hyploc acc decl = let open Context.Named.Declaration in - let f = f (Some (get_id decl, hyploc)) in + let f = f (Some (NamedDecl.get_id decl, hyploc)) in match decl,hyploc with | LocalAssum (id,_), InHypValueOnly -> error_occurrences_error (IncorrectInValueOccurrence id) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0dd64697c..ffb9f8940 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -20,6 +20,8 @@ open Nativecode open Nativevalues open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (** This module implements normalization by evaluation to OCaml code *) exception Find_at of int @@ -122,7 +124,7 @@ let build_case_type dep p realargs c = (* TODO move this function *) let type_of_rel env n = - lookup_rel n env |> get_type |> lift n + lookup_rel n env |> RelDecl.get_type |> lift n let type_of_prop = mkSort type1_sort diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1ef96e034..a172d2560 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -44,7 +44,8 @@ open Evarconv open Pattern open Misctypes open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = constr_under_binders Id.Map.t @@ -460,7 +461,7 @@ let pretype_id pretype k0 loc env evdref lvar id = end; (* Check if [id] is a section or goal variable *) try - { uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) } + { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found_loc loc id @@ -505,7 +506,7 @@ let pretype_ref loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try make_judge (mkVar id) (get_type (lookup_named id env)) + (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env)) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal @@ -1043,8 +1044,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f decl (subst,update) = - let id = get_id decl in - let t = replace_vars subst (get_type decl) in + let id = NamedDecl.get_id decl in + let t = replace_vars subst (NamedDecl.get_type decl) in let c, update = try let c = List.assoc id update in @@ -1056,7 +1057,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try - let t' = lookup_named id env |> get_type in + let t' = lookup_named id env |> NamedDecl.get_type in if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err_loc (loc,"",str "Cannot interpret " ++ diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 98b36fb92..5b67af3e7 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -20,6 +20,9 @@ open Termops open Arguments_renaming open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + type retype_error = | NotASort | NotAnArity @@ -78,8 +81,7 @@ let sort_of_atomic_type env sigma ft args = in concl_of_arity env 0 ft (Array.to_list args) let type_of_var env id = - let open Context.Named.Declaration in - try get_type (lookup_named id env) + try NamedDecl.get_type (lookup_named id env) with Not_found -> retype_error (BadVariable id) let decomp_sort env sigma t = @@ -94,7 +96,7 @@ let retype ?(polyprop=true) sigma = (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus with Not_found -> retype_error (BadMeta n)) | Rel n -> - let ty = get_type (lookup_rel n env) in + let ty = RelDecl.get_type (lookup_rel n env) in lift n ty | Var id -> type_of_var env id | Const cst -> rename_type_of_constant env cst @@ -239,7 +241,7 @@ let sorts_of_context env evc ctxt = | [] -> env,[] | d :: ctxt -> let env,sorts = aux ctxt in - let s = get_sort_of env evc (get_type d) in + let s = get_sort_of env evc (RelDecl.get_type d) in (push_rel d env,s::sorts) in snd (aux ctxt) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 820a81b5d..c1d4a3403 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -25,6 +25,9 @@ open Patternops open Locus open Sigma.Notations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* Errors *) type reduction_tactic_error = @@ -54,13 +57,12 @@ let is_evaluable env = function | EvalVarRef id -> is_evaluable_var env id let value_of_evaluable_ref env evref u = - let open Context.Named.Declaration in match evref with | EvalConstRef con -> (try constant_value_in env (con,u) with NotEvaluableConst IsProj -> raise (Invalid_argument "value_of_evaluable_ref")) - | EvalVarRef id -> lookup_named id env |> get_value |> Option.get + | EvalVarRef id -> lookup_named id env |> NamedDecl.get_value |> Option.get let evaluable_of_global_reference env = function | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst @@ -112,22 +114,18 @@ let unsafe_reference_opt_value env sigma eval = | Declarations.Def c -> Some (Mod_subst.force_constr c) | _ -> None) | EvalVar id -> - let open Context.Named.Declaration in - lookup_named id env |> get_value + lookup_named id env |> NamedDecl.get_value | EvalRel n -> - let open Context.Rel.Declaration in - lookup_rel n env |> map_value (lift n) |> get_value + lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value | EvalEvar ev -> Evd.existential_opt_value sigma ev let reference_opt_value env sigma eval u = match eval with | EvalConst cst -> constant_opt_value_in env (cst,u) | EvalVar id -> - let open Context.Named.Declaration in - lookup_named id env |> get_value + lookup_named id env |> NamedDecl.get_value | EvalRel n -> - let open Context.Rel.Declaration in - lookup_rel n env |> map_value (lift n) |> get_value + lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value | EvalEvar ev -> Evd.existential_opt_value sigma ev exception NotEvaluable @@ -541,11 +539,9 @@ let match_eval_ref_value env sigma constr = | Const (sp, u) when is_evaluable env (EvalConstRef sp) -> Some (constant_value_in env (sp, u)) | Var id when is_evaluable env (EvalVarRef id) -> - let open Context.Named.Declaration in - lookup_named id env |> get_value + lookup_named id env |> NamedDecl.get_value | Rel n -> - let open Context.Rel.Declaration in - lookup_rel n env |> map_value (lift n) |> get_value + lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value | Evar ev -> Evd.existential_opt_value sigma ev | _ -> None diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 9fff64ae5..c3cdb361b 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -17,6 +17,9 @@ open Util open Typeclasses_errors open Libobject open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (*i*) let typeclasses_unique_solutions = ref false @@ -181,7 +184,7 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (map_constr do_subst) in + let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, do_subst_ctx ctx in @@ -198,16 +201,15 @@ let discharge_class (_,cl) = let repl = Lib.replacement_context () in let rel_of_variable_context ctx = List.fold_right ( fun (decl,_) (ctx', subst) -> - let open Context.Named.Declaration in - let decl' = decl |> map_constr (substn_vars 1 subst) |> to_rel in - (decl' :: ctx', Context.Named.Declaration.get_id decl :: subst) + let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel in + (decl' :: ctx', NamedDecl.get_id decl :: subst) ) ctx ([], []) in let discharge_rel_context subst n rel = let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in let ctx, _ = List.fold_right (fun decl (ctx, k) -> - map_constr (substn_vars k subst) decl :: ctx, succ k + RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k ) rel ([], n) in ctx @@ -220,7 +222,7 @@ let discharge_class (_,cl) = let discharge_context ctx' subst (grs, ctx) = let grs' = let newgrs = List.map (fun decl -> - match decl |> get_type |> class_of_constr with + match decl |> RelDecl.get_type |> class_of_constr with | None -> None | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) ctx' diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0c1ce0d2f..e9ee55d37 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -29,7 +29,9 @@ open Locus open Locusops open Find_subterm open Sigma.Notations -open Context.Named.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let keyed_unification = ref (false) let _ = Goptions.declare_bool_option { @@ -78,9 +80,8 @@ let occur_meta_evd sigma mv c = let abstract_scheme env evd c l lname_typ = List.fold_left2 (fun (t,evd) (locc,a) decl -> - let open Context.Rel.Declaration in - let na = get_name decl in - let ta = get_type decl in + let na = RelDecl.get_name decl in + let ta = RelDecl.get_type decl in let na = match kind_of_term a with Var id -> Name id | _ -> na in (* [occur_meta ta] test removed for support of eelim/ecase but consequences are unclear... @@ -1472,10 +1473,10 @@ let indirectly_dependent c d decls = it is needed otherwise, as e.g. when abstracting over "2" in "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious way to see that the second hypothesis depends indirectly over 2 *) - List.exists (fun d' -> dependent_in_decl (mkVar (get_id d')) d) decls + List.exists (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) decls let indirect_dependency d decls = - decls |> List.filter (fun d' -> dependent_in_decl (mkVar (get_id d')) d) |> List.hd |> get_id + decls |> List.filter (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) |> List.hd |> NamedDecl.get_id let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let current_sigma = Sigma.to_evar_map current_sigma in @@ -1594,7 +1595,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let likefirst = clause_with_generic_occurrences occs in let mkvarid () = mkVar id in let compute_dependency _ d (sign,depdecls) = - let hyp = get_id d in + let hyp = NamedDecl.get_id d in match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> if indirectly_dependent c d depdecls then @@ -1631,7 +1632,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = replace_term_occ_modulo occ test mkvarid concl in let lastlhyp = - if List.is_empty depdecls then None else Some (get_id (List.last depdecls)) in + if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in let res = match out test with | None -> None | Some (sigma, c) -> Some (Sigma.Unsafe.of_pair (c, sigma)) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c396f593b..331ad0912 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -17,6 +17,9 @@ open Reduction open Vm open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (*******************************************) (* Calcul de la forme normal d'un terme *) (*******************************************) @@ -203,12 +206,11 @@ and constr_type_of_idkey env (idkey : Vars.id_key) stk = in nf_univ_args ~nb_univs mk env stk | VarKey id -> - let open Context.Named.Declaration in - let ty = get_type (lookup_named id env) in + let ty = NamedDecl.get_type (lookup_named id env) in nf_stk env (mkVar id) ty stk | RelKey i -> let n = (nb_rel env - i) in - let ty = get_type (lookup_rel n env) in + let ty = RelDecl.get_type (lookup_rel n env) in nf_stk env (mkRel n) (lift n ty) stk and nf_stk ?from:(from=0) env c t stk = diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f71719cb9..37098e504 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -27,6 +27,10 @@ open Recordops open Misctypes open Printer open Printmod +open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : mutual_inductive -> std_ppcmds; @@ -132,7 +136,6 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in - let open Context.Rel.Declaration in let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in @@ -170,9 +173,8 @@ type opacity = | TransparentMaybeOpacified of Conv_oracle.level let opacity env = - let open Context.Named.Declaration in function - | VarRef v when is_local_def (Environ.lookup_named v env) -> + | VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) | ConstRef cst -> @@ -733,8 +735,7 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - let open Context.Named.Declaration in - str |> Global.lookup_named |> set_id str |> print_named_decl + str |> Global.lookup_named |> NamedDecl.set_id str |> print_named_decl with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") @@ -762,8 +763,7 @@ let print_opaque_name qid = let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let open Context.Named.Declaration in - lookup_named id env |> set_id id |> print_named_decl + lookup_named id env |> NamedDecl.set_id id |> print_named_decl let print_about_any loc k = match k with diff --git a/proofs/goal.ml b/proofs/goal.ml index 111a947a9..75f56c6b9 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -10,7 +10,8 @@ open Util open Pp open Term open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated @@ -77,7 +78,7 @@ module V82 = struct let evars = Sigma.to_evar_map evars in let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (mkVar % get_id) ctxt in + let inst = Array.map_of_list (mkVar % NamedDecl.get_id) ctxt in let ev = Term.mkEvar (evk,inst) in (evk, ev, evars) @@ -148,7 +149,7 @@ module V82 = struct let env = env sigma gl in let genv = Global.env () in let is_proof_var decl = - try ignore (Environ.lookup_named (get_id decl) genv); false + try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false with Not_found -> true in Environ.fold_named_context_reverse (fun t decl -> if is_proof_var decl then diff --git a/proofs/logic.ml b/proofs/logic.ml index 39dff4aca..19f5f5d3f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -24,6 +24,8 @@ open Retyping open Misctypes open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + type refiner_error = (* Errors raised by the refiner *) @@ -162,7 +164,7 @@ let reorder_context env sign ord = (match ctxt_head with | [] -> error_no_such_hypothesis (List.hd ord) | d :: ctxt -> - let x = get_id d in + let x = NamedDecl.get_id d in if Id.Set.mem x expected then step ord (Id.Set.remove x expected) ctxt (push_item x d moved_hyps) ctxt_tail @@ -178,7 +180,7 @@ let reorder_val_context env sign ord = let check_decl_position env sign d = - let x = get_id d in + let x = NamedDecl.get_id d in let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then @@ -204,8 +206,8 @@ let move_location_eq m1 m2 = match m1, m2 with let rec get_hyp_after h = function | [] -> error_no_such_hypothesis h | d :: right -> - if Id.equal (get_id d) h then - match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst + if Id.equal (NamedDecl.get_id d) h then + match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst else get_hyp_after h right @@ -213,7 +215,7 @@ let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom | d :: right -> - let hyp = get_id d in + let hyp = NamedDecl.get_id d in if Id.equal hyp hfrom then (left,right,d, toleft || move_location_eq hto MoveLast) else @@ -235,24 +237,24 @@ let move_hyp toleft (left,declfrom,right) hto = let env = Global.env() in let test_dep d d2 = if toleft - then occur_var_in_decl env (get_id d2) d - else occur_var_in_decl env (get_id d) d2 + then occur_var_in_decl env (NamedDecl.get_id d2) d + else occur_var_in_decl env (NamedDecl.get_id d) d2 in let rec moverec first middle = function | [] -> if match hto with MoveFirst | MoveLast -> false | _ -> true then error_no_such_hypothesis (hyp_of_move_location hto); List.rev first @ List.rev middle - | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) -> + | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> List.rev first @ List.rev middle @ right | d :: right -> - let hyp = get_id d in + let hyp = NamedDecl.get_id d in let (first',middle') = if List.exists (test_dep d) middle then if not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else - errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++ + errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++ Miscprint.pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") @@ -489,16 +491,16 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp check sign sigma d = - let id = get_id d in - let b = get_value d in + let id = NamedDecl.get_id d in + let b = NamedDecl.get_value d in let env = Global.env() in let reorder = ref [] in let sign' = apply_to_hyp check sign id (fun _ d' _ -> - let c = get_value d' in + let c = NamedDecl.get_value d' in let env = Global.env_of_context sign in - if check && not (is_conv env sigma (get_type d) (get_type d')) then + if check && not (is_conv env sigma (NamedDecl.get_type d) (NamedDecl.get_type d')) then errorlabstrm "Logic.convert_hyp" (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7605f6387..4cb9f03ce 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -18,6 +18,8 @@ open Util open Pp open Names +module NamedDecl = Context.Named.Declaration + (*** Proof Modes ***) (* Type of proof modes : @@ -276,7 +278,7 @@ let set_used_variables l = let ids = List.fold_right Id.Set.add l Id.Set.empty in let ctx = Environ.keep_hyps env ids in let ctx_set = - List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in + List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in let aux env entry (ctx, all_safe, to_clear as orig) = match entry with diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index 5b24a1fb2..a125fb10d 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -12,6 +12,8 @@ open Util open Vernacexpr open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let to_string e = let rec aux = function | SsEmpty -> "()" @@ -39,10 +41,10 @@ let rec close_fwd e s = | LocalAssum _ -> Id.Set.empty | LocalDef (_,b,_) -> global_vars_set e b in - let vty = global_vars_set e (get_type decl) in + let vty = global_vars_set e (NamedDecl.get_type decl) in let vbty = Id.Set.union vb vty in if Id.Set.exists (fun v -> Id.Set.mem v s) vbty - then Id.Set.add (get_id decl) (Id.Set.union s vbty) else s) + then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s) s (named_context e) in if Id.Set.equal s s' then s else close_fwd e s' @@ -65,13 +67,13 @@ and set_of_id env ty id = Id.Set.union (global_vars_set env ty) acc) Id.Set.empty ty else if Id.to_string id = "All" then - List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty else if CList.mem_assoc_f Id.equal id !known_names then process_expr env (CList.assoc_f Id.equal id !known_names) [] else Id.Set.singleton id and full_set env = - List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty let process_expr env e ty = let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in diff --git a/proofs/refine.ml b/proofs/refine.ml index 76e2d7dc5..139862b8f 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -11,6 +11,8 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let extract_prefix env info = let ctx1 = List.rev (Environ.named_context env) in let ctx2 = List.rev (Evd.evar_context info) in @@ -26,7 +28,7 @@ let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = - let t = get_type decl in + let t = NamedDecl.get_type decl in let evdref = ref sigma in let _ = Typing.e_sort_of env evdref t in let () = match decl with diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ebd30820b..d9ab2fbdb 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -13,7 +13,8 @@ open Evd open Environ open Proof_type open Logic -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration let sig_it x = x.it let project x = x.sigma @@ -202,7 +203,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) let { it = gls; sigma = sigma; } = rslt in let hyps:Context.Named.t list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in - let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in + let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in let newhyps = List.map (fun hypl -> List.subtract cmp hypl oldhyps) @@ -215,7 +216,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) List.fold_left (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") ^ (List.fold_left - (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc) + (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) "" lh)) "" newhyps in Feedback.msg_notice diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 50984c48e..957843bc9 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -21,6 +21,8 @@ open Refiner open Sigma.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let re_sig it gc = { it = it; sigma = gc; } (**************************************************************) @@ -46,7 +48,7 @@ let pf_hyps_types gls = | LocalDef (id,_,x) -> id, x) sign -let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id +let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id let pf_last_hyp gl = List.hd (pf_hyps gl) @@ -57,7 +59,7 @@ let pf_get_hyp gls id = raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - pf_get_hyp gls id |> get_type + pf_get_hyp gls id |> NamedDecl.get_type let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) @@ -199,7 +201,7 @@ module New = struct sign let pf_get_hyp_typ id gl = - pf_get_hyp id gl |> get_type + pf_get_hyp id gl |> NamedDecl.get_type let pf_hyps_types gl = let env = Proofview.Goal.env gl in diff --git a/stm/lemmas.ml b/stm/lemmas.ml index fb2f0351d..5e4e34114 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -33,6 +33,9 @@ open Constrintern open Impargs open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a let mk_hook hook = hook let call_hook fix_exn hook l c = @@ -45,8 +48,7 @@ let call_hook fix_exn hook l c = let retrieve_first_recthm = function | VarRef id -> - let open Context.Named.Declaration in - (get_value (Global.lookup_named id),variable_opacity id) + (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in (Global.body_of_constant_body cb, is_opaque cb) @@ -110,7 +112,7 @@ let find_mutually_recursive_statements thms = (Global.env()) hyps in let ind_hyps = List.flatten (List.map_i (fun i decl -> - let t = get_type decl in + let t = RelDecl.get_type decl in match kind_of_term t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in @@ -456,7 +458,7 @@ let start_proof_com kind thms hook = let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); - let ids = List.map get_name ctx in + let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6e01a676a..8c43ac8b5 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -32,6 +32,8 @@ open Misctypes open Proofview.Notations open Hints +module NamedDecl = Context.Named.Declaration + (** Hint database named "typeclass_instances", now created directly in Auto *) (** Options handling *) @@ -523,9 +525,8 @@ let evars_to_goals p evm = (** Making local hints *) let make_resolve_hyp env sigma st flags only_classes pri decl = - let open Context.Named.Declaration in - let id = get_id decl in - let cty = Evarutil.nf_evar sigma (get_type decl) in + let id = NamedDecl.get_id decl in + let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in let rec iscl env ty = let ctx, ar = decompose_prod_assum ty in match kind_of_term (fst (decompose_app ar)) with @@ -564,10 +565,9 @@ let make_hints g st only_classes sign = List.fold_left (fun hints hyp -> let consider = - let open Context.Named.Declaration in - try let t = Global.lookup_named (get_id hyp) |> get_type in + try let t = Global.lookup_named (NamedDecl.get_id hyp) |> NamedDecl.get_type in (* Section variable, reindex only if the type changed *) - not (Term.eq_constr t (get_type hyp)) + not (Term.eq_constr t (NamedDecl.get_type hyp)) with Not_found -> true in if consider then diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c3796b484..c81705c1a 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -13,7 +13,8 @@ open Coqlib open Reductionops open Misctypes open Proofview.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* Absurd *) @@ -46,7 +47,7 @@ let absurd c = absurd c let filter_hyp f tac = let rec seek = function | [] -> Proofview.tclZERO Not_found - | d::rest when f (get_type d) -> tac (get_id d) + | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in @@ -60,8 +61,8 @@ let contradiction_context = let rec seek_neg l = match l with | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | d :: rest -> - let id = get_id d in - let typ = nf_evar sigma (get_type d) in + let id = NamedDecl.get_id d in + let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in if is_empty_type typ then simplest_elim (mkVar id) diff --git a/tactics/elim.ml b/tactics/elim.ml index f2b9eec4b..3f0c01a29 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -16,7 +16,8 @@ open Tacmach.New open Tacticals.New open Tactics open Proofview.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* Supposed to be called without as clause *) let introElimAssumsThen tac ba = @@ -139,7 +140,7 @@ let induction_trailer abs_i abs_j bargs = let (hyps,_) = List.fold_left (fun (bring_ids,leave_ids) d -> - let cid = get_id d in + let cid = NamedDecl.get_id d in if not (List.mem cid leave_ids) then (d::bring_ids,leave_ids) else (bring_ids,cid::leave_ids)) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 1a45217a4..c94dcfa9d 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -60,6 +60,8 @@ open Indrec open Sigma.Notations open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + let hid = Id.of_string "H" let xid = Id.of_string "X" let default_id_of_sort = function InProp | InSet -> hid | InType -> xid @@ -600,9 +602,9 @@ let fix_r2l_forward_rew_scheme (c, ctx') = | hp :: p :: ind :: indargs -> let c' = my_it_mkLambda_or_LetIn indargs - (mkLambda_or_LetIn (map_constr (liftn (-1) 1) p) - (mkLambda_or_LetIn (map_constr (liftn (-1) 2) hp) - (mkLambda_or_LetIn (map_constr (lift 2) ind) + (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p) + (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp) + (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind) (Reductionops.whd_beta Evd.empty (applist (c, Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) @@ -741,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind = if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported."; let env_with_arity = push_rel_context arityctxt env in - let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in + let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then diff --git a/tactics/equality.ml b/tactics/equality.ml index 3e5b7b65f..fcfd26185 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -45,6 +45,8 @@ open Proofview.Notations open Unification open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (* Options *) let discriminate_introduction = ref true @@ -1662,13 +1664,13 @@ exception FoundHyp of (Id.t * constr * bool) (* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *) let is_eq_x gl x d = - let id = get_id d in + let id = NamedDecl.get_id d in try let is_var id c = match kind_of_term c with | Var id' -> Id.equal id id' | _ -> false in - let c = pf_nf_evar gl (get_type d) in + let c = pf_nf_evar gl (NamedDecl.get_type d) in let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true)); if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false)) @@ -1686,7 +1688,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = (* The set of hypotheses using x *) let dephyps = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> - let id = get_id dcl in + let id = NamedDecl.get_id dcl in if not (Id.equal id hyp) && List.exists (fun y -> occur_var_in_decl env y dcl) deps then @@ -1715,7 +1717,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let subst_one_var dep_proof_ok x = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in - let xval = pf_get_hyp x gl |> get_value in + let xval = pf_get_hyp x gl |> NamedDecl.get_value in (* If x has a body, simply replace x with body and clear x *) if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) else (* Find a non-recursive definition for x *) @@ -1763,12 +1765,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let find_eq_data_decompose = find_eq_data_decompose gl in let test decl = try - let lbeq,u,(_,x,y) = find_eq_data_decompose (get_type decl) in + let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match kind_of_term x, kind_of_term y with | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) -> - Some (get_id decl) + Some (NamedDecl.get_id decl) | _ -> None with Constr_matching.PatternMatchingFailure -> None @@ -1782,7 +1784,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let find_eq_data_decompose = find_eq_data_decompose gl in - let c = pf_get_hyp hyp gl |> get_type in + let c = pf_get_hyp hyp gl |> NamedDecl.get_type in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else @@ -1851,10 +1853,10 @@ let rewrite_assumption_cond cond_eq_term cl = let rec arec hyps gl = match hyps with | [] -> error "No such assumption." | hyp ::rest -> - let id = get_id hyp in + let id = NamedDecl.get_id hyp in begin try - let dir = cond_eq_term (get_type hyp) gl in + let dir = cond_eq_term (NamedDecl.get_type hyp) gl in general_rewrite_clause dir false (mkVar id,NoBindings) cl with | Failure _ | UserError _ -> arec rest gl end diff --git a/tactics/hints.ml b/tactics/hints.ml index 8f3eb5eb5..a74fceb8f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -34,7 +34,8 @@ open Tacred open Printer open Vernacexpr open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (****************************************) (* General functions *) @@ -782,11 +783,11 @@ let make_resolves env sigma flags pri poly ?name cr = (* used to add an hypothesis to the local hint database *) let make_resolve_hyp env sigma decl = - let hname = get_id decl in + let hname = NamedDecl.get_id decl in try [make_apply_entry env sigma (true, true, false) None false ~name:(PathHints [VarRef hname]) - (mkVar hname, get_type decl, Univ.ContextSet.empty)] + (mkVar hname, NamedDecl.get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp") diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 6e24cc469..36770925f 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -19,6 +19,8 @@ open Declarations open Tacmach.New open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* I implemented the following functions which test whether a term t is an inductive but non-recursive type, a general conjuction, a general disjunction, or a type with no constructors. @@ -100,7 +102,7 @@ let match_with_one_constructor style onlybinary allow_rec t = (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in if List.for_all - (fun decl -> let c = get_type decl in + (fun decl -> let c = RelDecl.get_type decl in is_local_assum decl && isRel c && Int.equal (destRel c) mib.mind_nparams) ctx @@ -109,7 +111,7 @@ let match_with_one_constructor style onlybinary allow_rec t = else None else let ctyp = prod_applist mip.mind_nf_lc.(0) args in - let cargs = List.map get_type (prod_assum ctyp) in + let cargs = List.map RelDecl.get_type (prod_assum ctyp) in if not (is_lax_conjunction style) || has_nodep_prod ctyp then (* Record or non strict conjunction *) Some (hdapp,List.rev cargs) diff --git a/tactics/inv.ml b/tactics/inv.ml index bda16b01c..575710ecc 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -28,7 +28,8 @@ open Misctypes open Tacexpr open Sigma.Notations open Proofview.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration let var_occurs_in_pf gl id = let env = Proofview.Goal.env gl in @@ -182,7 +183,7 @@ let dependent_hyps env id idlist gl = | [] -> [] | d::l -> (* Update the type of id1: it may have been subject to rewriting *) - let d = pf_get_hyp (get_id d) gl in + let d = pf_get_hyp (NamedDecl.get_id d) gl in if occur_var_in_decl env id d then d :: dep_rec l else dep_rec l @@ -192,7 +193,7 @@ let dependent_hyps env id idlist gl = let split_dep_and_nodep hyps gl = List.fold_right (fun d (l1,l2) -> - if var_occurs_in_pf gl (get_id d) then (d::l1,l2) else (l1,d::l2)) + if var_occurs_in_pf gl (NamedDecl.get_id d) then (d::l1,l2) else (l1,d::l2)) hyps ([],[]) (* Computation of dids is late; must have been done in rewrite_equations*) @@ -383,7 +384,7 @@ let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.nf_enter { enter = begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in let first_eq = ref MoveLast in - let avoid = if as_mode then List.map get_id nodepids else [] in + let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in match othin with | Some thin -> tclTHENLIST @@ -399,10 +400,10 @@ let rewrite_equations as_mode othin neqns names ba = tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) names; tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) - let idopt = if as_mode then Some (get_id d) else None in + let idopt = if as_mode then Some (NamedDecl.get_id d) else None in intro_move idopt (if thin then MoveLast else !first_eq)) nodepids; - (tclMAP (fun d -> tclTRY (clear [get_id d])) depids)] + (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)] | None -> (* simple inversion *) if as_mode then diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 642bf520b..1639ec54c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -29,6 +29,8 @@ open Decl_kinds open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let no_inductive_inconstr env sigma constr = (str "Cannot recognize an inductive predicate in " ++ pr_lconstr_env env sigma constr ++ @@ -156,7 +158,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let revargs,ownsign = fold_named_context (fun env d (revargs,hyps) -> - let id = get_id d in + let id = NamedDecl.get_id d in if Id.List.mem id ivars then ((mkVar id)::revargs, Context.Named.add d hyps) else @@ -206,7 +208,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let ownSign = ref begin fold_named_context (fun env d sign -> - if mem_named_context (get_id d) global_named_context then sign + if mem_named_context (NamedDecl.get_id d) global_named_context then sign else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml index 004492e78..a5ccd500c 100644 --- a/tactics/tactic_matching.ml +++ b/tactics/tactic_matching.ml @@ -13,6 +13,8 @@ open Names open Tacexpr open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** [t] is the type of matching successes. It ultimately contains a {!Tacexpr.glob_tactic_expr} representing the left-hand side of the corresponding matching rule, a matching substitution to be @@ -280,9 +282,9 @@ module PatternMatching (E:StaticEnvironment) = struct the name of the matched hypothesis. *) let hyp_match_type hypname pat hyps = pick hyps >>= fun decl -> - let id = get_id decl in + let id = NamedDecl.get_id decl in let refresh = is_local_def decl in - pattern_match_term refresh pat (get_type decl) () <*> + pattern_match_term refresh pat (NamedDecl.get_type decl) () <*> put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*> return id @@ -319,7 +321,7 @@ module PatternMatching (E:StaticEnvironment) = struct (* spiwack: alternatively it is possible to return the list with the matched hypothesis removed directly in [hyp_match]. *) - let select_matched_hyp decl = Id.equal (get_id decl) matched_hyp in + let select_matched_hyp decl = Id.equal (NamedDecl.get_id decl) matched_hyp in let hyps = CList.remove_first select_matched_hyp hyps in hyp_pattern_list_match pats hyps lhs | [] -> return lhs diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 87fdcf14d..664629f34 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -16,7 +16,8 @@ open Declarations open Tacmach open Clenv open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (************************************************************************) (* Tacticals re-exported from the Refiner module *) @@ -70,7 +71,7 @@ let nthDecl m gl = try List.nth (pf_hyps gl) (m-1) with Failure _ -> error "No such assumption." -let nthHypId m gl = nthDecl m gl |> get_id +let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) let lastDecl gl = nthDecl 1 gl @@ -81,7 +82,7 @@ let nLastDecls n gl = try List.firstn n (pf_hyps gl) with Failure _ -> error "Not enough hypotheses in the goal." -let nLastHypsId n gl = List.map get_id (nLastDecls n gl) +let nLastHypsId n gl = List.map NamedDecl.get_id (nLastDecls n gl) let nLastHyps n gl = List.map mkVar (nLastHypsId n gl) let onNthDecl m tac gl = tac (nthDecl m gl) gl @@ -99,7 +100,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac let onNLastHyps n tac = onHyps (nLastHyps n) tac let afterHyp id gl = - fst (List.split_when (Id.equal id % get_id) (pf_hyps gl)) + fst (List.split_when (Id.equal id % NamedDecl.get_id) (pf_hyps gl)) (***************************************) (* Clause Tacticals *) @@ -560,7 +561,7 @@ module New = struct let nthHypId m gl = (** We only use [id] *) let gl = Proofview.Goal.assume gl in - nthDecl m gl |> get_id + nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) @@ -592,7 +593,7 @@ module New = struct let afterHyp id tac = Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let rem, _ = List.split_when (Id.equal id % get_id) hyps in + let rem, _ = List.split_when (Id.equal id % NamedDecl.get_id) hyps in tac rem end } diff --git a/tactics/tactics.ml b/tactics/tactics.ml index acc0fa1ca..d8c241193 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -43,6 +43,10 @@ open Locusops open Misctypes open Proofview.Notations open Sigma.Notations +open Context.Named.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let inj_with_occurrences e = (AllOccurrences,e) @@ -162,19 +166,17 @@ let _ = (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) let unsafe_intro env store decl b = - let open Context.Named.Declaration in Refine.refine ~unsafe:true { run = begin fun sigma -> let ctx = named_context_val env in let nctx = push_named_context_val decl ctx in - let inst = List.map (mkVar % get_id) (named_context env) in + let inst = List.map (mkVar % NamedDecl.get_id) (named_context env) in let ninst = mkRel 1 :: inst in - let nb = subst1 (mkVar (get_id decl)) b in + let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p) end } let introduction ?(check=true) id = - let open Context.Named.Declaration in Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in @@ -186,6 +188,7 @@ let introduction ?(check=true) id = errorlabstrm "Tactics.introduction" (str "Variable " ++ pr_id id ++ str " is already declared.") in + let open Context.Named.Declaration in match kind_of_term (whd_evar sigma concl) with | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b @@ -317,7 +320,6 @@ let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest) (* Renaming hypotheses *) let rename_hyp repl = - let open Context.Named.Declaration in let fold accu (src, dst) = match accu with | None -> None | Some (srcs, dsts) -> @@ -339,7 +341,7 @@ let rename_hyp repl = let concl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in (** Check that we do not mess variables *) - let fold accu decl = Id.Set.add (get_id decl) accu in + let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in let vars = List.fold_left fold Id.Set.empty hyps in let () = if not (Id.Set.subset src vars) then @@ -358,13 +360,13 @@ let rename_hyp repl = let subst = List.map make_subst repl in let subst c = Vars.replace_vars subst c in let map decl = - decl |> map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id) - |> map_constr subst + decl |> NamedDecl.map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id) + |> NamedDecl.map_constr subst in let nhyps = List.map map hyps in let nconcl = subst concl in let nctx = Environ.val_of_named_context nhyps in - let instance = List.map (mkVar % get_id) hyps in + let instance = List.map (mkVar % NamedDecl.get_id) hyps in Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar_instance nctx sigma nconcl ~store instance end } @@ -982,23 +984,21 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = aux n [] let get_next_hyp_position id gl = - let open Context.Named.Declaration in let rec aux = function | [] -> raise (RefinerError (NoSuchHyp id)) | decl :: right -> - if Id.equal (get_id decl) id then - match right with decl::_ -> MoveBefore (get_id decl) | [] -> MoveLast + if Id.equal (NamedDecl.get_id decl) id then + match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveLast else aux right in aux (Proofview.Goal.hyps (Proofview.Goal.assume gl)) let get_previous_hyp_position id gl = - let open Context.Named.Declaration in let rec aux dest = function | [] -> raise (RefinerError (NoSuchHyp id)) | decl :: right -> - let hyp = get_id decl in + let hyp = NamedDecl.get_id decl in if Id.equal hyp id then dest else aux (MoveAfter hyp) right in aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) @@ -1559,7 +1559,7 @@ let make_projection env sigma params cstr sign elim i n c u = | NotADefinedRecordUseScheme elim -> (* bugs: goes from right to left when i increases! *) let decl = List.nth cstr.cs_args i in - let t = get_type decl in + let t = RelDecl.get_type decl in let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in let branch = it_mkLambda_or_LetIn b cstr.cs_args in if @@ -1943,7 +1943,6 @@ let exact_proof c = end } let assumption = - let open Context.Named.Declaration in let rec arec gl only_eq = function | [] -> if only_eq then @@ -1951,7 +1950,7 @@ let assumption = arec gl false hyps else Tacticals.New.tclZEROMSG (str "No such assumption.") | decl::rest -> - let t = get_type decl in + let t = NamedDecl.get_type decl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let (sigma, is_same_type) = @@ -1962,7 +1961,7 @@ let assumption = in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> - Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h } + Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (NamedDecl.get_id decl)) h } else arec gl only_eq rest in let assumption_tac = { enter = begin fun gl -> @@ -1992,7 +1991,7 @@ let check_is_type env sigma ty = let check_decl env sigma decl = let open Context.Named.Declaration in - let ty = get_type decl in + let ty = NamedDecl.get_type decl in let evdref = ref sigma in try let _ = Typing.e_sort_of env evdref ty in @@ -2002,7 +2001,7 @@ let check_decl env sigma decl = in !evdref with e when CErrors.noncritical e -> - let id = get_id decl in + let id = NamedDecl.get_id decl in raise (DependsOnBody (Some id)) let clear_body ids = @@ -2034,7 +2033,7 @@ let clear_body ids = check_decl env sigma decl else sigma in - let seen = seen || List.mem_f Id.equal (get_id decl) ids in + let seen = seen || List.mem_f Id.equal (NamedDecl.get_id decl) ids in (push_named decl env, sigma, seen) in let (env, sigma, _) = List.fold_left check (base_env, sigma, false) (List.rev ctx) in @@ -2074,13 +2073,12 @@ let rec intros_clearing = function (* Keeping only a few hypotheses *) let keep hyps = - let open Context.Named.Declaration in Proofview.Goal.nf_enter { enter = begin fun gl -> Proofview.tclENV >>= fun env -> let ccl = Proofview.Goal.concl gl in let cl,_ = fold_named_context_reverse (fun (clear,keep) decl -> - let hyp = get_id decl in + let hyp = NamedDecl.get_id decl in if Id.List.mem hyp hyps || List.exists (occur_var_in_decl env hyp) keep || occur_var env hyp ccl @@ -2618,13 +2616,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = end } let insert_before decls lasthyp env = - let open Context.Named.Declaration in match lasthyp with | None -> push_named_context decls env | Some id -> Environ.fold_named_context (fun _ d env -> - let env = if Id.equal id (get_id d) then push_named_context decls env else env in + let env = if Id.equal id (NamedDecl.get_id d) then push_named_context decls env else env in push_named d env) ~init:(reset_context env) env @@ -2763,19 +2760,18 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = generalize_goal_gen env sigma ids i o t cl let old_generalize_dep ?(with_let=false) c gl = - let open Context.Named.Declaration in let env = pf_env gl in let sign = pf_hyps gl in let init_ids = ids_of_named_context (Global.named_context()) in let seek (d:Context.Named.Declaration.t) (toquant:Context.Named.t) = - if List.exists (fun d' -> occur_var_in_decl env (get_id d') d) toquant + if List.exists (fun d' -> occur_var_in_decl env (NamedDecl.get_id d') d) toquant || dependent_in_decl c d then d::toquant else toquant in let to_quantify = Context.Named.fold_outside seek sign ~init:[] in let to_quantify_rev = List.rev to_quantify in - let qhyps = List.map get_id to_quantify_rev in + let qhyps = List.map NamedDecl.get_id to_quantify_rev in let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in let tothin' = match kind_of_term c with @@ -2787,7 +2783,7 @@ let old_generalize_dep ?(with_let=false) c gl = let body = if with_let then match kind_of_term c with - | Var id -> Tacmach.pf_get_hyp gl id |> get_value + | Var id -> Tacmach.pf_get_hyp gl id |> NamedDecl.get_value | _ -> None else None in @@ -2936,7 +2932,7 @@ let unfold_body x = | LocalDef (_,xval,_) -> xval in Tacticals.New.afterHyp x begin fun aft -> - let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in + let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in let rfun _ _ c = replace_vars [x, xval] c in let reducth h = reduct_in_hyp rfun h in let reductc = reduct_in_concl (rfun, DEFAULTcast) in @@ -3255,7 +3251,6 @@ exception Shunt of Id.t move_location let cook_sign hyp0_opt inhyps indvars env = (* First phase from L to R: get [toclear], [decldep] and [statuslist] for the hypotheses before (= more ancient than) hyp0 (see above) *) - let open Context.Named.Declaration in let toclear = ref [] in let avoid = ref [] in let decldeps = ref [] in @@ -3265,7 +3260,7 @@ let cook_sign hyp0_opt inhyps indvars env = let before = ref true in let maindep = ref false in let seek_deps env decl rhyp = - let hyp = get_id decl in + let hyp = NamedDecl.get_id decl in if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then begin before:=false; @@ -3284,7 +3279,7 @@ let cook_sign hyp0_opt inhyps indvars env = in let depother = List.is_empty inhyps && (List.exists (fun id -> occur_var_in_decl env id decl) indvars || - List.exists (fun decl' -> occur_var_in_decl env (get_id decl') decl) !decldeps) + List.exists (fun decl' -> occur_var_in_decl env (NamedDecl.get_id decl') decl) !decldeps) in if not (List.is_empty inhyps) && Id.List.mem hyp inhyps || dephyp0 || depother @@ -3307,7 +3302,7 @@ let cook_sign hyp0_opt inhyps indvars env = let _ = fold_named_context seek_deps env ~init:MoveFirst in (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) let compute_lstatus lhyp decl = - let hyp = get_id decl in + let hyp = NamedDecl.get_id decl in if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then raise (Shunt lhyp); if Id.List.mem hyp !ldeps then begin @@ -3531,13 +3526,12 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = end } let hyps_of_vars env sign nogen hyps = - let open Context.Named.Declaration in if Id.Set.is_empty hyps then [] else let (_,lh) = Context.Named.fold_inside (fun (hs,hl) d -> - let x = get_id d in + let x = NamedDecl.get_id d in if Id.Set.mem x nogen then (hs,hl) else if Id.Set.mem x hs then (hs,x::hl) else @@ -3567,7 +3561,6 @@ let linear vars args = with Seen -> false let is_defined_variable env id = - let open Context.Named.Declaration in lookup_named id env |> is_local_def let abstract_args gl generalize_vars dep id defined f args = @@ -3591,7 +3584,7 @@ let abstract_args gl generalize_vars dep id defined f args = let name, ty, arity = let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in let decl = List.hd rel in - get_name decl, get_type decl, c + RelDecl.get_name decl, RelDecl.get_type decl, c in let argty = Tacmach.pf_unsafe_type_of gl arg in let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in @@ -4026,14 +4019,15 @@ let is_functional_induction elimc gl = need a dependent one or not *) let get_eliminator elim dep s gl = - let open Context.Rel.Declaration in match elim with | ElimUsing (elim,indsign) -> Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in - let branchlengthes = List.map (fun d -> assert (is_local_assum d); pi1 (decompose_prod_letin (get_type d))) (List.rev s.branches) in + let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (RelDecl.get_type d))) + (List.rev s.branches) + in evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l (* Instantiate all meta variables of elimclause using lid, some elts @@ -4095,7 +4089,6 @@ let induction_tac with_evars params indvars elim = induction applies with the induction hypotheses *) let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_tac = - let open Context.Named.Declaration in Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -4108,7 +4101,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let s = Retyping.get_sort_family_of env sigma tmpcl in let deps_cstr = List.fold_left - (fun a decl -> if is_local_assum decl then (mkVar (get_id decl))::a else a) [] deps in + (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.get_id decl))::a else a) [] deps in let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in @@ -4190,7 +4183,6 @@ let induction_without_atomization isrec with_evars elim names lid = (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls = Proofview.Goal.nf_enter { enter = begin fun gl -> - let open Context.Named.Declaration in if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences then errorlabstrm "" @@ -4199,7 +4191,7 @@ let clear_unselected_context id inhyps cls = match cls.onhyps with | Some hyps -> let to_erase d = - let id' = get_id d in + let id' = NamedDecl.get_id d in if Id.List.mem id' inhyps then (* if selected, do not erase *) None else (* erase if not selected and dependent on id or selected hyps *) @@ -4766,7 +4758,7 @@ let interpretable_as_section_decl evd d1 d2 = | LocalDef _, LocalAssum _ -> false | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 - | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (get_type d2) + | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2) let rec decompose len c t accu = let open Context.Rel.Declaration in @@ -4779,7 +4771,6 @@ let rec decompose len c t accu = | _ -> assert false let rec shrink ctx sign c t accu = - let open Context.Rel.Declaration in match ctx, sign with | [], [] -> (c, t, accu) | p :: ctx, decl :: sign -> @@ -4790,9 +4781,9 @@ let rec shrink ctx sign c t accu = else let c = mkLambda_or_LetIn p c in let t = mkProd_or_LetIn p t in - let accu = if is_local_assum p then let open Context.Named.Declaration in - mkVar (get_id decl) :: accu - else accu + let accu = if RelDecl.is_local_assum p + then mkVar (NamedDecl.get_id decl) :: accu + else accu in shrink ctx sign c t accu | _ -> assert false @@ -4818,7 +4809,6 @@ let abstract_subproof id gk tac = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in - let open Context.Named.Declaration in Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let current_sign = Global.named_context() @@ -4828,7 +4818,7 @@ let abstract_subproof id gk tac = let sign,secsign = List.fold_right (fun d (s1,s2) -> - let id = get_id d in + let id = NamedDecl.get_id d in if mem_named_context id current_sign && interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d then (s1,push_named_context_val d s2) diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 30b7f299f..9a7ea3cde 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -25,6 +25,8 @@ open Globnames open Printer open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** For a constant c in a module sealed by an interface (M:T and not M<:T), [Global.lookup_constant] may return a [constant_body] without body. We fix this by looking in the implementation @@ -144,7 +146,7 @@ let label_of = function let rec traverse current ctx accu t = match kind_of_term t with | Var id -> - let body () = Global.lookup_named id |> get_value in + let body () = Global.lookup_named id |> NamedDecl.get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> let body () = Global.body_of_constant_body (lookup_constant kn) in diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 180b836ea..81e17ffb5 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -25,7 +25,8 @@ open Tactics open Ind_tables open Misctypes open Proofview.Notations -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration let out_punivs = Univ.out_punivs @@ -150,14 +151,14 @@ let build_beq_scheme mode kn = ( fun a b decl -> (* mkLambda(n,b,a) ) *) (* here I leave the Naming thingy so that the type of the function is more readable for the user *) - mkNamedLambda (eqName (get_name decl)) b a ) + mkNamedLambda (eqName (RelDecl.get_name decl)) b a ) c (List.rev eqs_typ) lnamesparrec in List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *) (* Same here , hoping the auto renaming will do something good ;) *) mkNamedLambda - (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") - (get_type decl) a) eq_input lnamesparrec + (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec in let make_one_eq cur = let u = Univ.Instance.empty in @@ -249,7 +250,7 @@ let build_beq_scheme mode kn = | 0 -> Lazy.force tt | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in for ndx = 0 to nb_cstr_args-1 do - let cc = get_type (List.nth constrsi.(i).cs_args ndx) in + let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in let eqA, eff' = compute_A_equality rel_list nparrec (nparrec+3+2*nb_cstr_args) @@ -268,14 +269,14 @@ let build_beq_scheme mode kn = (Array.sub eqs 1 (nb_cstr_args - 1)) ) in - (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) cc + (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) cc (constrsj.(j).cs_args) ) else ar2.(j) <- (List.fold_left (fun a decl -> - mkLambda (get_name decl, get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) ) + mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) ) done; - ar.(i) <- (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) + ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (mkCase (ci,do_predicate rel_list nb_cstr_args, mkVar (Id.of_string "Y") ,ar2)) (constrsi.(i).cs_args)) @@ -489,7 +490,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al )] *) let list_id l = List.fold_left ( fun a decl -> let s' = - match get_name decl with + match RelDecl.get_name decl with Name s -> Id.to_string s | Anonymous -> "A" in (Id.of_string s',Id.of_string ("eq_"^s'), @@ -537,8 +538,8 @@ let compute_bl_goal ind lnamesparrec nparrec = mkNamedProd seq b a ) bl_input (List.rev list_id) (List.rev eqs_typ) in List.fold_left (fun a decl -> mkNamedProd - (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") - (get_type decl) a) eq_input lnamesparrec + (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in @@ -680,8 +681,8 @@ let compute_lb_goal ind lnamesparrec nparrec = mkNamedProd seq b a ) lb_input (List.rev list_id) (List.rev eqs_typ) in List.fold_left (fun a decl -> mkNamedProd - (match (get_name decl) with Name s -> s | Anonymous -> Id.of_string "A") - (get_type decl) a) eq_input lnamesparrec + (match (RelDecl.get_name decl) with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in @@ -821,8 +822,8 @@ let compute_dec_goal ind lnamesparrec nparrec = mkNamedProd seq b a ) bl_input (List.rev list_id) (List.rev eqs_typ) in List.fold_left (fun a decl -> mkNamedProd - (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") - (get_type decl) a) eq_input lnamesparrec + (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index d6a6162f9..a6fb48749 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -22,6 +22,8 @@ open Constrintern open Constrexpr open Sigma.Notations open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*i*) open Decl_kinds @@ -77,13 +79,13 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m let type_ctx_instance evars env ctx inst subst = let rec aux (subst, instctx) l = function decl :: ctx -> - let t' = substl subst (get_type decl) in + let t' = substl subst (RelDecl.get_type decl) in let c', l = match decl with | LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l | LocalDef (_,b,_) -> substl subst b, l in - let d = get_name decl, Some c', t' in + let d = RelDecl.get_name decl, Some c', t' in aux (c' :: subst, d :: instctx) l ctx | [] -> subst in aux (subst, []) inst (List.rev ctx) @@ -156,7 +158,6 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let cl, u = Typeclasses.typeclass_univ_instance k in let _, args = List.fold_right (fun decl (args, args') -> - let open Context.Rel.Declaration in match decl with | LocalAssum _ -> (List.tl args, List.hd args :: args') | LocalDef (_,b,_) -> (args, substl args' b :: args')) @@ -229,7 +230,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p (fun (props, rest) decl -> if is_local_assum decl then try - let is_id (id', _) = match get_name decl, get_id id' with + let is_id (id', _) = match RelDecl.get_name decl, get_id id' with | Name id, (_, id') -> Id.equal id id' | Anonymous, _ -> false in @@ -347,7 +348,7 @@ let named_of_rel_context l = let acc, ctx = List.fold_right (fun decl (subst, ctx) -> - let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in + let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in let d = match decl with | LocalAssum (_,t) -> id, None, substl subst t | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in diff --git a/toplevel/command.ml b/toplevel/command.ml index 097865648..7274ac170 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -39,6 +39,8 @@ open Sigma.Notations open Context.Rel.Declaration open Entries +module RelDecl = Context.Rel.Declaration + let do_universe poly l = Declare.do_universe poly l let do_constraint poly l = Declare.do_constraint poly l @@ -457,7 +459,7 @@ let sign_level env evd sign = | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env - (nf_evar evd (Retyping.get_type_of env evd (get_type d)))) + (nf_evar evd (Retyping.get_type_of env evd (RelDecl.get_type d)))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) @@ -576,7 +578,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter is_local_assum ctx_params in - let params = List.map (fun decl -> out_name (get_name decl)) assums in + let params = List.map (fun decl -> out_name (RelDecl.get_name decl)) assums in (* Interpret the arities *) let arities = List.map (interp_ind_arity env_params evdref) indl in @@ -909,8 +911,8 @@ let rec telescope = function let ty, tys, (k, constr) = List.fold_left (fun (ty, tys, (k, constr)) decl -> - let t = get_type decl in - let pred = mkLambda (get_name decl, t, ty) in + let t = RelDecl.get_type decl in + let pred = mkLambda (RelDecl.get_name decl, t, ty) in let ty = Universes.constr_of_global (Lazy.force sigT).typ in let intro = Universes.constr_of_global (Lazy.force sigT).intro in let sigty = mkApp (ty, [|t; pred|]) in @@ -920,7 +922,7 @@ let rec telescope = function in let (last, subst) = List.fold_right2 (fun pred decl (prev, subst) -> - let t = get_type decl in + let t = RelDecl.get_type decl in let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in let proj1 = applistc p1 [t; pred; prev] in @@ -1133,7 +1135,7 @@ let interp_recursive isfix fixl notations = let evd, nf = nf_evars_and_universes evd in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in - let fixctxnames = List.map (fun (_,ctx) -> List.map get_name ctx) fixctxs in + let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in (* Build the fix declaration block *) (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ff4c18ad2..d2deb9e1e 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -25,6 +25,8 @@ open Printer open Evd open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* This simplifies the typing context of Cases clauses *) (* hope it does not disturb other typing contexts *) let contract env lc = @@ -35,9 +37,9 @@ let contract env lc = l := (Vars.substl !l c') :: !l; env | _ -> - let t' = Vars.substl !l (get_type decl) in - let c' = Option.map (Vars.substl !l) (get_value decl) in - let na' = named_hd env t' (get_name decl) in + let t' = Vars.substl !l (RelDecl.get_type decl) in + let c' = Option.map (Vars.substl !l) (RelDecl.get_value decl) in + let na' = named_hd env t' (RelDecl.get_name decl) in l := (mkRel 1) :: List.map (Vars.lift 1) !l; match c' with | None -> push_rel (LocalAssum (na',t')) env diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 29d745732..b3c1623e0 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -20,6 +20,8 @@ open Pp open CErrors open Util +module NamedDecl = Context.Named.Declaration + let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) @@ -51,7 +53,6 @@ type oblinfo = where n binders were passed through. *) let subst_evar_constr evs n idf t = - let open Context.Named.Declaration in let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in let evar_info id = List.assoc_f Evar.equal id evs in @@ -74,6 +75,7 @@ let subst_evar_constr evs n idf t = in let args = let rec aux hyps args acc = + let open Context.Named.Declaration in match hyps, args with (LocalAssum _ :: tlh), (c :: tla) -> aux tlh tla ((substrec (depth, fixrels) c) :: acc) @@ -116,9 +118,9 @@ let etype_of_evar evs hyps concl = let open Context.Named.Declaration in let rec aux acc n = function decl :: tl -> - let t', s, trans = subst_evar_constr evs n mkVar (get_type decl) in + let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in let t'' = subst_vars acc 0 t' in - let rest, s', trans' = aux (get_id decl :: acc) (succ n) tl in + let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in let s' = Int.Set.union s s' in let trans' = Id.Set.union trans trans' in (match decl with @@ -598,7 +600,6 @@ let decompose_lam_prod c ty = in aux Context.Rel.empty c ty let shrink_body c ty = - let open Context.Rel.Declaration in let ctx, b, ty = match ty with | None -> @@ -613,6 +614,7 @@ let shrink_body c ty = if noccurn 1 b && Option.cata (noccurn 1) true ty then subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args else + let open Context.Rel.Declaration in let args = if is_local_assum decl then mkRel i :: args else args in mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty, succ i, args) diff --git a/toplevel/record.ml b/toplevel/record.ml index 71d070776..9d14bdf4c 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -27,6 +27,8 @@ open Goptions open Sigma.Notations open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (********** definition d'un record (structure) **************) (** Flag governing use of primitive projections. Disabled by default. *) @@ -82,7 +84,7 @@ let compute_constructor_level evars env l = List.fold_right (fun d (env, univ) -> let univ = if is_local_assum d then - let s = Retyping.get_sort_of env evars (get_type d) in + let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in Univ.sup (univ_of_sort s) univ else univ in (push_rel d env, univ)) @@ -167,7 +169,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs let degenerate_decl decl = - let id = match get_name decl with + let id = match RelDecl.get_name decl with | Name id -> id | Anonymous -> anomaly (Pp.str "Unnamed record variable") in match decl with @@ -288,8 +290,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let (_,_,kinds,sp_projs,_) = List.fold_left3 (fun (nfi,i,kinds,sp_projs,subst) coe decl impls -> - let fi = get_name decl in - let ti = get_type decl in + let fi = RelDecl.get_name decl in + let ti = RelDecl.get_type decl in let (sp_projs,i,subst) = match fi with | Anonymous -> @@ -362,17 +364,17 @@ let structure_signature ctx = | [decl] -> let env = Environ.empty_named_context_val in let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in + let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in let evm = Sigma.to_evar_map evm in evm | decl::tl -> let env = Environ.empty_named_context_val in let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in + let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in let evm = Sigma.to_evar_map evm in let new_tl = Util.List.map_i (fun pos decl -> - map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in + RelDecl.map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in deps_to_evar evm new_tl in deps_to_evar Evd.empty (List.rev ctx) @@ -422,7 +424,7 @@ let implicits_of_context ctx = | Name n -> Some n | Anonymous -> None in ExplByPos (i, explname), (true, true, true)) - 1 (List.rev (Anonymous :: (List.map get_name ctx))) + 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) let declare_class finite def poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = @@ -476,13 +478,13 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity if b then Backward, pri else Forward, pri) coe) coers priorities in - let l = List.map3 (fun decl b y -> get_name decl, b, y) + let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) (List.rev fields) coers (Recordops.lookup_projections ind) in IndRef ind, l in let ctx_context = List.map (fun decl -> - match Typeclasses.class_of_constr (get_type decl) with + match Typeclasses.class_of_constr (RelDecl.get_type decl) with | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) | None -> None) params, params diff --git a/toplevel/search.ml b/toplevel/search.ml index e670b59b7..d1c108c37 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -20,6 +20,8 @@ open Globnames open Nametab open Goptions +module NamedDecl = Context.Named.Declaration + type filter_function = global_reference -> env -> constr -> bool type display_function = global_reference -> env -> constr -> unit @@ -68,8 +70,7 @@ let iter_constructors indsp u fn env nconstr = done let iter_named_context_name_type f = - let open Context.Named.Declaration in - List.iter (fun decl -> f (get_id decl) (get_type decl)) + List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl)) (* General search over hypothesis of a goal *) let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = @@ -81,13 +82,12 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = (* General search over declarations *) let iter_declarations (fn : global_reference -> env -> constr -> unit) = - let open Context.Named.Declaration in let env = Global.env () in let iter_obj (sp, kn) lobj = match object_tag lobj with | "VARIABLE" -> begin try let decl = Global.lookup_named (basename sp) in - fn (VarRef (get_id decl)) env (get_type decl) + fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl) with Not_found -> (* we are in a section *) () end | "CONSTANT" -> let cst = Global.constant_of_delta_kn kn in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f69c4fa18..5b746ca46 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -33,6 +33,8 @@ open Misctypes open Locality open Sigma.Notations +module NamedDecl = Context.Named.Declaration + (** TODO: make this function independent of Ltac *) let (f_interp_redexp, interp_redexp_hook) = Hook.make () @@ -848,14 +850,13 @@ let vernac_set_end_tac tac = (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) let vernac_set_used_variables e = - let open Context.Named.Declaration in let env = Global.env () in let tys = List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in let l = Proof_using.process_expr env e tys in let vars = Environ.named_context env in List.iter (fun id -> - if not (List.exists (Id.equal id % get_id) vars) then + if not (List.exists (Id.equal id % NamedDecl.get_id) vars) then errorlabstrm "vernac_set_used_variables" (str "Unknown variable: " ++ pr_id id)) l; @@ -1507,7 +1508,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = let natureofid = match decl with | LocalAssum _ -> "Hypothesis" | LocalDef (_,bdy,_) ->"Constant (let in)" in - v 0 (pr_id id ++ str":" ++ pr_constr (get_type decl) ++ fnl() ++ fnl() + v 0 (pr_id id ++ str":" ++ pr_constr (NamedDecl.get_type decl) ++ fnl() ++ fnl() ++ str natureofid ++ str " of the goal context.") with (* fallback to globals *) | NoHyp | Not_found -> print_about ref_or_by_not |