From bedaec8452d0600ede52efeeac016c9d323c66de Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 18 Oct 2000 14:37:44 +0000 Subject: Renommage canonique : declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/closure.ml | 2 +- kernel/declarations.ml | 4 +-- kernel/declarations.mli | 7 +++-- kernel/environ.ml | 84 ++++++++++++++++++++++++------------------------- kernel/environ.mli | 58 +++++++++++++++++----------------- kernel/evd.ml | 2 +- kernel/evd.mli | 2 +- kernel/indtypes.ml | 8 ++--- kernel/instantiate.ml | 2 +- kernel/instantiate.mli | 4 +-- kernel/reduction.ml | 20 ++++++------ kernel/safe_typing.ml | 50 ++++++++++++++--------------- kernel/safe_typing.mli | 16 +++++----- kernel/sign.ml | 44 +++++++++++++------------- kernel/sign.mli | 55 +++++++++++++++++--------------- kernel/term.ml | 2 +- kernel/term.mli | 53 ++++++++++++------------------- kernel/typeops.ml | 28 ++++++++--------- kernel/typeops.mli | 4 +-- 19 files changed, 216 insertions(+), 229 deletions(-) (limited to 'kernel') diff --git a/kernel/closure.ml b/kernel/closure.ml index 71bfa0778f..ae5e51db0f 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -294,7 +294,7 @@ let make_constr_ref n = function let defined_vars flags env = if red_local_const (snd flags) then - fold_var_context + fold_named_context (fun env (id,b,t) e -> match b with | None -> e diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 82ad0583ce..3b2ba2ecef 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -19,7 +19,7 @@ type constant_body = { const_kind : path_kind; const_body : constant_value option; const_type : typed_type; - const_hyps : var_context; + const_hyps : named_context; const_constraints : constraints; mutable const_opaque : bool } @@ -61,7 +61,7 @@ type one_inductive_body = { type mutual_inductive_body = { mind_kind : path_kind; mind_ntypes : int; - mind_hyps : var_context; + mind_hyps : named_context; mind_packets : one_inductive_body array; mind_constraints : constraints; mind_singl : constr option; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 65f70e2776..3a85e7e05f 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -8,6 +8,9 @@ open Term open Sign (*i*) +(* This module defines the types of global declarations. This includes + global constants/axioms and mutual inductive definitions *) + (*s Constants (internal representation) (Definition/Axiom) *) type lazy_constant_value = @@ -20,7 +23,7 @@ type constant_body = { const_kind : path_kind; const_body : constant_value option; const_type : typed_type; - const_hyps : var_context; (* New: younger hyp at top *) + const_hyps : named_context; (* New: younger hyp at top *) const_constraints : constraints; mutable const_opaque : bool } @@ -66,7 +69,7 @@ type one_inductive_body = { type mutual_inductive_body = { mind_kind : path_kind; mind_ntypes : int; - mind_hyps : var_context; + mind_hyps : named_context; mind_packets : one_inductive_body array; mind_constraints : constraints; mind_singl : constr option; diff --git a/kernel/environ.ml b/kernel/environ.ml index bce436ade1..45ec56816a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -25,7 +25,7 @@ type globals = { env_imports : import list } type context = { - env_var_context : var_context; + env_named_context : named_context; env_rel_context : rel_context } type env = { @@ -34,7 +34,7 @@ type env = { env_universes : universes } let empty_context = { - env_var_context = empty_var_context; + env_named_context = empty_named_context; env_rel_context = empty_rel_context } let empty_env = { @@ -48,7 +48,7 @@ let empty_env = { let universes env = env.env_universes let context env = env.env_context -let var_context env = env.env_context.env_var_context +let named_context env = env.env_context.env_named_context let rel_context env = env.env_context.env_rel_context (* Construction functions. *) @@ -58,20 +58,20 @@ let map_context f env = { env with env_context = { context with - env_var_context = map_var_context f context.env_var_context ; + env_named_context = map_named_context f context.env_named_context ; env_rel_context = map_rel_context f context.env_rel_context } } -let var_context_app f env = +let named_context_app f env = { env with env_context = { env.env_context with - env_var_context = f env.env_context.env_var_context } } + env_named_context = f env.env_context.env_named_context } } -let change_hyps = var_context_app +let change_hyps = named_context_app -let push_var d = var_context_app (add_var d) -let push_var_def def = var_context_app (add_var_def def) -let push_var_decl decl = var_context_app (add_var_decl decl) -let pop_var id = var_context_app (pop_var id) +let push_named_decl d = named_context_app (add_named_decl d) +let push_named_def def = named_context_app (add_named_def def) +let push_named_assum decl = named_context_app (add_named_assum decl) +let pop_named_decl id = named_context_app (pop_named_decl id) let rel_context_app f env = { env with @@ -80,51 +80,51 @@ let rel_context_app f env = let reset_context env = { env with - env_context = { env_var_context = empty_var_context; + env_context = { env_named_context = empty_named_context; env_rel_context = empty_rel_context} } -let fold_var_context f env a = - snd (Sign.fold_var_context - (fun d (env,e) -> (push_var d env, f env d e)) - (var_context env) (reset_context env,a)) +let fold_named_context f env a = + snd (Sign.fold_named_context + (fun d (env,e) -> (push_named_decl d env, f env d e)) + (named_context env) (reset_context env,a)) -let fold_var_context_reverse f a env = - Sign.fold_var_context_reverse f a (var_context env) +let fold_named_context_reverse f a env = + Sign.fold_named_context_reverse f a (named_context env) -let process_var_context f env = - Sign.fold_var_context - (fun d env -> f env d) (var_context env) (reset_context env) +let process_named_context f env = + Sign.fold_named_context + (fun d env -> f env d) (named_context env) (reset_context env) -let process_var_context_both_sides f env = - fold_var_context_both_sides f (var_context env) (reset_context env) +let process_named_context_both_sides f env = + fold_named_context_both_sides f (named_context env) (reset_context env) -let push_rel d = rel_context_app (add_rel d) +let push_rel d = rel_context_app (add_rel_decl d) let push_rel_def def = rel_context_app (add_rel_def def) -let push_rel_decl decl = rel_context_app (add_rel_decl decl) +let push_rel_assum decl = rel_context_app (add_rel_assum decl) let push_rels ctxt = rel_context_app (concat_rel_context ctxt) -let push_rels_to_vars env = - let sign0 = env.env_context.env_var_context in +let push_rel_context_to_named_context env = + let sign0 = env.env_context.env_named_context in let (subst,_,sign) = List.fold_right (fun (na,c,t) (subst,avoid,sign) -> let na = if na = Anonymous then Name(id_of_string"_") else na in let id = next_name_away na avoid in ((mkVar id)::subst,id::avoid, - add_var (id,option_app (substl subst) c,typed_app (substl subst) t) + add_named_decl (id,option_app (substl subst) c,typed_app (substl subst) t) sign)) - env.env_context.env_rel_context ([],ids_of_var_context sign0,sign0) - in subst, (var_context_app (fun _ -> sign) env) + env.env_context.env_rel_context ([],ids_of_named_context sign0,sign0) + in subst, (named_context_app (fun _ -> sign) env) let push_rec_types (typarray,names,_) env = let vect_lift_type = Array.mapi (fun i t -> outcast_type (lift i t)) in let nlara = List.combine (List.rev names) (Array.to_list (vect_lift_type typarray)) in - List.fold_left (fun env nvar -> push_rel_decl nvar env) env nlara + List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara let reset_rel_context env = { env with - env_context = { env_var_context = env.env_context.env_var_context; + env_context = { env_named_context = env.env_context.env_named_context; env_rel_context = empty_rel_context} } let fold_rel_context f env a = @@ -136,11 +136,11 @@ let process_rel_context f env = List.fold_right (fun d env -> f env d) (rel_context env) (reset_rel_context env) -let instantiate_vars = instantiate_sign +let instantiate_named_context = instantiate_sign let ids_of_context env = (ids_of_rel_context env.env_context.env_rel_context) - @ (ids_of_var_context env.env_context.env_var_context) + @ (ids_of_named_context env.env_context.env_named_context) let names_of_rel_context env = names_of_rel_context env.env_context.env_rel_context @@ -178,13 +178,13 @@ let new_meta ()=incr meta_ctr;!meta_ctr;; (* Access functions. *) -let lookup_var_type id env = - lookup_id_type id env.env_context.env_var_context +let lookup_named_type id env = + lookup_id_type id env.env_context.env_named_context -let lookup_var_value id env = - lookup_id_value id env.env_context.env_var_context +let lookup_named_value id env = + lookup_id_value id env.env_context.env_named_context -let lookup_var id env = lookup_id id env.env_context.env_var_context +let lookup_named id env = lookup_id id env.env_context.env_named_context let lookup_rel_type n env = Sign.lookup_rel_type n env.env_context.env_rel_context @@ -288,11 +288,11 @@ let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c) let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) -let it_mkNamedProd_or_LetIn = it_var_context_quantifier mkNamedProd_or_LetIn -let it_mkNamedLambda_or_LetIn = it_var_context_quantifier mkNamedLambda_or_LetIn +let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn +let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn let make_all_name_different env = - let avoid = ref (ids_of_var_context (var_context env)) in + let avoid = ref (ids_of_named_context (named_context env)) in process_rel_context (fun newenv (na,c,t) -> let id = next_name_away na !avoid in diff --git a/kernel/environ.mli b/kernel/environ.mli index 30d93a02e4..611987c90b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -23,50 +23,48 @@ val empty_env : env val universes : env -> universes val context : env -> context val rel_context : env -> rel_context -val var_context : env -> var_context +val named_context : env -> named_context -(* This forgets var and rel contexts *) +(* This forgets named and rel contexts *) val reset_context : env -> env -(*s This concerns only the context of local vars referred by names - [var_context] *) -val push_var : var_declaration -> env -> env -val push_var_decl : identifier * typed_type -> env -> env -val push_var_def : identifier * constr * typed_type -> env -> env -val change_hyps : (var_context -> var_context) -> env -> env -val instantiate_vars : var_context -> constr list -> (identifier * constr) list -val pop_var : identifier -> env -> env - -(*s This concerns only the context of local vars referred by indice - [rel_context] *) +(*s This concerns only local vars referred by names [named_context] *) +val push_named_decl : named_declaration -> env -> env +val push_named_assum : identifier * typed_type -> env -> env +val push_named_def : identifier * constr * typed_type -> env -> env +val change_hyps : (named_context -> named_context) -> env -> env +val instantiate_named_context : named_context -> constr list -> (identifier * constr) list +val pop_named_decl : identifier -> env -> env + +(*s This concerns only local vars referred by indice [rel_context] *) val push_rel : rel_declaration -> env -> env -val push_rel_decl : name * typed_type -> env -> env +val push_rel_assum : name * typed_type -> env -> env val push_rel_def : name * constr * typed_type -> env -> env val push_rels : rel_context -> env -> env val names_of_rel_context : env -> names_context (*s Returns also the substitution to be applied to rel's *) -val push_rels_to_vars : env -> constr list * env +val push_rel_context_to_named_context : env -> constr list * env (*s Push the types of a (co-)fixpoint *) val push_rec_types : rec_declaration -> env -> env -(* Gives identifiers in [var_context] and [rel_context] *) +(* Gives identifiers in [named_context] and [rel_context] *) val ids_of_context : env -> identifier list val map_context : (constr -> constr) -> env -> env -(*s Recurrence on [var_context] *) -val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a -val process_var_context : (env -> var_declaration -> env) -> env -> env +(*s Recurrence on [named_context] *) +val fold_named_context : (env -> named_declaration -> 'a -> 'a) -> env -> 'a -> 'a +val process_named_context : (env -> named_declaration -> env) -> env -> env -(* Recurrence on [var_context] starting from younger decl *) -val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> env -> 'a +(* Recurrence on [named_context] starting from younger decl *) +val fold_named_context_reverse : ('a -> named_declaration -> 'a) -> 'a -> env -> 'a -(* [process_var_context_both_sides f env] iters [f] on the var +(* [process_named_context_both_sides f env] iters [f] on the named declarations of [env] taking as argument both the initial segment, the middle value and the tail segment *) -val process_var_context_both_sides : - (env -> var_declaration -> var_context -> env) -> env -> env +val process_named_context_both_sides : + (env -> named_declaration -> named_context -> env) -> env -> env (*s Recurrence on [rel_context] *) val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a @@ -83,11 +81,11 @@ val new_meta : unit -> int (*s Looks up in environment *) -(* Looks up in the context of local vars referred by names ([var_context]) *) +(* Looks up in the context of local vars referred by names ([named_context]) *) (* raises [Not_found] if the identifier is not found *) -val lookup_var_type : identifier -> env -> typed_type -val lookup_var_value : identifier -> env -> constr option -val lookup_var : identifier -> env -> constr option * typed_type +val lookup_named_type : identifier -> env -> typed_type +val lookup_named_value : identifier -> env -> constr option +val lookup_named : identifier -> env -> constr option * typed_type (* Looks up in the context of local vars referred by indice ([rel_context]) *) (* raises [Not_found] if the index points out of the context *) @@ -136,8 +134,8 @@ val it_mkProd_wo_LetIn : constr -> rel_context -> constr val it_mkLambda_or_LetIn : constr -> rel_context -> constr val it_mkProd_or_LetIn : constr -> rel_context -> constr -val it_mkNamedLambda_or_LetIn : constr -> var_context -> constr -val it_mkNamedProd_or_LetIn : constr -> var_context -> constr +val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr +val it_mkNamedProd_or_LetIn : constr -> named_context -> constr (* [lambda_create env (t,c)] builds [[x:t]c] where [x] is a name built from [t]; [prod_create env (t,c)] builds [(x:t)c] where [x] is a diff --git a/kernel/evd.ml b/kernel/evd.ml index b482f94538..64602f870c 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -65,7 +65,7 @@ let is_defined sigma ev = let info = map sigma ev in not (info.evar_body = Evar_empty) -let evar_hyps ev = var_context ev.evar_env +let evar_hyps ev = named_context ev.evar_env let evar_body ev = ev.evar_body let id_of_existential ev = diff --git a/kernel/evd.mli b/kernel/evd.mli index 4315994964..e744748358 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -48,7 +48,7 @@ val is_evar : 'a evar_map -> evar -> bool val is_defined : 'a evar_map -> evar -> bool -val evar_hyps : 'a evar_info -> var_context +val evar_hyps : 'a evar_info -> named_context val evar_body : 'a evar_info -> evar_body val id_of_existential : evar -> identifier diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a5ca14f522..fdfdf0052e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -180,7 +180,7 @@ let listrec_mconstr env ntypes nparams i indlc = assert (largs = []); if not (noccur_between n ntypes b) then raise (IllFormedInd (LocalNonPos n)); - check_pos (push_rel_decl (na, outcast_type b) env) (n+1) d + check_pos (push_rel_assum (na, outcast_type b) env) (n+1) d | IsRel k -> if k >= n && k if noccur_between n ntypes b - then check_weak_pos (push_rel_decl (na,outcast_type b) env) (n+1) d + then check_weak_pos (push_rel_assum (na,outcast_type b) env) (n+1) d else raise (IllFormedInd (LocalNonPos n)) (******************) | _ -> check_pos env n x @@ -263,7 +263,7 @@ let listrec_mconstr env ntypes nparams i indlc = | IsProd (na,b,d) -> assert (largs = []); let recarg = check_pos env n b in - check_constr_rec (push_rel_decl (na,outcast_type b) env) + check_constr_rec (push_rel_assum (na,outcast_type b) env) (recarg::lrec) (n+1) d (* LetIn's must be free of occurrence of the inductive types and @@ -358,7 +358,7 @@ let cci_inductive env env_ar kind nparams finite inds cst = let packets = Array.of_list (list_map_i one_packet 1 inds) in { mind_kind = kind; mind_ntypes = ntypes; - mind_hyps = keep_hyps ids (var_context env); + mind_hyps = keep_hyps ids (named_context env); mind_packets = packets; mind_constraints = cst; mind_singl = None; diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 7888afd390..ab818d0e52 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -19,7 +19,7 @@ let is_id_inst inst = List.for_all is_id inst let instantiate_constr sign c args = - let inst = instantiate_vars sign args in + let inst = instantiate_named_context sign args in if is_id_inst inst then c else diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli index f0719d2f1e..f905ca27ee 100644 --- a/kernel/instantiate.mli +++ b/kernel/instantiate.mli @@ -12,9 +12,9 @@ open Environ (* Instantiation of constants and inductives on their real arguments. *) val instantiate_constr : - var_context -> constr -> constr list -> constr + named_context -> constr -> constr list -> constr val instantiate_type : - var_context -> typed_type -> constr list -> typed_type + named_context -> typed_type -> constr list -> typed_type (*s [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no diff --git a/kernel/reduction.ml b/kernel/reduction.ml index bfb3a565fd..3306927d6e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -277,7 +277,7 @@ let whd_state_gen flags env sigma = | Some body -> whrec (lift n body, stack) | None -> s) | IsVar id when red_delta flags -> - (match lookup_var_value id env with + (match lookup_named_value id env with | Some body -> whrec (body, stack) | None -> s) *) @@ -975,7 +975,7 @@ let splay_prod env sigma = let t = whd_betadeltaiota env sigma c in match kind_of_term t with | IsProd (n,a,c0) -> - decrec (push_rel_decl (n,outcast_type a) env) + decrec (push_rel_assum (n,outcast_type a) env) ((n,a)::m) c0 | _ -> m,t in @@ -986,8 +986,8 @@ let splay_prod_assum env sigma = let t = whd_betadeltaiota_nolet env sigma c in match kind_of_term c with | IsProd (x,t,c) -> - prodec_rec (push_rel_decl (x,outcast_type t) env) - (Sign.add_rel_decl (x,outcast_type t) l) c + prodec_rec (push_rel_assum (x,outcast_type t) env) + (Sign.add_rel_assum (x,outcast_type t) l) c | IsLetIn (x,b,t,c) -> prodec_rec (push_rel_def (x,b,outcast_type t) env) (Sign.add_rel_def (x,b,outcast_type t) l) c @@ -1009,8 +1009,8 @@ let decomp_n_prod env sigma n = match kind_of_term (whd_betadeltaiota env sigma c) with | IsProd (n,a,c0) -> let a = make_typed_lazy a (fun _ -> Type dummy_univ) in - decrec (push_rel_decl (n,a) env) - (m-1) (Sign.add_rel_decl (n,a) ln) c0 + decrec (push_rel_assum (n,a) env) + (m-1) (Sign.add_rel_assum (n,a) ln) c0 | _ -> error "decomp_n_prod: Not enough products" in decrec env n Sign.empty_rel_context @@ -1078,8 +1078,8 @@ let find_conclusion env sigma = let rec decrec env c = let t = whd_betadeltaiota env sigma c in match kind_of_term t with - | IsProd (x,t,c0) -> decrec (push_rel_decl (x,outcast_type t) env) c0 - | IsLambda (x,t,c0) -> decrec (push_rel_decl (x,outcast_type t) env) c0 + | IsProd (x,t,c0) -> decrec (push_rel_assum (x,outcast_type t) env) c0 + | IsLambda (x,t,c0) -> decrec (push_rel_assum (x,outcast_type t) env) c0 | t -> t in decrec env @@ -1135,12 +1135,12 @@ let poly_args env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with | IsProd (x,a,b) -> add_free_rels_until n a - (aux (push_rel_decl (x,outcast_type a) env) (n+1) b) + (aux (push_rel_assum (x,outcast_type a) env) (n+1) b) | _ -> Intset.empty in match kind_of_term (whd_betadeltaiota env sigma t) with | IsProd (x,a,b) -> - Intset.elements (aux (push_rel_decl (x,outcast_type a) env) 1 b) + Intset.elements (aux (push_rel_assum (x,outcast_type a) env) 1 b) | _ -> [] (* Expanding existential variables (pretyping.ml) *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 75e7cd70df..a62bc962a8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -48,7 +48,7 @@ let rec execute mf env cstr = (relative env Evd.empty n, cst0) | IsVar id -> - (make_judge cstr (lookup_var_type id env), cst0) + (make_judge cstr (lookup_named_type id env), cst0) (* ATTENTION : faudra faire le typage du contexte des Const, MutInd et MutConstructsi un jour cela devient des constructions @@ -104,7 +104,7 @@ let rec execute mf env cstr = | IsLambda (name,c1,c2) -> let (j,cst1) = execute mf env c1 in let var = assumption_of_judgment env Evd.empty j in - let env1 = push_rel_decl (name,var) env in + let env1 = push_rel_assum (name,var) env in let (j',cst2) = execute mf env1 c2 in let (j,cst3) = abs_rel env1 Evd.empty name var j' in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in @@ -113,7 +113,7 @@ let rec execute mf env cstr = | IsProd (name,c1,c2) -> let (j,cst1) = execute mf env c1 in let varj = type_judgment env Evd.empty j in - let env1 = push_rel_decl (name,assumption_of_type_judgment varj) env in + let env1 = push_rel_assum (name,assumption_of_type_judgment varj) env in let (j',cst2) = execute mf env1 c2 in let (j,cst3) = gen_rel env1 Evd.empty name varj j' in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in @@ -143,7 +143,7 @@ and execute_fix mf env lar lfi vdef = let nlara = List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in let env1 = - List.fold_left (fun env nvar -> push_rel_decl nvar env) env nlara in + List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in let (vdefj,cst2) = execute_array mf env1 vdef in let vdefv = Array.map j_val_only vdefj in let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in @@ -233,11 +233,11 @@ let empty_environment = empty_env let universes = universes let context = context -let var_context = var_context +let named_context = named_context -let lookup_var_type = lookup_var_type +let lookup_named_type = lookup_named_type let lookup_rel_type = lookup_rel_type -let lookup_var = lookup_var +let lookup_named = lookup_named let lookup_constant = lookup_constant let lookup_mind = lookup_mind let lookup_mind_specif = lookup_mind_specif @@ -245,27 +245,25 @@ let lookup_mind_specif = lookup_mind_specif (* Insertion of variables (named and de Bruijn'ed). They are now typed before being added to the environment. *) -let push_rel_or_var_def push (id,c) env = - let (j,cst) = safe_infer env c in +let push_rel_or_named_def push (id,b) env = + let (j,cst) = safe_infer env b in let env' = add_constraints cst env in push (id,j.uj_val,j.uj_type) env' -let push_var_def nvar env = push_rel_or_var_def push_var_def nvar env +let push_named_def = push_rel_or_named_def push_named_def +let push_rel_def = push_rel_or_named_def push_rel_def -let push_rel_def nrel env = push_rel_or_var_def push_rel_def nrel env - -let push_rel_or_var_decl push (id,c) env = - let (j,cst) = safe_infer_type env c in +let push_rel_or_named_assum push (id,t) env = + let (j,cst) = safe_infer env t in let env' = add_constraints cst env in - let var = assumption_of_type_judgment j in - push (id,var) env' - -let push_var_decl nvar env = push_rel_or_var_decl push_var_decl nvar env + let t = assumption_of_judgment env Evd.empty j in + push (id,t) env' -let push_rel_decl nrel env = push_rel_or_var_decl push_rel_decl nrel env +let push_named_assum = push_rel_or_named_assum push_named_assum +let push_rel_assum = push_rel_or_named_assum push_rel_assum let push_rels_with_univ vars env = - List.fold_left (fun env nvar -> push_rel_decl nvar env) env vars + List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars (* Insertion of constants and parameters in environment. *) @@ -294,7 +292,7 @@ let add_constant_with_value sp body typ env = const_kind = kind_of_path sp; const_body = Some (ref (Cooked body)); const_type = ty; - const_hyps = keep_hyps ids (var_context env); + const_hyps = keep_hyps ids (named_context env); const_constraints = Constraint.union cst cst'; const_opaque = false } in @@ -308,7 +306,7 @@ let add_lazy_constant sp f t env = const_kind = kind_of_path sp; const_body = Some (ref (Recipe f)); const_type = assumption_of_judgment env' Evd.empty jt; - const_hyps = keep_hyps ids (var_context env); + const_hyps = keep_hyps ids (named_context env); const_constraints = cst; const_opaque = false } in @@ -330,7 +328,7 @@ let add_parameter sp t env = const_kind = kind_of_path sp; const_body = None; const_type = assumption_of_judgment env' Evd.empty jt; - const_hyps = keep_hyps ids (var_context env); + const_hyps = keep_hyps ids (named_context env); const_constraints = cst; const_opaque = false } in @@ -355,7 +353,7 @@ let rec infos_and_sort env t = | IsProd (name,c1,c2) -> let (varj,_) = safe_infer_type env c1 in let var = assumption_of_type_judgment varj in - let env1 = Environ.push_rel_decl (name,var) env in + let env1 = Environ.push_rel_assum (name,var) env in let s1 = varj.utj_type in let logic = not (is_info_type env Evd.empty varj) in let small = is_small s1 in @@ -453,10 +451,10 @@ let add_mind sp mie env = let add_constraints = add_constraints -let rec pop_vars idl env = +let rec pop_named_decls idl env = match idl with | [] -> env - | id::l -> pop_vars l (Environ.pop_var id env) + | id::l -> pop_named_decls l (Environ.pop_named_decl id env) let export = export let import = import diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 577f753d37..a07be1fca6 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -24,14 +24,12 @@ val empty_environment : safe_environment val universes : safe_environment -> universes val context : safe_environment -> context -val var_context : safe_environment -> var_context +val named_context : safe_environment -> named_context -val push_var_decl : identifier * constr -> safe_environment -> safe_environment -val push_var_def : identifier * constr -> safe_environment -> safe_environment -(*i -val push_rel_decl : name * constr -> safe_environment -> safe_environment -val push_rel_def : name * constr -> safe_environment -> safe_environment -i*) +val push_named_assum : + identifier * constr -> safe_environment -> safe_environment +val push_named_def : + identifier * constr -> safe_environment -> safe_environment val add_constant : section_path -> constant_entry -> safe_environment -> safe_environment @@ -45,9 +43,9 @@ val add_mind : -> safe_environment val add_constraints : constraints -> safe_environment -> safe_environment -val pop_vars : identifier list -> safe_environment -> safe_environment +val pop_named_decls : identifier list -> safe_environment -> safe_environment -val lookup_var : identifier -> safe_environment -> constr option * typed_type +val lookup_named : identifier -> safe_environment -> constr option * typed_type (*i val lookup_rel : int -> safe_environment -> name * typed_type i*) diff --git a/kernel/sign.ml b/kernel/sign.ml index d9438eb98a..4a8078ef4b 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -14,12 +14,12 @@ let map f = List.map (fun (na,c,t) -> (na,option_app f c,typed_app f t)) let add_decl (n,t) sign = (n,None,t)::sign let add_def (n,c,t) sign = (n,Some c,t)::sign -type var_declaration = identifier * constr option * typed_type -type var_context = var_declaration list +type named_declaration = identifier * constr option * typed_type +type named_context = named_declaration list -let add_var = add -let add_var_decl = add_decl -let add_var_def = add_def +let add_named_decl = add +let add_named_assum = add_decl +let add_named_def = add_def let rec lookup_id_type id = function | (id',c,t) :: _ when id=id' -> t | _ :: sign -> lookup_id_type id sign @@ -32,26 +32,26 @@ let rec lookup_id id = function | (id',c,t) :: _ when id=id' -> (c,t) | _ :: sign -> lookup_id id sign | [] -> raise Not_found -let empty_var_context = [] -let pop_var id = function +let empty_named_context = [] +let pop_named_decl id = function | (id',_,_) :: sign -> assert (id = id'); sign | [] -> assert false -let ids_of_var_context = List.map (fun (id,_,_) -> id) -let map_var_context = map -let rec mem_var_context id = function +let ids_of_named_context = List.map (fun (id,_,_) -> id) +let map_named_context = map +let rec mem_named_context id = function | (id',_,_) :: _ when id=id' -> true - | _ :: sign -> mem_var_context id sign + | _ :: sign -> mem_named_context id sign | [] -> false -let fold_var_context = List.fold_right -let fold_var_context_reverse = List.fold_left -let fold_var_context_both_sides = list_fold_right_and_left -let it_var_context_quantifier f = List.fold_left (fun c d -> f d c) +let fold_named_context = List.fold_right +let fold_named_context_reverse = List.fold_left +let fold_named_context_both_sides = list_fold_right_and_left +let it_named_context_quantifier f = List.fold_left (fun c d -> f d c) type rel_declaration = name * constr option * typed_type type rel_context = rel_declaration list -let add_rel = add -let add_rel_decl = add_decl +let add_rel_decl = add +let add_rel_assum = add_decl let add_rel_def = add_def let lookup_rel_type n sign = let rec lookrec = function @@ -90,7 +90,7 @@ let ids_of_rel_context sign = (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) sign [] let names_of_rel_context = List.map (fun (na,_,_) -> na) -let decls_of_rel_context sign = +let assums_of_rel_context sign = List.fold_right (fun (na,c,t) l -> match c with Some _ -> l | None -> (na,body_of_type t)::l) sign [] @@ -149,7 +149,7 @@ let empty_names_context = [] let decompose_prod_assum = let rec prodec_rec l c = match kind_of_term c with - | IsProd (x,t,c) -> prodec_rec (add_rel_decl (x,outcast_type t) l) c + | IsProd (x,t,c) -> prodec_rec (add_rel_assum (x,outcast_type t) l) c | IsLetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,outcast_type t) l) c | IsCast (c,_) -> prodec_rec l c | _ -> l,c @@ -161,7 +161,7 @@ let decompose_prod_assum = let decompose_lam_assum = let rec lamdec_rec l c = match kind_of_term c with - | IsLambda (x,t,c) -> lamdec_rec (add_rel_decl (x,outcast_type t) l) c + | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,outcast_type t) l) c | IsLetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,outcast_type t) l) c | IsCast (c,_) -> lamdec_rec l c | _ -> l,c @@ -175,7 +175,7 @@ let decompose_prod_n_assum n = let rec prodec_rec l n c = if n=0 then l,c else match kind_of_term c with - | IsProd (x,t,c) -> prodec_rec (add_rel_decl(x,outcast_type t) l) (n-1) c + | IsProd (x,t,c) -> prodec_rec (add_rel_assum(x,outcast_type t) l) (n-1) c | IsLetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,outcast_type t) l) (n-1) c | IsCast (c,_) -> prodec_rec l n c @@ -190,7 +190,7 @@ let decompose_lam_n_assum n = let rec lamdec_rec l n c = if n=0 then l,c else match kind_of_term c with - | IsLambda (x,t,c) -> lamdec_rec (add_rel_decl (x,outcast_type t) l) (n-1) c + | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,outcast_type t) l) (n-1) c | IsLetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,outcast_type t) l) (n-1) c | IsCast (c,_) -> lamdec_rec l n c diff --git a/kernel/sign.mli b/kernel/sign.mli index 30e1dae28d..51e8107448 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -7,39 +7,42 @@ open Names open Term (*i*) -(*s Signatures of ordered named variables, intended to be accessed by name *) +(*s Signatures of ordered named declarations *) -type var_context = var_declaration list +type named_context = named_declaration list -val add_var : - identifier * constr option * typed_type -> var_context -> var_context -val add_var_decl : identifier * typed_type -> var_context -> var_context -val add_var_def : - identifier * constr * typed_type -> var_context -> var_context -val lookup_id : identifier -> var_context -> constr option * typed_type -val lookup_id_type : identifier -> var_context -> typed_type -val lookup_id_value : identifier -> var_context -> constr option -val pop_var : identifier -> var_context -> var_context -val empty_var_context : var_context -val ids_of_var_context : var_context -> identifier list -val map_var_context : (constr -> constr) -> var_context -> var_context -val mem_var_context : identifier -> var_context -> bool -val fold_var_context : (var_declaration -> 'a -> 'a) -> var_context -> 'a -> 'a -val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> var_context -> 'a -val fold_var_context_both_sides : - ('a -> var_declaration -> var_context -> 'a) -> var_context -> 'a -> 'a -val it_var_context_quantifier : - (var_declaration -> constr -> constr) -> constr -> var_context -> constr -val instantiate_sign : var_context -> constr list -> (identifier * constr) list -val keep_hyps : Idset.t -> var_context -> var_context +val add_named_decl : + identifier * constr option * typed_type -> named_context -> named_context +val add_named_assum : identifier * typed_type -> named_context -> named_context +val add_named_def : + identifier * constr * typed_type -> named_context -> named_context +val lookup_id : identifier -> named_context -> constr option * typed_type +val lookup_id_type : identifier -> named_context -> typed_type +val lookup_id_value : identifier -> named_context -> constr option +val pop_named_decl : identifier -> named_context -> named_context +val empty_named_context : named_context +val ids_of_named_context : named_context -> identifier list +val map_named_context : (constr -> constr) -> named_context -> named_context +val mem_named_context : identifier -> named_context -> bool +val fold_named_context : + (named_declaration -> 'a -> 'a) -> named_context -> 'a -> 'a +val fold_named_context_reverse : + ('a -> named_declaration -> 'a) -> 'a -> named_context -> 'a +val fold_named_context_both_sides : + ('a -> named_declaration -> named_context -> 'a) -> named_context -> 'a -> 'a +val it_named_context_quantifier : + (named_declaration -> constr -> constr) -> constr -> named_context -> constr +val instantiate_sign : + named_context -> constr list -> (identifier * constr) list +val keep_hyps : Idset.t -> named_context -> named_context (*s Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) type rel_context = rel_declaration list -val add_rel : (name * constr option * typed_type) -> rel_context -> rel_context -val add_rel_decl : (name * typed_type) -> rel_context -> rel_context +val add_rel_decl : (name * constr option * typed_type) -> rel_context -> rel_context +val add_rel_assum : (name * typed_type) -> rel_context -> rel_context val add_rel_def : (name * constr * typed_type) -> rel_context -> rel_context val lookup_rel_type : int -> rel_context -> name * typed_type val lookup_rel_value : int -> rel_context -> constr option @@ -49,7 +52,7 @@ val rel_context_length : rel_context -> int val lift_rel_context : int -> rel_context -> rel_context val concat_rel_context : newer:rel_context -> older:rel_context -> rel_context val ids_of_rel_context : rel_context -> identifier list -val decls_of_rel_context : rel_context -> (name * constr) list +val assums_of_rel_context : rel_context -> (name * constr) list val map_rel_context : (constr -> constr) -> rel_context -> rel_context (*s This is used to translate names into de Bruijn indices and diff --git a/kernel/term.ml b/kernel/term.ml index b70bb05a07..81fbd9a02e 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -784,7 +784,7 @@ let outcast_type x = x let typed_combine f g t u = f t u (**) -type var_declaration = identifier * constr option * typed_type +type named_declaration = identifier * constr option * typed_type type rel_declaration = name * constr option * typed_type diff --git a/kernel/term.mli b/kernel/term.mli index f2a49e838f..40bc12ce3d 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -35,29 +35,6 @@ type case_printing = (* the integer is the number of real args, needed for reduction *) type case_info = int array * case_printing -(* -type 'a oper = - | Meta of int - | Sort of 'a - | Cast | Prod | Lambda - | AppL | Const of section_path - | Evar of existential_key - | MutInd of inductive_path - | MutConstruct of constructor_path - | MutCase of case_info - | Fix of int array * int - | CoFix of int - | XTRA of string -*) - -(*s The type [constr] of the terms of CCI - is obtained by instanciating a generic notion of terms - on the above operators, themselves instanciated - on the above sorts. *) - -(* [VAR] is used for named variables and [Rel] for variables as - de Bruijn indices. *) - type constr type typed_type @@ -78,12 +55,20 @@ val incast_type : typed_type -> constr val outcast_type : constr -> typed_type -type var_declaration = identifier * constr option * typed_type +(*s A {\em declaration} has the form (name,body,type). It is either an + {\em assumption} if [body=None] or a {\em definition} if + [body=Some actualbody]. It is referred by {\em name} if [na] is an + identifier or by {\em relative index} if [na] is not an identifier + (in the latter case, [na] is of type [name] but just for printing + purpose *) + +type named_declaration = identifier * constr option * typed_type type rel_declaration = name * constr option * typed_type type arity = rel_declaration list * sorts -(**********************************************************************) +(*i********************************************************************i*) +(*s type of global reference *) type global_reference = | ConstRef of section_path | IndRef of inductive_path @@ -96,7 +81,7 @@ type global_reference = (* Concrete type for making pattern-matching. *) -(* [constr array] is an instance matching definitional [var_context] in +(* [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) type existential = int * constr array type constant = section_path * constr array @@ -106,6 +91,8 @@ type rec_declaration = constr array * name list * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration +(* [IsVar] is used for named variables and [IsRel] for variables as + de Bruijn indices. *) type kind_of_term = | IsRel of int @@ -178,15 +165,15 @@ val mkNamedLetIn : identifier -> constr -> constr -> constr -> constr (* Constructs either [(x:t)c] or [[x=b:t]c] *) val mkProd_or_LetIn : rel_declaration -> constr -> constr -val mkNamedProd_or_LetIn : var_declaration -> constr -> constr +val mkNamedProd_or_LetIn : named_declaration -> constr -> constr (* Constructs either [[x:t]c] or [[x=b:t]c] *) val mkLambda_or_LetIn : rel_declaration -> constr -> constr -val mkNamedLambda_or_LetIn : var_declaration -> constr -> constr +val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *) val mkProd_wo_LetIn : rel_declaration -> constr -> constr -val mkNamedProd_wo_LetIn : var_declaration -> constr -> constr +val mkNamedProd_wo_LetIn : named_declaration -> constr -> constr (* non-dependant product $t_1 \rightarrow t_2$ *) val mkArrow : constr -> constr -> constr @@ -474,8 +461,8 @@ val substnl : constr list -> int -> constr -> constr val substl : constr list -> constr -> constr val subst1 : constr -> constr -> constr -val substl_decl : constr list -> var_declaration -> var_declaration -val subst1_decl : constr -> var_declaration -> var_declaration +val substl_decl : constr list -> named_declaration -> named_declaration +val subst1_decl : constr -> named_declaration -> named_declaration (* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *) val global_vars : constr -> identifier list @@ -525,7 +512,7 @@ val occur_evar : existential_key -> constr -> bool in c, [false] otherwise *) val occur_var : identifier -> constr -> bool -val occur_var_in_decl : identifier -> var_declaration -> bool +val occur_var_in_decl : identifier -> named_declaration -> bool (* [dependent M N] is true iff M is eq\_constr with a subterm of N M is appropriately lifted through abstractions of N *) @@ -542,7 +529,7 @@ val eta_eq_constr : constr -> constr -> bool val subst_term : what:constr -> where:constr -> constr val subst_term_occ : occs:int list -> what:constr -> where:constr -> constr val subst_term_occ_decl : occs:int list -> what:constr -> - where:var_declaration -> var_declaration + where:named_declaration -> named_declaration (* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c] for each binding $(i,c_i)$ in [bl], diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 31a31a9d90..927b33e8c4 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -52,11 +52,11 @@ let relative env sigma n = (* Checks if a context of variable is included in another one. *) (* let rec hyps_inclusion env sigma sign1 sign2 = - if sign1 = empty_var_context then true + if sign1 = empty_named_context then true else let (id1,ty1) = hd_sign sign1 in let rec search sign2 = - if sign2 = empty_var_context then false + if sign2 = empty_named_context then false else let (id2,ty2) = hd_sign sign2 in if id1 = id2 then @@ -73,7 +73,7 @@ let rec hyps_inclusion env sigma sign1 sign2 = current context of [env]. *) (* let check_hyps id env sigma hyps = - let hyps' = var_context env in + let hyps' = named_context env in if not (hyps_inclusion env sigma hyps hyps') then error_reference_variables CCI env id *) @@ -368,13 +368,13 @@ let check_term env mind_recvec f = match lrec, kind_of_term (strip_outer_cast c) with | (Param(_)::lr, IsLambda (x,a,b)) -> let l' = map_lift_fst l in - crec (push_rel_decl (x,outcast_type a) env) (n+1) l' (lr,b) + crec (push_rel_assum (x,outcast_type a) env) (n+1) l' (lr,b) | (Norec::lr, IsLambda (x,a,b)) -> let l' = map_lift_fst l in - crec (push_rel_decl (x,outcast_type a) env) (n+1) l' (lr,b) + crec (push_rel_assum (x,outcast_type a) env) (n+1) l' (lr,b) | (Mrec(i)::lr, IsLambda (x,a,b)) -> let l' = map_lift_fst l in - crec (push_rel_decl (x,outcast_type a) env) (n+1) + crec (push_rel_assum (x,outcast_type a) env) (n+1) ((1,mind_recvec.(i))::l') (lr,b) | (Imbr((sp,i) as ind_sp,lrc)::lr, IsLambda (x,a,b)) -> let l' = map_lift_fst l in @@ -383,7 +383,7 @@ let check_term env mind_recvec f = let lc = Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i) in - crec (push_rel_decl (x,outcast_type a) env) (n+1) ((1,lc)::l') (lr,b) + crec (push_rel_assum (x,outcast_type a) env) (n+1) ((1,lc)::l') (lr,b) | _,_ -> f env n l (strip_outer_cast c) in crec env @@ -444,7 +444,7 @@ let is_subterm_specif env sigma lcx mind_recvec = | IsLambda (x,a,b) when l=[] -> let lst' = map_lift_fst lst in - crec (push_rel_decl (x,outcast_type a) env) (n+1) lst' b + crec (push_rel_assum (x,outcast_type a) env) (n+1) lst' b (*** Experimental change *************************) | IsMeta _ -> [||] @@ -473,7 +473,7 @@ let rec check_subterm_rec_meta env sigma vectn k def = match kind_of_term (strip_outer_cast def) with | IsLambda (x,a,b) -> if noccur_with_meta n nfi a then - let env' = push_rel_decl (x,outcast_type a) env in + let env' = push_rel_assum (x,outcast_type a) env in if n = k+1 then (env',a,b) else check_occur env' (n+1) b else @@ -581,13 +581,13 @@ let rec check_subterm_rec_meta env sigma vectn k def = | IsLambda (x,a,b) -> (check_rec_call env n lst a) && - (check_rec_call (push_rel_decl (x,outcast_type a) env) + (check_rec_call (push_rel_assum (x,outcast_type a) env) (n+1) (map_lift_fst lst) b) && (List.for_all (check_rec_call env n lst) l) | IsProd (x,a,b) -> (check_rec_call env n lst a) && - (check_rec_call (push_rel_decl (x,outcast_type a) env) + (check_rec_call (push_rel_assum (x,outcast_type a) env) (n+1) (map_lift_fst lst) b) && (List.for_all (check_rec_call env n lst) l) @@ -643,7 +643,7 @@ let rec check_subterm_rec_meta env sigma vectn k def = | IsLambda (x,a,b) -> (check_rec_call env n lst a) & (check_rec_call_fix_body - (push_rel_decl (x,outcast_type a) env) (n+1) + (push_rel_assum (x,outcast_type a) env) (n+1) (map_lift_fst lst) (decr-1) recArgsDecrArg b) | _ -> anomaly "Not enough abstractions in fix body" @@ -683,7 +683,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = let b = whd_betadeltaiota env sigma (strip_outer_cast c) in match kind_of_term b with | IsProd (x,a,b) -> - codomain_is_coind (push_rel_decl (x,outcast_type a) env) b + codomain_is_coind (push_rel_assum (x,outcast_type a) env) b | _ -> try find_coinductive env sigma b @@ -756,7 +756,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = | IsLambda (x,a,b) -> assert (args = []); if (noccur_with_meta n nbfix a) then - check_rec_call (push_rel_decl (x,outcast_type a) env) + check_rec_call (push_rel_assum (x,outcast_type a) env) alreadygrd (n+1) vlra b else raise (CoFixGuardError (RecCallInTypeOfAbstraction t)) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index a2fedf7f16..9c4d62b95c 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -51,7 +51,7 @@ val judge_of_prop_contents : contents -> unsafe_judgment val judge_of_type : universe -> unsafe_judgment * constraints -val generalize_without_universes : var_declaration -> typed_type -> typed_type +val generalize_without_universes : named_declaration -> typed_type -> typed_type val abs_rel : env -> 'a evar_map -> name -> typed_type -> unsafe_judgment @@ -85,6 +85,6 @@ val find_case_dep_nparams : env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool (*i -val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool +val hyps_inclusion : env -> 'a evar_map -> named_context -> named_context -> bool i*) -- cgit v1.2.3