From 943e6b23229b5eed2fb8265089563ce0a25b9b44 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 29 Apr 2013 16:02:46 +0000 Subject: Merging Context and Sign. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7 --- dev/printers.mllib | 1 - interp/constrextern.mli | 1 - interp/constrintern.ml | 4 +- interp/constrintern.mli | 1 - interp/implicit_quantifiers.mli | 2 +- kernel/closure.ml | 2 +- kernel/context.ml | 60 ++++++++++++++++++++++ kernel/context.mli | 59 ++++++++++++++++++++-- kernel/cooking.ml | 7 ++- kernel/cooking.mli | 4 +- kernel/csymtable.ml | 2 +- kernel/declarations.mli | 4 +- kernel/declareops.ml | 2 +- kernel/entries.mli | 4 +- kernel/environ.ml | 17 +++---- kernel/environ.mli | 1 - kernel/inductive.ml | 4 +- kernel/kernel.mllib | 1 - kernel/nativecode.ml | 1 - kernel/pre_env.ml | 5 +- kernel/pre_env.mli | 1 - kernel/sign.ml | 88 --------------------------------- kernel/sign.mli | 67 ------------------------- kernel/term_typing.ml | 2 +- kernel/typeops.ml | 2 +- kernel/vars.mli | 1 - library/declare.mli | 2 +- library/decls.ml | 2 +- library/decls.mli | 2 +- library/global.mli | 2 +- library/lib.mli | 6 +-- plugins/funind/glob_term_to_relation.ml | 2 +- pretyping/coercion.mli | 2 +- pretyping/detyping.mli | 1 - pretyping/evarconv.mli | 2 +- pretyping/evarutil.ml | 8 +-- pretyping/evarutil.mli | 1 - pretyping/evd.mli | 2 +- pretyping/glob_ops.mli | 2 +- pretyping/inductiveops.mli | 1 - pretyping/patternops.mli | 2 +- pretyping/pretype_errors.mli | 2 +- pretyping/pretyping.ml | 1 - pretyping/pretyping.mli | 2 +- pretyping/term_dnet.mli | 2 +- pretyping/termops.ml | 14 +++--- pretyping/termops.mli | 1 - pretyping/typeclasses.ml | 1 - pretyping/typeclasses.mli | 1 - pretyping/typeclasses_errors.mli | 1 - printing/prettyp.mli | 2 +- printing/printer.ml | 3 +- printing/printer.mli | 1 - proofs/clenv.mli | 2 +- proofs/clenvtac.mli | 2 +- proofs/goal.mli | 4 +- proofs/logic.mli | 2 +- proofs/pfedit.ml | 2 +- proofs/pfedit.mli | 4 +- proofs/proof.ml | 2 +- proofs/proof.mli | 4 +- proofs/proof_global.mli | 2 +- proofs/refiner.ml | 4 +- proofs/refiner.mli | 2 +- proofs/tacmach.ml | 2 +- proofs/tacmach.mli | 1 - tactics/auto.mli | 1 - tactics/equality.ml | 4 +- tactics/equality.mli | 1 - tactics/hipattern.mli | 2 +- tactics/leminv.ml | 2 +- tactics/tacticals.ml | 2 +- tactics/tacticals.mli | 1 - tactics/tactics.ml | 11 ++--- tactics/tactics.mli | 1 - toplevel/auto_ind_decl.mli | 2 +- toplevel/autoinstance.mli | 1 - toplevel/classes.mli | 1 - toplevel/command.ml | 4 +- toplevel/discharge.ml | 2 +- toplevel/discharge.mli | 2 +- toplevel/himsg.ml | 2 +- toplevel/ind_tables.mli | 2 +- toplevel/lemmas.ml | 2 +- toplevel/obligations.ml | 4 +- toplevel/record.mli | 1 - 86 files changed, 210 insertions(+), 282 deletions(-) delete mode 100644 kernel/sign.ml delete mode 100644 kernel/sign.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index b09c8e97e..0f1686000 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -46,7 +46,6 @@ Context Vars Term Mod_subst -Sign Cbytecodes Copcodes Cemitcodes diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 4cf79337c..de4b13b06 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -11,7 +11,6 @@ open Names open Term open Context open Termops -open Sign open Environ open Libnames open Globnames diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4e63b16fa..c7f4635c9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -98,7 +98,7 @@ let global_reference id = let construct_reference ctx id = try - Term.mkVar (let _ = Sign.lookup_named id ctx in id) + Term.mkVar (let _ = Context.lookup_named id ctx in id) with Not_found -> global_reference id @@ -636,7 +636,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> (* Is [id] a goal or section variable *) - let _ = Sign.lookup_named id namedctx in + let _ = Context.lookup_named id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 1fa0db911..e352c7f7a 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -9,7 +9,6 @@ open Names open Term open Context -open Sign open Evd open Environ open Libnames diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 66be2ae5a..df29d0592 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -10,7 +10,7 @@ open Loc open Names open Decl_kinds open Term -open Sign +open Context open Evd open Environ open Nametab diff --git a/kernel/closure.ml b/kernel/closure.ml index 2628895eb..49fd1ae8e 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -262,7 +262,7 @@ let evar_value info ev = let defined_vars flags env = (* if red_local_const (snd flags) then*) - Sign.fold_named_context + Context.fold_named_context (fun (id,b,_) e -> match b with | None -> e diff --git a/kernel/context.ml b/kernel/context.ml index 4bc268da1..d24922e18 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -6,6 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Jean-Christophe Filliâtre out of names.ml as part of the + rebuilding of Coq around a purely functional abstract type-checker, + Aug 1999 *) +(* Miscellaneous extensions, restructurations and bug-fixes by Hugo + Herbelin and Bruno Barras *) + +(* This file defines types and combinators regarding indexes-based and + names-based contexts *) + +open Util open Names (***************************************************************************) @@ -62,3 +72,53 @@ let rel_context_nhyps hyps = | (_,None,_)::hyps -> nhyps (1+acc) hyps | (_,Some _,_)::hyps -> nhyps acc hyps in nhyps 0 hyps + +(*s Signatures of named hypotheses. Used for section variables and + goal assumptions. *) + +type named_context = named_declaration list + +let empty_named_context = [] + +let add_named_decl d sign = d::sign + +let rec lookup_named id = function + | (id',_,_ as decl) :: _ when Id.equal id id' -> decl + | _ :: sign -> lookup_named id sign + | [] -> raise Not_found + +let named_context_length = List.length +let named_context_equal = List.equal eq_named_declaration + +let vars_of_named_context = List.map (fun (id,_,_) -> id) + +let instance_from_named_context sign = + let rec inst_rec = function + | (id,None,_) :: sign -> Constr.mkVar id :: inst_rec sign + | _ :: sign -> inst_rec sign + | [] -> [] in + Array.of_list (inst_rec sign) + +let fold_named_context f l ~init = List.fold_right f l init +let fold_named_context_reverse f ~init l = List.fold_left f init l + +(*s Signatures of ordered section variables *) +type section_context = named_context + +let fold_rel_context f l ~init:x = List.fold_right f l x +let fold_rel_context_reverse f ~init:x l = List.fold_left f x l + +let map_context f l = + let map_decl (n, body_o, typ as decl) = + let body_o' = Option.smartmap f body_o in + let typ' = f typ in + if body_o' == body_o && typ' == typ then decl else + (n, body_o', typ') + in + List.smartmap map_decl l + +let map_rel_context = map_context +let map_named_context = map_context + +let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) +let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) diff --git a/kernel/context.mli b/kernel/context.mli index 32efb743a..79ddbe49b 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -8,7 +8,9 @@ open Names -(** {6 Local } *) +(** TODO: cleanup *) + +(** {6 Declarations} *) (** A {e declaration} has the form [(name,body,type)]. It is either an {e assumption} if [body=None] or a {e definition} if [body=Some actualbody]. It is referred by {e name} if [na] is an @@ -45,10 +47,61 @@ val eq_named_declaration : val eq_rel_declaration : rel_declaration -> rel_declaration -> bool -(** {6 Contexts of declarations referred to by de Bruijn indices } *) +(** {6 Signatures of ordered named declarations } *) -(** In [rel_context], more recent declaration is on top *) +type named_context = named_declaration list +type section_context = named_context type rel_context = rel_declaration list +(** In [rel_context], more recent declaration is on top *) + +val empty_named_context : named_context +val add_named_decl : named_declaration -> named_context -> named_context +val vars_of_named_context : named_context -> Id.t list + +val lookup_named : Id.t -> named_context -> named_declaration + +(** number of declarations *) +val named_context_length : named_context -> int + +(** named context equality *) +val named_context_equal : named_context -> named_context -> bool + +(** {6 Recurrence on [named_context]: older declarations processed first } *) +val fold_named_context : + (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a + +(** newer declarations first *) +val fold_named_context_reverse : + ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a + +(** {6 Section-related auxiliary functions } *) +val instance_from_named_context : named_context -> Constr.t array + +(** {6 ... } *) +(** Signatures of ordered optionally named variables, intended to be + accessed by de Bruijn indices *) + +(** {6 Recurrence on [rel_context]: older declarations processed first } *) +val fold_rel_context : + (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a + +(** newer declarations first *) +val fold_rel_context_reverse : + ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a + +(** {6 Map function of [rel_context] } *) +val map_rel_context : (Constr.t -> Constr.t) -> rel_context -> rel_context + +(** {6 Map function of [named_context] } *) +val map_named_context : (Constr.t -> Constr.t) -> named_context -> named_context + +(** {6 Map function of [rel_context] } *) +val iter_rel_context : (Constr.t -> unit) -> rel_context -> unit + +(** {6 Map function of [named_context] } *) +val iter_named_context : (Constr.t -> unit) -> named_context -> unit + +(** {6 Contexts of declarations referred to by de Bruijn indices } *) val empty_rel_context : rel_context val add_rel_decl : rel_declaration -> rel_context -> rel_context diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 0851f682d..bb29b9645 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -18,7 +18,6 @@ open Util open Names open Term open Context -open Sign open Declarations open Environ @@ -124,7 +123,7 @@ type inline = bool type result = constant_def * constant_type * Univ.constraints * inline - * Sign.section_context option + * Context.section_context option let on_body f = function | Undef inl -> Undef inl @@ -139,13 +138,13 @@ let constr_of_def = function let cook_constant env r = let cb = r.d_from in - let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in + let hyps = Context.map_named_context (expmod_constr r.d_modlist) r.d_abstract in let body = on_body (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps) cb.const_body in let const_hyps = - Sign.fold_named_context (fun (h,_,_) hyps -> + Context.fold_named_context (fun (h,_,_) hyps -> List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with diff --git a/kernel/cooking.mli b/kernel/cooking.mli index d6280e119..8d046a12e 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -18,14 +18,14 @@ type work_list = Id.t array Cmap.t * Id.t array Mindmap.t type recipe = { d_from : constant_body; - d_abstract : Sign.named_context; + d_abstract : Context.named_context; d_modlist : work_list } type inline = bool type result = constant_def * constant_type * constraints * inline - * Sign.section_context option + * Context.section_context option val cook_constant : env -> recipe -> result diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index d00a20a80..146b6a1ec 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -115,7 +115,7 @@ and slot_for_fv env fv = match !nv with | VKvalue (v,_) -> v | VKnone -> - let (_, b, _) = Sign.lookup_named id env.env_named_context in + let (_, b, _) = Context.lookup_named id env.env_named_context in let v,d = match b with | None -> (val_of_named id, Id.Set.empty) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 5d9eaa928..24572da59 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -47,7 +47,7 @@ type native_name = | NotLinked type constant_body = { - const_hyps : Sign.section_context; (** New: younger hyp at top *) + const_hyps : Context.section_context; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted; @@ -132,7 +132,7 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Sign.section_context; (** Section hypotheses on which the block depends *) + mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 3c1f6a415..64496033a 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -166,7 +166,7 @@ let subst_mind sub mib = mind_nparams = mib.mind_nparams; mind_nparams_rec = mib.mind_nparams_rec; mind_params_ctxt = - Sign.map_rel_context (subst_mps sub) mib.mind_params_ctxt; + Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_constraints = mib.mind_constraints; mind_native_name = ref NotLinked } diff --git a/kernel/entries.mli b/kernel/entries.mli index 650c3566d..b2d65d3ed 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -50,14 +50,14 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; - const_entry_secctx : Sign.section_context option; + const_entry_secctx : Context.section_context option; const_entry_type : types option; const_entry_opaque : bool; const_entry_inline_code : bool } type inline = int option (* inlining level, None for no inlining *) -type parameter_entry = Sign.section_context option * types * inline +type parameter_entry = Context.section_context option * types * inline type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/environ.ml b/kernel/environ.ml index d3b223505..4a3e51aa1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -25,7 +25,6 @@ open Util open Names open Term open Context -open Sign open Vars open Univ open Declarations @@ -68,7 +67,7 @@ let nb_rel env = env.env_nb_rel let push_rel = push_rel -let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x +let push_rel_context ctxt x = Context.fold_rel_context push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in @@ -110,8 +109,8 @@ let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named id env = Sign.lookup_named id env.env_named_context -let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt +let lookup_named id env = Context.lookup_named id env.env_named_context +let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt let eq_named_context_val c1 c2 = c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2) @@ -150,7 +149,7 @@ let fold_named_context f env ~init = in fold_right env let fold_named_context_reverse f ~init env = - Sign.fold_named_context_reverse f ~init:init (named_context env) + Context.fold_named_context_reverse f ~init:init (named_context env) (* Global constants *) @@ -216,11 +215,11 @@ let set_engagement c env = (* Unsafe *) (* Lookup of section variables *) let lookup_constant_variables c env = let cmap = lookup_constant c env in - Sign.vars_of_named_context cmap.const_hyps + Context.vars_of_named_context cmap.const_hyps let lookup_inductive_variables (kn,i) env = let mis = lookup_mind kn env in - Sign.vars_of_named_context mis.mind_hyps + Context.vars_of_named_context mis.mind_hyps let lookup_constructor_variables (ind,_) env = lookup_inductive_variables ind env @@ -254,7 +253,7 @@ let global_vars_set env constr = let keep_hyps env needed = let really_needed = - Sign.fold_named_context_reverse + Context.fold_named_context_reverse (fun need (id,copt,t) -> if Id.Set.mem id need then let globc = @@ -267,7 +266,7 @@ let keep_hyps env needed = else need) ~init:needed (named_context env) in - Sign.fold_named_context + Context.fold_named_context (fun (id,_,_ as d) nsign -> if Id.Set.mem id really_needed then add_named_decl d nsign else nsign) diff --git a/kernel/environ.mli b/kernel/environ.mli index ffe28ddc4..ffa3ceb87 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -10,7 +10,6 @@ open Names open Term open Context open Declarations -open Sign (** Unsafe environments. We define here a datatype for environments. Since typing is not yet defined, it is not possible to check the diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ef4416061..ee311ab24 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -68,7 +68,7 @@ let instantiate_params full t args sign = let fail () = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = - Sign.fold_rel_context + Context.fold_rel_context (fun (_,copt,_) (largs,subs,ty) -> match (copt, largs, kind_of_term ty) with | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) @@ -240,7 +240,7 @@ let type_of_constructors ind (mib,mip) = let local_rels ctxt = let (rels,_) = - Sign.fold_rel_context_reverse + Context.fold_rel_context_reverse (fun (rels,n) (_,copt,_) -> match copt with None -> (mkRel n :: rels, n+1) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 421003560..36b3d8323 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -7,7 +7,6 @@ Context Vars Term Mod_subst -Sign Cbytecodes Copcodes Cemitcodes diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index f112393cd..20593744b 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -14,7 +14,6 @@ open Util open Nativevalues open Nativelambda open Pre_env -open Sign (** This file defines the mllambda code generation phase of the native compiler. mllambda represents a fragment of ML, and can easily be printed diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 922fbae92..61fb6b07b 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -16,7 +16,6 @@ open Util open Names open Context -open Sign open Univ open Term open Declarations @@ -105,7 +104,7 @@ let env_of_rel n env = let push_named_context_val d (ctxt,vals) = let id,_,_ = d in let rval = ref VKnone in - Sign.add_named_decl d ctxt, (id,rval)::vals + Context.add_named_decl d ctxt, (id,rval)::vals let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); @@ -113,7 +112,7 @@ let push_named d env = let id,body,_ = d in let rval = ref VKnone in { env with - env_named_context = Sign.add_named_decl d env.env_named_context; + env_named_context = Context.add_named_decl d env.env_named_context; env_named_vals = (id,rval):: env.env_named_vals } let lookup_named_val id env = diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index d3d500b2c..10c9c27cb 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Sign open Univ open Term open Context diff --git a/kernel/sign.ml b/kernel/sign.ml deleted file mode 100644 index 66c872f12..000000000 --- a/kernel/sign.ml +++ /dev/null @@ -1,88 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* decl - | _ :: sign -> lookup_named id sign - | [] -> raise Not_found - -let named_context_length = List.length -let named_context_equal = List.equal eq_named_declaration - -let vars_of_named_context = List.map (fun (id,_,_) -> id) - -let instance_from_named_context sign = - let rec inst_rec = function - | (id,None,_) :: sign -> mkVar id :: inst_rec sign - | _ :: sign -> inst_rec sign - | [] -> [] in - Array.of_list (inst_rec sign) - -let fold_named_context f l ~init = List.fold_right f l init -let fold_named_context_reverse f ~init l = List.fold_left f init l - -(*s Signatures of ordered section variables *) -type section_context = named_context - -let fold_rel_context f l ~init:x = List.fold_right f l x -let fold_rel_context_reverse f ~init:x l = List.fold_left f x l - -let map_context f l = - let map_decl (n, body_o, typ as decl) = - let body_o' = Option.smartmap f body_o in - let typ' = f typ in - if body_o' == body_o && typ' == typ then decl else - (n, body_o', typ') - in - List.smartmap map_decl l - -let map_rel_context = map_context -let map_named_context = map_context - -let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) -let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) - -(* Push named declarations on top of a rel context *) -(* Bizarre. Should be avoided. *) -(*let push_named_to_rel_context hyps ctxt = - let rec push = function - | (id,b,t) :: l -> - let s, hyps = push l in - let d = (Name id, Option.map (subst_vars s) b, subst_vars s t) in - id::s, d::hyps - | [] -> [],[] in - let s, hyps = push hyps in - let rec subst = function - | d :: l -> - let n, ctxt = subst l in - (n+1), (map_rel_declaration (substn_vars n s) d)::ctxt - | [] -> 1, hyps in - snd (subst ctxt)*) diff --git a/kernel/sign.mli b/kernel/sign.mli deleted file mode 100644 index 6e581df34..000000000 --- a/kernel/sign.mli +++ /dev/null @@ -1,67 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* named_context -> named_context -val vars_of_named_context : named_context -> Id.t list - -val lookup_named : Id.t -> named_context -> named_declaration - -(** number of declarations *) -val named_context_length : named_context -> int - -(** named context equality *) -val named_context_equal : named_context -> named_context -> bool - -(** {6 Recurrence on [named_context]: older declarations processed first } *) -val fold_named_context : - (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a - -(** newer declarations first *) -val fold_named_context_reverse : - ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a - -(** {6 Section-related auxiliary functions } *) -val instance_from_named_context : named_context -> constr array - -(** {6 ... } *) -(** Signatures of ordered optionally named variables, intended to be - accessed by de Bruijn indices *) - -(* val push_named_to_rel_context : named_context -> rel_context -> rel_context *) - -(** {6 Recurrence on [rel_context]: older declarations processed first } *) -val fold_rel_context : - (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a - -(** newer declarations first *) -val fold_rel_context_reverse : - ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a - -(** {6 Map function of [rel_context] } *) -val map_rel_context : (constr -> constr) -> rel_context -> rel_context - -(** {6 Map function of [named_context] } *) -val map_named_context : (constr -> constr) -> named_context -> named_context - -(** {6 Map function of [rel_context] } *) -val iter_rel_context : (constr -> unit) -> rel_context -> unit - -(** {6 Map function of [named_context] } *) -val iter_named_context : (constr -> unit) -> named_context -> unit diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3653e1954..83d1ce16c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -76,7 +76,7 @@ let infer_declaration env = function let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t | PolymorphicArity (ctx,_) -> - Sign.fold_rel_context + Context.fold_rel_context (fold_rel_declaration (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty diff --git a/kernel/typeops.ml b/kernel/typeops.ml index a27ce1c47..cc7cf0c68 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -97,7 +97,7 @@ let judge_of_variable env id = variables of the current env *) (* TODO: check order? *) let check_hyps_inclusion env c sign = - Sign.fold_named_context + Context.fold_named_context (fun (id,_,ty1) () -> try let ty2 = named_type id env in diff --git a/kernel/vars.mli b/kernel/vars.mli index 240d4d413..55a28516b 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -9,7 +9,6 @@ open Names open Term open Context -open Sign (** {6 Occur checks } *) diff --git a/library/declare.mli b/library/declare.mli index fa9917a13..602cd64fa 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -9,7 +9,7 @@ open Names open Libnames open Term -open Sign +open Context open Declarations open Entries open Indtypes diff --git a/library/decls.ml b/library/decls.ml index a93913a77..2d8807f80 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -11,7 +11,7 @@ open Util open Names -open Sign +open Context open Decl_kinds open Libnames diff --git a/library/decls.mli b/library/decls.mli index 87d963cd4..001d060e8 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Sign +open Context open Libnames open Decl_kinds diff --git a/library/global.mli b/library/global.mli index a06d4640e..6ca5bfb83 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,7 +31,7 @@ val env_is_empty : unit -> bool val universes : unit -> universes val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Sign.named_context +val named_context : unit -> Context.named_context val env_is_empty : unit -> bool diff --git a/library/lib.mli b/library/lib.mli index a37d7a113..ce57721fb 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -187,7 +187,7 @@ type variable_info = Names.Id.t * Decl_kinds.binding_kind * type variable_context = variable_info list val instance_from_variable_context : variable_context -> Names.Id.t array -val named_of_variable_context : variable_context -> Sign.named_context +val named_of_variable_context : variable_context -> Context.named_context val section_segment_of_constant : Names.constant -> variable_context val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context @@ -197,8 +197,8 @@ val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> unit -val add_section_constant : Names.constant -> Sign.named_context -> unit -val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit +val add_section_constant : Names.constant -> Context.named_context -> unit +val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit val replacement_context : unit -> (Names.Id.t array Names.Cmap.t * Names.Id.t array Names.Mindmap.t) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 2b4b6245a..e98a0952b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env = let new_env = add_pat_variables env pat typ in let res = fst ( - Sign.fold_rel_context + Context.fold_rel_context (fun (na,v,t) (env,ctxt) -> match na with | Anonymous -> assert false diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 4330948aa..b397cc3d5 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -10,7 +10,7 @@ open Pp open Evd open Names open Term -open Sign +open Context open Environ open Evarutil open Glob_term diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index f2f5c9eff..cb478777f 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -11,7 +11,6 @@ open Pp open Names open Term open Context -open Sign open Environ open Glob_term open Termops diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 30495857a..9d0c79143 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -8,7 +8,7 @@ open Names open Term -open Sign +open Context open Environ open Termops open Reductionops diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 5719d750e..14c102cbc 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -62,10 +62,10 @@ let env_nf_betaiotaevar sigma env = push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env let nf_named_context_evar sigma ctx = - Sign.map_named_context (Reductionops.nf_evar sigma) ctx + Context.map_named_context (Reductionops.nf_evar sigma) ctx let nf_rel_context_evar sigma ctx = - Sign.map_rel_context (Reductionops.nf_evar sigma) ctx + Context.map_rel_context (Reductionops.nf_evar sigma) ctx let nf_env_evar sigma env = let nc' = nf_named_context_evar sigma (Environ.named_context env) in @@ -305,7 +305,7 @@ let push_rel_context_to_named_context env typ = (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, _, env) = - Sign.fold_rel_context + Context.fold_rel_context (fun (na,c,t) (subst, avoid, env) -> let id = next_name_away na avoid in let d = (id,Option.map (substl subst) c,substl subst t) in @@ -433,7 +433,7 @@ let rec check_and_clear_in_constr evdref err ids c = begin match rids with | [] -> c | _ -> - let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in + let env = Context.fold_named_context push_named nhyps ~init:(empty_env) in let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in evdref := Evd.define evk ev' !evdref; let (evk',_) = destEvar ev' in diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 26d85ac94..889b2c9bf 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -12,7 +12,6 @@ open Names open Glob_term open Term open Context -open Sign open Evd open Environ open Reductionops diff --git a/pretyping/evd.mli b/pretyping/evd.mli index f7ec791b7..52c24a3f2 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -10,7 +10,7 @@ open Loc open Pp open Names open Term -open Sign +open Context open Environ open Libnames open Mod_subst diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 730332514..4e8224879 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -8,7 +8,7 @@ open Pp open Names -open Sign +open Context open Term open Libnames open Nametab diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 038bf465a..204f506a6 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -12,7 +12,6 @@ open Context open Declarations open Environ open Evd -open Sign (** The following three functions are similar to the ones defined in Inductive, but they expect an env *) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 8148fe25d..4a4649cca 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -8,7 +8,7 @@ open Pp open Names -open Sign +open Context open Term open Environ open Globnames diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 69994531d..996b75146 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -9,7 +9,7 @@ open Pp open Names open Term -open Sign +open Context open Environ open Glob_term open Inductiveops diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 26325872f..6253fcfbf 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -25,7 +25,6 @@ open Pp open Errors open Util open Names -open Sign open Evd open Term open Vars diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index e637d2b8e..04d29ac28 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -13,7 +13,7 @@ implicit arguments. *) open Names -open Sign +open Context open Term open Environ open Evd diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli index bf4557fc2..57ae3a857 100644 --- a/pretyping/term_dnet.mli +++ b/pretyping/term_dnet.mli @@ -7,7 +7,7 @@ (************************************************************************) open Term -open Sign +open Context open Libnames open Mod_subst diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 0128f8bde..8a5a82803 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -827,9 +827,9 @@ let subst_closed_term_occ_decl_modulo (plocs,hyploc) test d = let vars_of_env env = let s = - Sign.fold_named_context (fun (id,_,_) s -> Id.Set.add id s) + Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s) (named_context env) ~init:Id.Set.empty in - Sign.fold_rel_context + Context.fold_rel_context (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s) (rel_context env) ~init:s @@ -855,12 +855,12 @@ let lookup_rel_of_name id names = let empty_names_context = [] let ids_of_rel_context sign = - Sign.fold_rel_context + Context.fold_rel_context (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) sign ~init:[] let ids_of_named_context sign = - Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[] + Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[] let ids_of_context env = (ids_of_rel_context (rel_context env)) @@ -997,10 +997,10 @@ let process_rel_context f env = let sign = named_context_val env in let rels = rel_context env in let env0 = reset_with_named_context sign env in - Sign.fold_rel_context f rels ~init:env0 + Context.fold_rel_context f rels ~init:env0 let assums_of_rel_context sign = - Sign.fold_rel_context + Context.fold_rel_context (fun (na,c,t) l -> match c with Some _ -> l @@ -1072,7 +1072,7 @@ let global_vars_set_of_decl env = function let dependency_closure env sign hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = - Sign.fold_named_context_reverse + Context.fold_named_context_reverse (fun (hs,hl) (x,_,_ as d) -> if Id.Set.mem x hs then (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs), diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 9547231af..552513a27 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -11,7 +11,6 @@ open Pp open Names open Term open Context -open Sign open Environ open Locus diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 53171d02c..4dc6280f1 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -13,7 +13,6 @@ open Decl_kinds open Term open Vars open Context -open Sign open Evd open Environ open Util diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index af6824924..46877a58f 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -11,7 +11,6 @@ open Globnames open Decl_kinds open Term open Context -open Sign open Evd open Environ open Nametab diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index f80ff00fc..a55b9204e 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -11,7 +11,6 @@ open Names open Decl_kinds open Term open Context -open Sign open Evd open Environ open Nametab diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 2747abe60..1bf8c6ab3 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -8,7 +8,7 @@ open Pp open Names -open Sign +open Context open Term open Environ open Reductionops diff --git a/printing/printer.ml b/printing/printer.ml index 27266cfe1..5d63d179d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -12,7 +12,6 @@ open Util open Names open Term open Vars -open Sign open Context open Environ open Globnames @@ -245,7 +244,7 @@ let pr_named_context_of env = hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) let pr_named_context env ne_context = - hv 0 (Sign.fold_named_context + hv 0 (Context.fold_named_context (fun d pps -> pps ++ ws 2 ++ pr_var_decl env d) ne_context ~init:(mt ())) diff --git a/printing/printer.mli b/printing/printer.mli index 55058ae16..fea8c0673 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -12,7 +12,6 @@ open Libnames open Globnames open Term open Context -open Sign open Environ open Glob_term open Pattern diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 461b38a6a..bfb5ee27c 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -8,7 +8,7 @@ open Names open Term -open Sign +open Context open Environ open Evd open Evarutil diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index cf8c5dff8..dd46f1ec7 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -8,7 +8,7 @@ open Names open Term -open Sign +open Context open Evd open Clenv open Proof_type diff --git a/proofs/goal.mli b/proofs/goal.mli index 4cd3e4746..bb1c0639e 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -191,7 +191,7 @@ module V82 : sig val extra : Evd.evar_map -> goal -> Evd.Store.t (* Old style filtered_context primitive *) - val filtered_context : Evd.evar_map -> goal -> Sign.named_context + val filtered_context : Evd.evar_map -> goal -> Context.named_context (* Old style mk_goal primitive, returns a new goal with corresponding hypotheses and conclusion, together with a term which is precisely @@ -228,7 +228,7 @@ module V82 : sig val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Sign.named_context -> goal Evd.sigma + val new_goal_with : Evd.evar_map -> goal -> Context.named_context -> goal Evd.sigma (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map diff --git a/proofs/logic.mli b/proofs/logic.mli index 40feb5c56..eff766b7c 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -8,7 +8,7 @@ open Names open Term -open Sign +open Context open Evd open Environ open Proof_type diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d8609ed80..c07db32b7 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -176,7 +176,7 @@ let solve_by_implicit_tactic env sigma (evk,args) = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac) with e when Logic.catchable_exception e -> raise Exit) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 9d22b60e0..090edde5a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -10,7 +10,7 @@ open Loc open Pp open Names open Term -open Sign +open Context open Environ open Decl_kinds open Tacmach @@ -141,7 +141,7 @@ val set_end_tac : tactic -> unit (** [set_used_variables l] declares that section variables [l] will be used in the proof *) val set_used_variables : Id.t list -> unit -val get_used_variables : unit -> Sign.section_context option +val get_used_variables : unit -> Context.section_context option (** {6 ... } *) (** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the diff --git a/proofs/proof.ml b/proofs/proof.ml index c38f80a55..6cc43de72 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -127,7 +127,7 @@ type proof_state = { type proof_info = { mutable endline_tactic : unit Proofview.tactic ; - mutable section_vars : Sign.section_context option; + mutable section_vars : Context.section_context option; initial_conclusions : Term.types list } diff --git a/proofs/proof.mli b/proofs/proof.mli index 7d82ee91e..b563452a9 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -139,8 +139,8 @@ val is_last_focus : 'a focus_kind -> proof -> bool val no_focused_goal : proof -> bool (* Sets the section variables assumed by the proof *) -val set_used_variables : Sign.section_context -> proof -> unit -val get_used_variables : proof -> Sign.section_context option +val set_used_variables : Context.section_context -> proof -> unit +val get_used_variables : proof -> Context.section_context option (*** Endline tactic ***) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index c1ca6a694..7fa44cf86 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -78,7 +78,7 @@ val set_endline_tactic : unit Proofview.tactic -> unit (** Sets the section variables assumed by the proof *) val set_used_variables : Names.Id.t list -> unit -val get_used_variables : unit -> Sign.section_context option +val get_used_variables : unit -> Context.section_context option (** Appends the endline tactic of the current proof to a tactic. *) val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 04d125804..5a71b6816 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -190,10 +190,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal = something similar (better?) in the xml protocol. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Sign.named_context = pf_hyps goal in + let oldhyps:Context.named_context = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let {it=gls;sigma=sigma} = rslt in - let hyps:Sign.named_context list = + let hyps:Context.named_context list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma}) gls in let newhyps = List.map (fun hypl -> List.subtract hypl oldhyps) hyps in diff --git a/proofs/refiner.mli b/proofs/refiner.mli index d353a566f..c198958e3 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -7,7 +7,7 @@ (************************************************************************) open Term -open Sign +open Context open Evd open Proof_type open Tacexpr diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 2b5114174..813a0d850 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -51,7 +51,7 @@ let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = try - Sign.lookup_named id (pf_hyps gls) + Context.lookup_named id (pf_hyps gls) with Not_found -> error ("No such hypothesis: " ^ (Id.to_string id)) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 5b502f2c9..1c0ab2d14 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -9,7 +9,6 @@ open Names open Term open Context -open Sign open Environ open Evd open Reduction diff --git a/tactics/auto.mli b/tactics/auto.mli index a93f9be26..99f4768c2 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -9,7 +9,6 @@ open Names open Term open Context -open Sign open Proof_type open Tacmach open Clenv diff --git a/tactics/equality.ml b/tactics/equality.ml index 18e582b31..2dc42e35f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1392,7 +1392,7 @@ user = raise user error specific to rewrite let unfold_body x gl = let hyps = pf_hyps gl in let xval = - match Sign.lookup_named x hyps with + match Context.lookup_named x hyps with (_,Some xval,_) -> xval | _ -> errorlabstrm "unfold_body" (pr_id x ++ str" is not a defined hypothesis.") in @@ -1474,7 +1474,7 @@ let subst_one_var dep_proof_ok x gl = let (hyp,rhs,dir) = try let test hyp _ = is_eq_x gl varx hyp in - Sign.fold_named_context test ~init:() hyps; + Context.fold_named_context test ~init:() hyps; errorlabstrm "Subst" (str "Cannot find any non-recursive equality over " ++ pr_id x ++ str".") diff --git a/tactics/equality.mli b/tactics/equality.mli index d341db4f4..aa1bfaa0f 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -11,7 +11,6 @@ open Pp open Names open Term open Context -open Sign open Evd open Environ open Proof_type diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 1367bb87a..b38eb654b 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -8,7 +8,7 @@ open Names open Term -open Sign +open Context open Evd open Pattern open Coqlib diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 86651e76c..ac4cd5442 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -14,7 +14,7 @@ open Term open Vars open Termops open Namegen -open Sign +open Context open Evd open Printer open Reductionops diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index b2d39b57a..4625cc84b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -12,7 +12,7 @@ open Util open Names open Term open Termops -open Sign +open Context open Declarations open Tacmach open Clenv diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 3ab04dcbd..13eaaff5c 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -11,7 +11,6 @@ open Pp open Names open Term open Context -open Sign open Tacmach open Proof_type open Clenv diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a4b89f865..21487a36d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -11,7 +11,6 @@ open Errors open Util open Names open Nameops -open Sign open Term open Vars open Context @@ -1552,7 +1551,7 @@ let generalize_dep ?(with_let=false) c gl = d::toquant else toquant in - let to_quantify = Sign.fold_named_context seek sign ~init:[] in + let to_quantify = Context.fold_named_context seek sign ~init:[] in let to_quantify_rev = List.rev to_quantify in let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in @@ -1837,7 +1836,7 @@ let assert_by na t tac = forward (Some tac) (ipat_of_name na) t let unfold_body x gl = let hyps = pf_hyps gl in let xval = - match Sign.lookup_named x hyps with + match Context.lookup_named x hyps with (_,Some xval,_) -> xval | _ -> errorlabstrm "unfold_body" (pr_id x ++ str" is not a defined hypothesis.") in @@ -2387,7 +2386,7 @@ let hyps_of_vars env sign nogen hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = - Sign.fold_named_context_reverse + Context.fold_named_context_reverse (fun (hs,hl) (x,_,_ as d) -> if Id.Set.mem x nogen then (hs,hl) else if Id.Set.mem x hs then (hs,x::hl) @@ -3526,7 +3525,7 @@ let abstract_subproof id tac gl = List.fold_right (fun (id,_,_ as d) (s1,s2) -> if mem_named_context id current_sign & - interpretable_as_section_decl (Sign.lookup_named id current_sign) d + interpretable_as_section_decl (Context.lookup_named id current_sign) d then (s1,push_named_context_val d s2) else (add_named_decl d s1,s2)) global_sign (empty_named_context,empty_named_context_val) in @@ -3562,7 +3561,7 @@ let admit_as_an_axiom gl = List.fold_right (fun (id,_,_ as d) (s1,s2) -> if mem_named_context id current_sign & - interpretable_as_section_decl (Sign.lookup_named id current_sign) d + interpretable_as_section_decl (Context.lookup_named id current_sign) d then (s1,add_named_decl d s2) else (add_named_decl d s1,s2)) global_sign (empty_named_context,empty_named_context) in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f39ed97f8..2b45ecde6 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -12,7 +12,6 @@ open Names open Term open Context open Environ -open Sign open Tacmach open Proof_type open Reduction diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 1eaf6b768..b05f94c3c 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -10,7 +10,7 @@ open Term open Names open Libnames open Mod_subst -open Sign +open Context open Proof_type open Ind_tables diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli index fcd46c3e8..ebaaee12d 100644 --- a/toplevel/autoinstance.mli +++ b/toplevel/autoinstance.mli @@ -12,7 +12,6 @@ open Typeclasses open Names open Evd open Context -open Sign (** {6 Automatic detection of (some) record instances } *) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index d05eff126..0a71921b0 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -10,7 +10,6 @@ open Names open Decl_kinds open Term open Context -open Sign open Evd open Environ open Nametab diff --git a/toplevel/command.ml b/toplevel/command.ml index 6a3d9a11a..e3a299340 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -316,10 +316,10 @@ let interp_mutual_inductive (paramsl,indl) notations finite = let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env_params evd in let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in - let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in + let ctx_params = Context.map_rel_context (nf_evar sigma) ctx_params in let arities = List.map (nf_evar sigma) arities in List.iter (check_evars env_params Evd.empty evd) arities; - Sign.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; + Context.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; List.iter (fun (_,ctyps,_) -> List.iter (check_evars env_ar_params Evd.empty evd) ctyps) constructors; diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index aeb63c348..8d9e73e6d 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -9,7 +9,7 @@ open Names open Errors open Util -open Sign +open Context open Term open Vars open Entries diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index 8c64f3ed0..a74f69456 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Sign +open Context open Cooking open Declarations open Entries diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b289bb9b0..dc906d281 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -14,7 +14,7 @@ open Namegen open Term open Termops open Indtypes -open Sign +open Context open Environ open Pretype_errors open Type_errors diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 35ceef86a..9dd25c63e 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -10,7 +10,7 @@ open Term open Names open Libnames open Mod_subst -open Sign +open Context open Declarations (** This module provides support for registering inductive scheme builders, diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 3779815e9..b237a4762 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -344,7 +344,7 @@ let start_proof_com kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in let t', imps' = interp_type_evars_impls ~impls ~evdref env t in - Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx; + Context.iter_rel_context (check_evars env Evd.empty !evdref) ctx; let ids = List.map pi1 ctx in (compute_proof_name (fst kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 53ee27f3b..a369bf505 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -13,7 +13,7 @@ open Declare *) open Term -open Sign +open Context open Vars open Names open Evd @@ -205,7 +205,7 @@ open Environ let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) let nc = Environ.named_context env in - let nc_len = Sign.named_context_length nc in + let nc_len = Context.named_context_length nc in let evm = Evarutil.nf_evar_map_undefined evm in let evl = List.rev (Evarutil.non_instantiated evm) in let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in diff --git a/toplevel/record.mli b/toplevel/record.mli index 331bf9ed5..018366667 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -9,7 +9,6 @@ open Names open Term open Context -open Sign open Vernacexpr open Constrexpr open Impargs -- cgit v1.2.3