diff options
| author | herbelin | 2000-10-18 14:37:44 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-18 14:37:44 +0000 |
| commit | bedaec8452d0600ede52efeeac016c9d323c66de (patch) | |
| tree | 7f056ffcd58f58167a0e813d5a8449eb950a8e23 | |
| parent | 9983a5754258f74293b77046986b698037902e2b (diff) | |
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
67 files changed, 415 insertions, 428 deletions
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<n+ntypes then begin check_correct_par env nparams ntypes n (k-n+1) largs; @@ -246,7 +246,7 @@ let listrec_mconstr env ntypes nparams i indlc = (* The extra case *) | IsLambda (na,b,d) -> 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*) diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 5e6137db01..bdf48ddbb5 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -253,7 +253,7 @@ let error_fixname_unbound str is_cofix loc name = 'sTR ((if is_cofix then "co" else "")^"fixpoint definition") >]) (* let rec collapse_env n env = if n=0 then env else - add_rel (Anonymous,()) (collapse_env (n-1) (snd (uncons_rel_env env))) + add_rel_decl (Anonymous,()) (collapse_env (n-1) (snd (uncons_rel_env env))) *) let check_capture s ty = function @@ -459,8 +459,8 @@ let ast_adjust_consts sigma = dbrec let globalize_constr ast = - let sign = Global.var_context () in - ast_adjust_consts Evd.empty (from_list (ids_of_var_context sign)) ast + let sign = Global.named_context () in + ast_adjust_consts Evd.empty (from_list (ids_of_named_context sign)) ast (* Globalizes ast expressing constructions in tactics or vernac *) (* Actually, it is incomplete, see vernacinterp.ml and tacinterp.ml *) @@ -479,8 +479,8 @@ let rec glob_ast sigma env = | x -> x let globalize_ast ast = - let sign = Global.var_context () in - glob_ast Evd.empty (from_list (ids_of_var_context sign)) ast + let sign = Global.named_context () in + glob_ast Evd.empty (from_list (ids_of_named_context sign)) ast (**************************************************************************) (* Functions to translate ast into rawconstr *) @@ -489,7 +489,7 @@ let globalize_ast ast = let interp_rawconstr_gen sigma env allow_soapp lvar com = ast_to_rawconstr sigma (from_list (ids_of_rel_context (rel_context env))) - allow_soapp (lvar,var_context env) com + allow_soapp (lvar,named_context env) com let interp_rawconstr sigma env com = interp_rawconstr_gen sigma env false [] com @@ -500,7 +500,7 @@ let interp_rawconstr sigma env com = let interp_rawconstr_wo_glob sigma env lvar com = ast_to_rawconstr sigma (from_list (ids_of_rel_context (rel_context env))) - false (lvar,var_context env) com + false (lvar,named_context env) com (*let raw_fconstr_of_com sigma env com = ast_to_fw sigma (unitize_env (context env)) [] com @@ -619,7 +619,7 @@ let interp_constrpattern_gen sigma env lvar com = ast_to_rawconstr sigma (from_list (ids_of_rel_context (rel_context env))) true (List.map (fun x -> - string_of_id (fst x)) lvar,var_context env) com + string_of_id (fst x)) lvar,named_context env) com and nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in try pattern_of_rawconstr nlvar c diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 1e81bf2844..43f28fbe6b 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -115,8 +115,8 @@ let implicit_args_msg sp mipv = >]) mipv >] -let instance_of_var_context sign = - Array.of_list (List.map mkVar (ids_of_var_context sign)) +let instance_of_named_context sign = + Array.of_list (List.map mkVar (ids_of_named_context sign)) let print_mutual sp mib = let pk = kind_of_path sp in @@ -147,7 +147,7 @@ let print_mutual sp mib = else [< 'sTR "["; pr_rel_context env lpars; 'sTR "]"; 'bRK(1,2) >] in let print_oneind tyi = - let mis = build_mis ((sp,tyi),instance_of_var_context mib.mind_hyps) mib in + let mis = build_mis ((sp,tyi),instance_of_named_context mib.mind_hyps) mib in let (_,arity) = decomp_n_prod env evd nparams (body_of_type (mis_user_arity mis)) in (hOV 0 @@ -156,7 +156,7 @@ let print_mutual sp mib = 'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]); 'bRK(1,2); print_constructors mis >]) in - let mis0 = build_mis ((sp,0),instance_of_var_context mib.mind_hyps) mib in + let mis0 = build_mis ((sp,0),instance_of_named_context mib.mind_hyps) mib in (* Case one [co]inductive *) if Array.length mipv = 1 then let (_,arity) = decomp_n_prod env evd nparams @@ -431,7 +431,7 @@ let print_name name = | ConstructRef ((sp,_),_) -> print_inductive sp with Not_found -> try - let (c,typ) = Global.lookup_var name in + let (c,typ) = Global.lookup_named name in [< print_var (name,c,typ); try print_impl_args (implicits_of_var name) with _ -> [<>] >] @@ -440,7 +440,7 @@ let print_name name = let print_opaque_name name = let sigma = Evd.empty in let env = Global.env () in - let sign = Global.var_context () in + let sign = Global.named_context () in try let x = global_reference CCI name in match kind_of_term x with @@ -457,7 +457,7 @@ let print_opaque_name name = let ty = Typeops.type_of_constructor env sigma cstr in print_typed_value (x, ty) | IsVar id -> - let (c,ty) = lookup_var id env in + let (c,ty) = lookup_named id env in print_var (id,c,ty) | _ -> failwith "print_name" with Not_found -> diff --git a/parsing/printer.ml b/parsing/printer.ml index e8eccf6834..04578675ac 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -186,8 +186,8 @@ let pr_rel_decl env (na,c,typ) = * It's printed out from outermost to innermost, so it's readable. *) (* Prints a signature, all declarations on the same line if possible *) -let pr_var_context_of env = - hV 0 [< (fold_var_context +let pr_named_context_of env = + hV 0 [< (fold_named_context (fun env d pps -> [< pps; 'wS 2; pr_var_decl env d >]) env) [< >] >] @@ -205,7 +205,7 @@ let pr_rel_context env rel_context = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env = let sign_env = - fold_var_context + fold_named_context (fun env d pps -> let pidt = pr_var_decl env d in [< pps; 'fNL; pidt >]) env [< >] @@ -223,14 +223,14 @@ let pr_ne_context_of header k env = else let penv = pr_context_unlimited env in [< header; penv >] let pr_context_limit n env = - let var_context = Environ.var_context env in - let lgsign = List.length var_context in + let named_context = Environ.named_context env in + let lgsign = List.length named_context in if n >= lgsign then pr_context_unlimited env else let k = lgsign-n in let _,sign_env = - fold_var_context + fold_named_context (fun env d (i,pps) -> if i < k then (i+1, [< pps ;'sTR "." >]) diff --git a/parsing/printer.mli b/parsing/printer.mli index 67434ee317..3e5b589b4a 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -36,10 +36,10 @@ val pr_pattern_env : names_context -> constr_pattern -> std_ppcmds val pr_ne_context_of : std_ppcmds -> path_kind -> env -> std_ppcmds -val pr_var_decl : env -> var_declaration -> std_ppcmds +val pr_var_decl : env -> named_declaration -> std_ppcmds val pr_rel_decl : env -> rel_declaration -> std_ppcmds -val pr_var_context_of : env -> std_ppcmds +val pr_named_context_of : env -> std_ppcmds val pr_rel_context : env -> rel_context -> std_ppcmds val pr_context_of : env -> std_ppcmds diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 9d536b644a..176a3c3e9e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -136,7 +136,7 @@ let inductive_of_rawconstructor c = (* Environment management *) let push_rel_type sigma (na,t) env = - push_rel_decl (na,get_assumption_of env sigma t) env + push_rel_assum (na,get_assumption_of env sigma t) env let push_rels vars env = List.fold_right (fun nvar env -> push_rel_type Evd.empty nvar env) vars env @@ -750,7 +750,7 @@ let shift_problem pb = (* Building the sub-pattern-matching problem for a given branch *) let build_branch pb defaults eqns const_info = - let cs_args = decls_of_rel_context const_info.cs_args in + let cs_args = assums_of_rel_context const_info.cs_args in let names = get_names pb.env cs_args eqns in let newpats = if !substitute_alias then @@ -764,7 +764,7 @@ let build_branch pb defaults eqns const_info = let _,typs' = List.fold_right (fun (na,t) (env,typs) -> - (push_rel_decl (na,outcast_type t) env, + (push_rel_assum (na,outcast_type t) env, ((na,to_mutind env !(pb.isevars) t),t)::typs)) typs (pb.env,[]) in let tomatchs = @@ -882,7 +882,7 @@ let matx_of_eqns env tomatchl eqns = let initial_lpat,initial_rhs = prepare_initial_alias lpat tomatchl rhs in let rhs = { rhs_env = env; - other_ids = ids@(ids_of_var_context (var_context env)); + other_ids = ids@(ids_of_named_context (named_context env)); private_ids = []; user_ids = ids; subst = []; @@ -924,7 +924,7 @@ let inh_coerce_to_ind isevars env ty tyi = List.fold_right (fun (na,ty) (env,evl) -> let aty = get_assumption_of env Evd.empty ty in - (push_rel_decl (na,aty) env, + (push_rel_assum (na,aty) env, (new_isevar isevars env (incast_type aty) CCI)::evl)) ntys (env,[]) in let expected_typ = applist (mkMutInd tyi,evarl) in diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 839cfac4f1..9040ce3eb3 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -131,7 +131,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj = (* let jv1 = exemeta_rec def_vty_con env isevars v1 in let assv1 = assumption_of_judgement env !isevars jv1 in *) let assv1 = outcast_type v1 in - let env1 = push_rel_decl (x,assv1) env in + let env1 = push_rel_assum (x,assv1) env in let h2 = inh_conv_coerce_to_fail env isevars u2 {uj_val = v2; uj_type = get_assumption_of env1 !isevars t2 } in @@ -141,7 +141,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj = let name = (match name with | Anonymous -> Name (id_of_string "x") | _ -> name) in - let env1 = push_rel_decl (name,assu1) env in + let env1 = push_rel_assum (name,assu1) env in let h1 = inh_conv_coerce_to_fail env isevars t1 {uj_val = mkRel 1; diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a49bcb098f..70eba2949e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -253,7 +253,7 @@ let lookup_name_as_renamed ctxt t s = | (None,avoid') -> lookup avoid' env_names (n+1) (pop c')) | IsCast (c,_) -> lookup avoid env_names n c | _ -> None - in lookup (ids_of_var_context ctxt) empty_names_context 1 t + in lookup (ids_of_named_context ctxt) empty_names_context 1 t let lookup_index_as_renamed t n = let rec lookup n d c = match kind_of_term c with diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 8c8dd417d1..5f3108d483 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -15,7 +15,7 @@ open Rawterm val detype : identifier list -> names_context -> constr -> rawconstr (* look for the index of a named var or a nondep var as it is renamed *) -val lookup_name_as_renamed : var_context -> constr -> identifier -> int option +val lookup_name_as_renamed : named_context -> constr -> identifier -> int option val lookup_index_as_renamed : constr -> int -> int option diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b877624ada..f4e9d01b7a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -264,7 +264,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = evar_conv_x env isevars CONV c1 c2 & (let d = Retyping.get_assumption_of env !isevars (nf_ise1 !isevars c1) - in evar_conv_x (push_rel_decl (n,d) env) isevars pbty c'1 c'2) + in evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2) | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) -> sp1=sp2 diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b7061962bf..8aac75e39f 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -45,8 +45,8 @@ let filter_sign p sign x = (* All ids of sign must be distincts! *) let new_isevar_sign env sigma typ instance = - let sign = var_context env in - if not (list_distinct (ids_of_var_context sign)) then + let sign = named_context env in + if not (list_distinct (ids_of_named_context sign)) then error "new_isevar_sign: two vars have the same name"; let newev = Evd.new_evar() in let info = { evar_concl = typ; evar_env = env; @@ -58,7 +58,7 @@ let new_isevar_sign env sigma typ instance = let dummy_sort = mkType dummy_univ let make_instance env = - fold_var_context + fold_named_context (fun env (id, b, _) l -> if b=None then mkVar id :: l else l) env [] @@ -74,9 +74,9 @@ let split_evar_to_arrow sigma c = let evd = Evd.map sigma ev in let evenv = evd.evar_env in let (sigma1,dom) = new_type_var evenv sigma in - let hyps = var_context evenv in - let nvar = next_ident_away (id_of_string "x") (ids_of_var_context hyps) in - let newenv = push_var_decl (nvar,make_typed dom (Type dummy_univ)) evenv in + let hyps = named_context evenv in + let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in + let newenv = push_named_assum (nvar,make_typed dom (Type dummy_univ)) evenv in let (sigma2,rng) = new_type_var newenv sigma1 in let prod = mkProd (named_hd newenv dom Anonymous, dom, subst_var nvar rng) in let sigma3 = Evd.define sigma2 ev prod in @@ -100,7 +100,7 @@ let do_restrict_hyps sigma c = let args = Array.to_list args in let evd = Evd.map sigma ev in let env = evd.evar_env in - let hyps = var_context env in + let hyps = named_context env in let (_,(rsign,ncargs)) = List.fold_left (fun (sign,(rs,na)) a -> @@ -108,7 +108,7 @@ let do_restrict_hyps sigma c = if not(closed0 a) then (rs,na) else - (add_var (List.hd sign) rs, a::na))) + (add_named_decl (List.hd sign) rs, a::na))) (hyps,([],[])) args in let sign' = List.rev rsign in @@ -146,7 +146,7 @@ let ise_try isevars l = (* say if the section path sp corresponds to an existential *) let ise_in_dom isevars sp = Evd.in_dom !isevars sp -(* map the given section path to the evar_declaration *) +(* map the given section path to the enamed_declaration *) let ise_map isevars sp = Evd.map !isevars sp (* define the existential of section path sp as the constr body *) @@ -198,7 +198,7 @@ let real_clean isevars sp args rhs = let make_instance_with_rel env = let n = rel_context_length (rel_context env) in let vars = - fold_var_context + fold_named_context (fun env (id,b,_) l -> if b=None then mkVar id :: l else l) env [] in snd (fold_rel_context @@ -206,7 +206,7 @@ let make_instance_with_rel env = env (n+1,vars)) let make_subst env args = - snd (fold_var_context + snd (fold_named_context (fun env (id,b,c) (args,l as g) -> match b, args with | None, a::rest -> (rest, (id,a)::l) @@ -218,7 +218,7 @@ let make_subst env args = (* Converting the env into the sign of the evar to define *) let new_isevar isevars env typ k = - let subst,env' = push_rels_to_vars env in + let subst,env' = push_rel_context_to_named_context env in let typ' = substl subst typ in let instance = make_instance_with_rel env in let (sigma',evar) = new_isevar_sign env' !isevars typ' instance in @@ -270,19 +270,19 @@ let solve_refl conv_algo isevars c1 c2 = and (_,argsv2) = destEvar c2 in let evd = Evd.map !isevars ev in let env = evd.evar_env in - let hyps = var_context env in + let hyps = named_context env in let (_,rsign) = array_fold_left2 (fun (sgn,rsgn) a1 a2 -> if conv_algo a1 a2 then - (List.tl sgn, add_var (List.hd sgn) rsgn) + (List.tl sgn, add_named_decl (List.hd sgn) rsgn) else (List.tl sgn, rsgn)) (hyps,[]) argsv1 argsv2 in let nsign = List.rev rsign in let nenv = change_hyps (fun _ -> nsign) env in - let nargs = (Array.of_list (List.map mkVar (ids_of_var_context nsign))) in + let nargs = (Array.of_list (List.map mkVar (ids_of_named_context nsign))) in let newev = Evd.new_evar () in let info = { evar_concl = evd.evar_concl; evar_env = nenv; evar_body = Evar_empty; evar_info = None } in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a7ac436b60..9caab6bcce 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -159,7 +159,7 @@ let pretype_id loc env lvar id = { uj_val = mkRel n; uj_type = typed_app (lift n) typ } with Not_found -> try - let typ = lookup_id_type id (var_context env) in + let typ = lookup_id_type id (named_context env) in { uj_val = mkVar id; uj_type = typ } with Not_found -> error_var_not_found_loc loc CCI id @@ -240,7 +240,7 @@ match cstr with (* Oů teste-t-on que le résultat doit satisfaire tycon ? *) let nbfix = Array.length lfi in let lfi = List.map (fun id -> Name id) (Array.to_list lfi) in let newenv = - array_fold_left2 (fun env id ar -> (push_rel_decl (id,ar) env)) + array_fold_left2 (fun env id ar -> (push_rel_assum (id,ar) env)) env (Array.of_list (List.rev lfi)) (vect_lift_type lara) in let vdefj = Array.mapi @@ -280,7 +280,7 @@ match cstr with (* Oů teste-t-on que le résultat doit satisfaire tycon ? *) let j = pretype_type dom_valcon env isevars lvar lmeta c1 in let assum = assumption_of_type_judgment (inh_ass_of_j env isevars j) in let var = (name,assum) in - let j' = pretype rng (push_rel_decl var env) isevars lvar lmeta c2 + let j' = pretype rng (push_rel_assum var env) isevars lvar lmeta c2 in fst (abs_rel env !isevars name assum j') @@ -288,7 +288,7 @@ match cstr with (* Oů teste-t-on que le résultat doit satisfaire tycon ? *) let j = pretype empty_tycon env isevars lvar lmeta c1 in let assum = inh_ass_of_j env isevars j in let var = (name,assumption_of_type_judgment assum) in - let j' = pretype empty_tycon (push_rel_decl var env) isevars lvar lmeta c2 in + let j' = pretype empty_tycon (push_rel_assum var env) isevars lvar lmeta c2 in (try fst (gen_rel env !isevars name assum j') with TypeError _ as e -> Stdpp.raise_with_loc loc e) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 1e7da45794..4f36fbbdd0 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -45,7 +45,7 @@ let rec type_of env cstr= with Not_found -> anomaly "type_of: this is not a well-typed term") | IsRel n -> lift n (body_of_type (snd (lookup_rel_type n env))) | IsVar id -> - (try body_of_type (snd (lookup_var id env)) + (try body_of_type (snd (lookup_named id env)) with Not_found -> anomaly ("type_of: variable "^(string_of_id id)^" unbound")) | IsConst c -> body_of_type (type_of_constant env sigma c) @@ -64,7 +64,7 @@ let rec type_of env cstr= whd_betadeltaiota env sigma (applist (p,al)) | IsLambda (name,c1,c2) -> let var = make_typed c1 (sort_of env c1) in - mkProd (name, c1, type_of (push_rel_decl (name,var) env) c2) + mkProd (name, c1, type_of (push_rel_assum (name,var) env) c2) | IsLetIn (name,b,c1,c2) -> let var = make_typed c1 (sort_of env c1) in subst1 b (type_of (push_rel_def (name,b,var) env) c2) @@ -84,7 +84,7 @@ and sort_of env t = | IsSort (Type u) -> Type Univ.dummy_univ | IsProd (name,t,c2) -> let var = make_typed t (sort_of env t) in - (match (sort_of (push_rel_decl (name,var) env) c2) with + (match (sort_of (push_rel_assum (name,var) env) c2) with | Prop _ as s -> s | Type u2 -> Type Univ.dummy_univ) | IsApp(f,args) -> sort_of_atomic_type env sigma (type_of env f) args diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 8b9319a29c..ebab35c2cd 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -36,7 +36,7 @@ let rec execute mf env sigma cstr = | IsVar id -> (try - make_judge cstr (snd (lookup_var id env)) + make_judge cstr (snd (lookup_named id env)) with Not_found -> error ("execute: variable " ^ (string_of_id id) ^ " not defined")) @@ -86,7 +86,7 @@ let rec execute mf env sigma cstr = | IsLambda (name,c1,c2) -> let j = execute mf env sigma c1 in let var = assumption_of_judgment env sigma j in - let env1 = push_rel_decl (name,var) env in + let env1 = push_rel_assum (name,var) env in let j' = execute mf env1 sigma c2 in let (j,_) = abs_rel env1 sigma name var j' in j @@ -95,7 +95,7 @@ let rec execute mf env sigma cstr = let j = execute mf env sigma c1 in let varj = type_judgment env sigma j in let var = assumption_of_type_judgment varj in - let env1 = push_rel_decl (name,var) env in + let env1 = push_rel_assum (name,var) env in let j' = execute mf env1 sigma c2 in let (j,_) = gen_rel env1 sigma name varj j' in j @@ -121,7 +121,7 @@ and execute_fix mf env sigma 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 = execute_array mf env1 sigma vdef in let vdefv = Array.map j_val_only vdefj in let cst3 = type_fixpoint env1 sigma lfi lara vdefj in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 3e55d555a6..5ef2d60357 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -33,7 +33,7 @@ type 'a clausenv = { type wc = walking_constraints let new_evar_in_sign env = - let ids = ids_of_var_context (Environ.var_context env) in + let ids = ids_of_named_context (Environ.named_context env) in let ev = new_evar () in mkEvar (ev, Array.of_list (List.map mkVar ids)) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 3e2d96a957..efeda72f38 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -100,7 +100,7 @@ let w_add_sign (id,t) (wc : walking_constraints) = ids_mk (ts_mod (fun evr -> { focus = evr.focus; - env = push_var_decl (id,t) evr.env; + env = push_named_assum (id,t) evr.env; decls = evr.decls }) (ids_it wc)) @@ -116,7 +116,7 @@ let w_Focus sp wc = ids_mod (extract_decl sp) wc let w_Underlying wc = (ts_it (ids_it wc)).decls let w_type_of wc c = ctxt_type_of (ids_it wc) c let w_env wc = get_env (ids_it wc) -let w_hyps wc = var_context (get_env (ids_it wc)) +let w_hyps wc = named_context (get_env (ids_it wc)) let w_ORELSE wt1 wt2 wc = try wt1 wc with e when catchable_exception e -> wt2 wc diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 70416a363a..b1c4a5a2c8 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -37,9 +37,9 @@ val w_Declare : evar -> constr * constr -> w_tactic val w_Declare_At : evar -> evar -> constr * constr -> w_tactic val w_Define : evar -> constr -> w_tactic -val w_Underlying : walking_constraints -> evar_declarations +val w_Underlying : walking_constraints -> enamed_declarations val w_env : walking_constraints -> env -val w_hyps : walking_constraints -> var_context +val w_hyps : walking_constraints -> named_context val w_type_of : walking_constraints -> constr -> constr val w_add_sign : (identifier * typed_type) -> walking_constraints -> walking_constraints diff --git a/proofs/logic.ml b/proofs/logic.ml index 0e5b970c90..61126b262f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -223,9 +223,9 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = let apply_to_hyp env id f = let found = ref false in let env' = - process_var_context_both_sides + process_named_context_both_sides (fun env (idc,c,ct as d) tail -> - if idc = id then (found:=true; f env d tail) else push_var d env) + if idc = id then (found:=true; f env d tail) else push_named_decl d env) env in if (not !check) || !found then env' else error "No such assumption" @@ -237,7 +237,7 @@ let global_vars_set_of_var = function let check_backward_dependencies env d = if not (Idset.for_all - (fun id -> mem_var_context id (var_context env)) + (fun id -> mem_named_context id (named_context env)) (global_vars_set_of_var d)) then error "Can't introduce at that location: free variable conflict" @@ -255,7 +255,7 @@ let convert_hyp env sigma id ty = (fun env (idc,c,ct) _ -> if !check && not (is_conv env sigma ty (body_of_type ct)) then error "convert-hyp rule passed non-converting term"; - push_var (idc,c,get_assumption_of env sigma ty) env) + push_named_decl (idc,c,get_assumption_of env sigma ty) env) let replace_hyp env id d = apply_to_hyp env id @@ -263,13 +263,13 @@ let replace_hyp env id d = if !check then (check_backward_dependencies env d; check_forward_dependencies id tail); - push_var d env) + push_named_decl d env) let insert_after_hyp env id d = apply_to_hyp env id (fun env d' _ -> if !check then check_backward_dependencies env d; - push_var d (push_var d' env)) + push_named_decl d (push_named_decl d' env)) let remove_hyp env id = apply_to_hyp env id @@ -281,33 +281,33 @@ let remove_hyp env id = let prim_refiner r sigma goal = let env = goal.evar_env in - let sign = var_context env in + let sign = named_context env in let cl = goal.evar_concl in let info = out_some goal.evar_info in match r with | { name = Intro; newids = [id] } -> - if !check && mem_var_context id sign then + if !check && mem_named_context id sign then error "New variable is already declared"; (match kind_of_term (strip_outer_cast cl) with | IsProd (_,c1,b) -> if occur_meta c1 then error_use_instantiate(); let a = get_assumption_of env sigma c1 and v = mkVar id in - let sg = mk_goal info (push_var_decl (id,a) env) (subst1 v b) in + let sg = mk_goal info (push_named_assum (id,a) env) (subst1 v b) in [sg] | IsLetIn (_,c1,t1,b) -> if occur_meta c1 or occur_meta t1 then error_use_instantiate(); let a = get_assumption_of env sigma t1 and v = mkVar id in let sg = - mk_goal info (push_var_def (id,c1,a) env) (subst1 v b) in + mk_goal info (push_named_def (id,c1,a) env) (subst1 v b) in [sg] | _ -> if !check then raise (RefinerError IntroNeedsProduct) else anomaly "Intro: expects a product") | { name = Intro_after; newids = [id]; hypspecs = [whereid] } -> - if !check && mem_var_context id sign then + if !check && mem_named_context id sign then error "New variable is already declared"; (match kind_of_term (strip_outer_cast cl) with | IsProd (_,c1,b) -> @@ -363,10 +363,10 @@ let prim_refiner r sigma goal = | _ -> error "not enough products" in check_ind n cl; - if !check && mem_var_context f sign then + if !check && mem_named_context f sign then error ("The name "^(string_of_id f)^" is already used"); let a = get_assumption_of env sigma cl in - let sg = mk_goal info (push_var_decl (f,a) env) cl in + let sg = mk_goal info (push_named_assum (f,a) env) cl in [sg] | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } -> @@ -390,10 +390,10 @@ let prim_refiner r sigma goal = if not (sp=sp') then error ("fixpoints should be on the same " ^ "mutual inductive declaration"); - if mem_var_context f sign then + if mem_named_context f sign then error "name already used in the environment"; let a = get_assumption_of env sigma ar in - mk_sign (add_var_decl (f,a) sign) (lar',lf',ln') + mk_sign (add_named_assum (f,a) sign) (lar',lf',ln') | ([],[],[]) -> List.map (mk_goal info env) (cl::lar) | _ -> error "not the right number of arguments" @@ -416,12 +416,12 @@ let prim_refiner r sigma goal = let rec mk_env env = function | (ar::lar'),(f::lf') -> (try - (let _ = lookup_var f env in + (let _ = lookup_named f env in error "name already used in the environment") with | Not_found -> let a = get_assumption_of env sigma ar in - mk_env (push_var_decl (f,a) env) (lar',lf')) + mk_env (push_named_assum (f,a) env) (lar',lf')) | ([],[]) -> List.map (mk_goal info env) (cl::lar) | _ -> error "not the right number of arguments" in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index a796cd1f44..01df402523 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -97,11 +97,11 @@ val get_pftreestate : unit -> pftreestate the current focused proof or raises a [UserError] if there is no focused proof or if there is no more subgoals *) -val get_goal_context : int -> evar_declarations * env +val get_goal_context : int -> enamed_declarations * env (* [get_current_goal_context ()] works as [get_goal_context 1] *) -val get_current_goal_context : unit -> evar_declarations * env +val get_current_goal_context : unit -> enamed_declarations * env (*s [get_current_proof_name ()] return the name of the current focused proof or failed if no proof is focused *) diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 2f7d069a81..54febf40ba 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -76,7 +76,7 @@ let is_tactic_proof pf = (pf.subproof <> None) with some extra information for the program and mimick tactics. *) -type global_constraints = evar_declarations timestamped +type global_constraints = enamed_declarations timestamped (* A readable constraint is a global constraint plus a focus set of existential variables and a signature. *) @@ -84,7 +84,7 @@ type global_constraints = evar_declarations timestamped type evar_recordty = { focus : local_constraints; env : env; - decls : evar_declarations } + decls : enamed_declarations } and readable_constraints = evar_recordty timestamped @@ -233,7 +233,7 @@ let pr_seq evd = | None -> anomaly "pr_seq : info = None" in let pc = pr_ctxt info in - let pdcl = pr_var_context_of env in + let pdcl = pr_named_context_of env in let pcl = prterm_env_at_top env cl in hOV 0 [< pc; pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >] @@ -244,13 +244,13 @@ let prgl gl = let pr_evgl gl = let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in - let phyps = pr_idl (ids_of_var_context (var_context gl.evar_env)) in + let phyps = pr_idl (ids_of_named_context (named_context gl.evar_env)) in let pc = prterm gl.evar_concl in hOV 0 [< 'sTR"[[" ; plc; 'sTR"] " ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >] let pr_evgl_sign gl = let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in - let ps = pr_var_context_of gl.evar_env in + let ps = pr_named_context_of gl.evar_env in let pc = prterm gl.evar_concl in hOV 0 [< 'sTR"[[" ; plc ; 'sTR"] " ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >] diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 60ae9b4f4c..56ef12fb00 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -37,7 +37,7 @@ val is_tactic_proof : proof_tree -> bool (*s A global constraint is a mappings of existential variables with some extra information for the program and mimick tactics. *) -type global_constraints = evar_declarations timestamped +type global_constraints = enamed_declarations timestamped (*s A readable constraint is a global constraint plus a focus set of existential variables and a signature. *) @@ -45,7 +45,7 @@ type global_constraints = evar_declarations timestamped type evar_recordty = { focus : local_constraints; env : env; - decls : evar_declarations } + decls : enamed_declarations } and readable_constraints = evar_recordty timestamped @@ -53,13 +53,13 @@ val rc_of_gc : global_constraints -> goal -> readable_constraints val rc_add : readable_constraints -> int * goal -> readable_constraints val get_env : readable_constraints -> env val get_focus : readable_constraints -> local_constraints -val get_decls : readable_constraints -> evar_declarations +val get_decls : readable_constraints -> enamed_declarations val get_gc : readable_constraints -> global_constraints val remap : readable_constraints -> int * goal -> readable_constraints val ctxt_access : readable_constraints -> int -> bool val pf_lookup_name_as_renamed : - var_context -> constr -> identifier -> int option + named_context -> constr -> identifier -> int option val pf_lookup_index_as_renamed : constr -> int -> int option @@ -83,6 +83,6 @@ val pr_focus : local_constraints -> std_ppcmds val pr_ctxt : ctxtty -> std_ppcmds val pr_evars : (int * goal) list -> std_ppcmds val pr_evars_int : int -> (int * goal) list -> std_ppcmds -val pr_subgoals_existential : evar_declarations -> goal list -> std_ppcmds +val pr_subgoals_existential : enamed_declarations -> goal list -> std_ppcmds val ast_of_cvt_arg : tactic_arg -> Coqast.t diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 2a65d799b2..ac13464091 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -46,11 +46,11 @@ type ctxtty = { pgm : constr option; lc : local_constraints } -type evar_declarations = ctxtty evar_map +type enamed_declarations = ctxtty evar_map (* A global constraint is a mappings of existential variables with some extra information for the program tactic *) -type global_constraints = evar_declarations timestamped +type global_constraints = enamed_declarations timestamped (* Signature useful to define the tactic type *) type 'a sigma = { diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 1b4a1c60dc..cc64be7162 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -49,11 +49,11 @@ type ctxtty = { pgm : constr option; lc : local_constraints } -type evar_declarations = ctxtty evar_map +type enamed_declarations = ctxtty evar_map (* A global constraint is a mappings of existential variables with some extra information for the program tactic *) -type global_constraints = evar_declarations timestamped +type global_constraints = enamed_declarations timestamped (* Signature useful to define the tactic type *) type 'a sigma = { diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 048ce3721f..868e71f850 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -245,7 +245,7 @@ let extract_open_proof sigma pf = (fun id -> try let n = list_index id vl in (n,id) with Not_found -> failwith "caught") - (ids_of_var_context (evar_hyps goal)) in + (ids_of_named_context (evar_hyps goal)) in let sorted_rels = Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in let abs_concl = @@ -797,12 +797,12 @@ exception Different (* We remove from the var context of env what is already in osign *) let thin_sign osign env = - process_var_context + process_named_context (fun env (id,c,ty as d) -> try if lookup_id id osign = (c,ty) then env else raise Different - with Not_found | Different -> push_var d env) + with Not_found | Different -> push_named_decl d env) env let rec print_proof sigma osign pf = @@ -814,7 +814,7 @@ let rec print_proof sigma osign pf = hOV 0 [< pr_seq {evar_env=env'; evar_concl=cl; evar_info=info; evar_body=body} >] | Some(r,spfl) -> - let sign = var_context env in + let sign = named_context env in hOV 0 [< hOV 0 (pr_seq {evar_env=env'; evar_concl=cl; evar_info=info; evar_body=body}); 'sPC ; 'sTR" BY "; @@ -827,7 +827,7 @@ let pr_change gl = [< 'sTR"Change " ; prterm gl.evar_concl ; 'sTR"." ; 'fNL>] let rec print_script nochange sigma osign pf = let {evar_env=env; evar_concl=cl} = pf.goal in - let sign = var_context env in + let sign = named_context env in match pf.ref with | None -> if nochange then @@ -842,7 +842,7 @@ let rec print_script nochange sigma osign pf = let rec print_treescript sigma osign pf = let {evar_env=env; evar_concl=cl} = pf.goal in - let sign = var_context env in + let sign = named_context env in match pf.ref with | None -> [< >] | Some(r,spfl) -> @@ -858,7 +858,7 @@ let rec print_treescript sigma osign pf = let rec print_info_script sigma osign pf = let {evar_env=env; evar_concl=cl} = pf.goal in - let sign = var_context env in + let sign = named_context env in match pf.ref with | None -> [< >] | Some(r,spfl) -> @@ -887,7 +887,7 @@ let tclINFO (tac : tactic) gls = let (sgl,v) as res = tac gls in begin try let pf = v (List.map leaf (sig_it sgl)) in - let sign = var_context (sig_it gls).evar_env in + let sign = named_context (sig_it gls).evar_env in mSGNL(hOV 0 [< 'sTR" == "; print_subscript ((compose ts_it sig_sig) gls) sign pf >]) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index be59f56857..4c1e2f9770 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -104,7 +104,7 @@ type pftreestate val proof_of_pftreestate : pftreestate -> proof_tree val cursor_of_pftreestate : pftreestate -> int list val is_top_pftreestate : pftreestate -> bool -val evc_of_pftreestate : pftreestate -> evar_declarations +val evc_of_pftreestate : pftreestate -> enamed_declarations val top_goal_of_pftreestate : pftreestate -> goal sigma val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma @@ -137,10 +137,10 @@ val change_constraints_pftreestate open Pp (*i*) -val print_proof : evar_declarations -> var_context -> proof_tree -> std_ppcmds +val print_proof : enamed_declarations -> named_context -> proof_tree -> std_ppcmds val pr_rule : rule -> std_ppcmds val pr_tactic : tactic_expression -> std_ppcmds val print_script : - bool -> evar_declarations -> var_context -> proof_tree -> std_ppcmds + bool -> enamed_declarations -> named_context -> proof_tree -> std_ppcmds val print_treescript : - evar_declarations -> var_context -> proof_tree -> std_ppcmds + enamed_declarations -> named_context -> proof_tree -> std_ppcmds diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index fe4ee94a47..209ea10f67 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -52,10 +52,10 @@ let constr_of_Constr_context = function anomalylabstrm "constr_of_Constr_context" [<'sTR "Not a Constr_context tactic_arg">] -(* Transforms a var_context into a (string * constr) list *) +(* Transforms a named_context into a (string * constr) list *) let make_hyps = List.map (fun (id,_,typ) -> (string_of_id id,body_of_type typ)) -(* let lid = List.map string_of_id (ids_of_var_context hyps) +(* let lid = List.map string_of_id (ids_of_named_context hyps) and lhyp = List.map body_of_type (vals_of_sign hyps) in List.rev (List.combine lid lhyp)*) @@ -70,7 +70,7 @@ let rec constr_list goalopt = function (match goalopt with | None -> constr_list goalopt tl | Some goal -> - if mem_var_context id (pf_hyps goal) then + if mem_named_context id (pf_hyps goal) then (id_of_string str,mkVar id)::(constr_list goalopt tl) else constr_list goalopt tl)) @@ -79,7 +79,7 @@ let rec constr_list goalopt = function (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = - evar_declarations * Environ.env * (string * value) list * + enamed_declarations * Environ.env * (string * value) list * (int * constr) list * goal sigma option (* Table of interpretation functions *) diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 50b454df8f..746c89f08e 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -24,7 +24,7 @@ val constr_of_Constr : tactic_arg -> constr (* Signature for interpretation: [val_interp] and interpretation functions *) type interp_sign = - evar_declarations * Environ.env * (string * value) list * + enamed_declarations * Environ.env * (string * value) list * (int * constr) list * goal sigma option (* Adds a Tactic Definition in the table *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 88ca18f1c5..4b2fcbc8ef 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -37,16 +37,16 @@ let sig_it = Refiner.sig_it let sig_sig = Refiner.sig_sig let project = compose ts_it sig_sig let pf_env gls = (sig_it gls).evar_env -let pf_hyps gls = var_context (sig_it gls).evar_env +let pf_hyps gls = named_context (sig_it gls).evar_env let pf_concl gls = (sig_it gls).evar_concl (* let pf_untyped_hyps gls = - let sign = Environ.var_context (pf_env gls) in + let sign = Environ.named_context (pf_env gls) in map_sign_typ (fun x -> body_of_type x) sign *) let pf_hyps_types gls = - let sign = Environ.var_context (pf_env gls) in + let sign = Environ.named_context (pf_env gls) in List.map (fun (id,_,x) -> (id,body_of_type x)) sign let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id @@ -59,7 +59,7 @@ let pf_get_hyp_typ gls id = with Not_found -> error ("No such hypothesis : " ^ (string_of_id id)) -let pf_ids_of_hyps gls = ids_of_var_context (var_context (pf_env gls)) +let pf_ids_of_hyps gls = ids_of_named_context (named_context (pf_env gls)) let pf_ctxt gls = get_ctxt (sig_it gls) @@ -278,7 +278,7 @@ let mutual_cofix lf lar pf = let rename_bound_var_goal gls = let { evar_env = env; evar_concl = cl } as gl = sig_it gls in - let ids = ids_of_var_context (Environ.var_context env) in + let ids = ids_of_named_context (Environ.named_context env) in convert_concl (rename_bound_var ids cl) gls @@ -510,7 +510,7 @@ open Printer let pr_com sigma goal com = prterm (rename_bound_var - (ids_of_var_context (var_context goal.evar_env)) + (ids_of_named_context (named_context goal.evar_env)) (Astterm.interp_constr sigma goal.evar_env com)) let pr_one_binding sigma goal = function diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 9108d48cfa..8eb0b39e6a 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -22,7 +22,7 @@ type tactic = Proof_type.tactic;; val sig_it : 'a sigma -> 'a val sig_sig : goal sigma -> global_constraints -val project : goal sigma -> evar_declarations +val project : goal sigma -> enamed_declarations val re_sig : 'a -> global_constraints -> 'a sigma @@ -33,11 +33,11 @@ val apply_sig_tac : val pf_concl : goal sigma -> constr val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> var_context +val pf_hyps : goal sigma -> named_context (*i val pf_untyped_hyps : goal sigma -> (identifier * constr) list i*) val pf_hyps_types : goal sigma -> (identifier * constr) list val pf_nth_hyp_id : goal sigma -> int -> identifier -val pf_last_hyp : goal sigma -> var_declaration +val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> identifier list val pf_ctxt : goal sigma -> ctxtty val pf_global : goal sigma -> identifier -> constr @@ -57,7 +57,7 @@ val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr val pf_reduce : - (env -> evar_declarations -> constr -> constr) -> + (env -> enamed_declarations -> constr -> constr) -> goal sigma -> constr -> constr val pf_whd_betadeltaiota : goal sigma -> constr -> constr @@ -90,7 +90,7 @@ type pftreestate val proof_of_pftreestate : pftreestate -> proof_tree val cursor_of_pftreestate : pftreestate -> int list val is_top_pftreestate : pftreestate -> bool -val evc_of_pftreestate : pftreestate -> evar_declarations +val evc_of_pftreestate : pftreestate -> enamed_declarations val top_goal_of_pftreestate : pftreestate -> goal sigma val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma val traverse : int -> pftreestate -> pftreestate @@ -193,9 +193,9 @@ val w_Focusing_THEN : int -> 'a result_w_tactic val w_Declare : int -> constr * constr -> w_tactic val w_Declare_At : int -> int -> constr * constr -> w_tactic val w_Define : int -> constr -> w_tactic -val w_Underlying : walking_constraints -> evar_declarations +val w_Underlying : walking_constraints -> enamed_declarations val w_env : walking_constraints -> env -val w_hyps : walking_constraints -> var_context +val w_hyps : walking_constraints -> named_context val w_type_of : walking_constraints -> constr -> constr val w_add_sign : (identifier * typed_type) -> walking_constraints -> walking_constraints diff --git a/tactics/auto.ml b/tactics/auto.ml index 89f84332ea..c8c75cd5ea 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -756,7 +756,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal = List.map (fun ntac -> tclTHEN ntac - (search_gen decomp (n-1) db_list local_db empty_var_context)) + (search_gen decomp (n-1) db_list local_db empty_named_context)) (possible_resolve db_list local_db (pf_concl goal)) in tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal @@ -905,10 +905,10 @@ let rec super_search n db_list local_db argl goal = let search_superauto n ids argl g = let sigma = List.fold_right - (fun id -> add_var_decl + (fun id -> add_named_assum (id,Retyping.get_assumption_of (pf_env g) (project g) (pf_type_of g (pf_global g id)))) - ids empty_var_context in + ids empty_named_context in let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in let db = Hint_db.add_list db0 (make_local_hint_db g) in super_search n [Stringmap.find "core" !searchtable] db argl g diff --git a/tactics/auto.mli b/tactics/auto.mli index 399176c5bc..14df28f548 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -88,7 +88,7 @@ val make_resolves : If the hyp cannot be used as a Hint, the empty list is returned. *) val make_resolve_hyp : - env -> 'a evar_map -> var_declaration -> + env -> 'a evar_map -> named_declaration -> (constr_label * pri_auto_tactic) list (* [make_extern name pri pattern tactic_ast] *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 09c8767e23..8c6ace2f61 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -606,7 +606,7 @@ let discr id gls = | Inl (cpath, (_,dirn), _) -> let e = pf_get_new_id (id_of_string "ee") gls in let e_env = - push_var_decl (e,assumption_of_judgment env sigma tj) env + push_named_assum (e,assumption_of_judgment env sigma tj) env in let discriminator = build_discriminator sigma e_env dirn (mkVar e) sort cpath in @@ -885,7 +885,7 @@ let inj id gls = | Inr posns -> let e = pf_get_new_id (id_of_string "e") gls in let e_env = - push_var_decl (e,assumption_of_judgment env sigma tj) env + push_named_assum (e,assumption_of_judgment env sigma tj) env in let injectors = map_succeed @@ -951,7 +951,7 @@ let decompEqThen ntac id gls = | Inl (cpath, (_,dirn), _) -> let e = pf_get_new_id (id_of_string "e") gls in let e_env = - push_var_decl (e,assumption_of_judgment env sigma tj) env in + push_named_assum (e,assumption_of_judgment env sigma tj) env in let discriminator = build_discriminator sigma e_env dirn (mkVar e) sort cpath in let (pf, absurd_term) = @@ -963,7 +963,7 @@ let decompEqThen ntac id gls = | Inr posns -> (let e = pf_get_new_id (id_of_string "e") gls in let e_env = - push_var_decl (e,assumption_of_judgment env sigma tj) env in + push_named_assum (e,assumption_of_judgment env sigma tj) env in let injectors = map_succeed (fun (cpath,t1_0,t2_0) -> @@ -1356,7 +1356,7 @@ let sub_term_with_unif cref ceq = let general_rewrite_in lft2rgt id (c,lb) gls = let typ_id = (try - let (_,ty) = lookup_var id (pf_env gls) in (body_of_type ty) + let (_,ty) = lookup_named id (pf_env gls) in (body_of_type ty) with Not_found -> errorlabstrm "general_rewrite_in" [< 'sTR"No such hypothesis : "; print_id id >]) @@ -1422,7 +1422,7 @@ let v_conditional_rewriteRL_in = let rewrite_in lR com id gls = (try - let _ = lookup_var id (pf_env gls) in () + let _ = lookup_named id (pf_env gls) in () with Not_found -> errorlabstrm "rewrite_in" [< 'sTR"No such hypothesis : " ;print_id id >]); let c = pf_interp_constr gls com in diff --git a/tactics/inv.ml b/tactics/inv.ml index ed5406b79c..fa26027897 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -181,7 +181,7 @@ let rec dependent_hyps id idlist sign = let rec dep_rec =function | [] -> [] | (id1::l) -> - let id1ty = snd (lookup_var id1 sign) in + let id1ty = snd (lookup_named id1 sign) in if occur_var id (body_of_type id1ty) then id1::dep_rec l else dep_rec l in dep_rec idlist diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 1e115c671e..9efdd718ec 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -94,7 +94,7 @@ let thin_ids (hyps,vars) = (* let get_local_sign sign = let lid = ids_of_sign sign in - let globsign = Global.var_context() in + let globsign = Global.named_context() in let add_local id res_sign = if not (mem_sign globsign id) then add_sign (lookup_sign id sign) res_sign @@ -129,12 +129,12 @@ let rec add_prods_sign env sigma t = let id = Environ.id_of_name_using_hdchar env t na in let b'= subst1 (mkVar id) b in let j = Retyping.get_assumption_of env sigma c1 in - add_prods_sign (Environ.push_var_decl (id,j) env) sigma b' + add_prods_sign (Environ.push_named_assum (id,j) env) sigma b' | IsLetIn (na,c1,t1,b) -> let id = Environ.id_of_name_using_hdchar env t na in let b'= subst1 (mkVar id) b in let j = Retyping.get_assumption_of env sigma t1 in - add_prods_sign (Environ.push_var_def (id,c1,j) env) sigma b' + add_prods_sign (Environ.push_named_def (id,c1,j) env) sigma b' | _ -> (env,t) (* [dep_option] indicates wether the inversion lemma is dependent or not. @@ -166,9 +166,9 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let i = mkAppliedInd ind in let ivars = global_vars i in let revargs,ownsign = - fold_var_context + fold_named_context (fun env (id,_,_ as d) (revargs,hyps) -> - if List.mem id ivars then ((mkVar id)::revargs,add_var d hyps) + if List.mem id ivars then ((mkVar id)::revargs,add_named_decl d hyps) else (revargs,hyps)) env ([],[]) in let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in @@ -177,7 +177,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = in let npty = nf_betadeltaiota env sigma pty in let nptyj = make_typed npty (Retyping.get_sort_of env sigma npty) in - let extenv = push_var_decl (p,nptyj) env in + let extenv = push_named_assum (p,nptyj) env in extenv, goal (* [inversion_scheme sign I] @@ -195,7 +195,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) in let (invEnv,invGoal) = compute_first_inversion_scheme env sigma ind sort dep_option in - assert (list_subset (global_vars invGoal) (ids_of_var_context (var_context invEnv))); + assert (list_subset (global_vars invGoal) (ids_of_named_context (named_context invEnv))); (* errorlabstrm "lemma_inversion" [< 'sTR"Computed inversion goal was not closed in initial signature" >]; @@ -205,18 +205,18 @@ let inversion_scheme env sigma t sort dep_option inv_op = solve_pftreestate (tclTHEN intro (onLastHyp (compose inv_op out_some))) pfs in let (pfterm,meta_types) = extract_open_pftreestate pfs in - let global_var_context = Global.var_context () in + let global_named_context = Global.named_context () in let ownSign = - fold_var_context + fold_named_context (fun env (id,_,_ as d) sign -> - if mem_var_context id global_var_context then sign - else add_var d sign) - invEnv empty_var_context in + if mem_named_context id global_named_context then sign + else add_named_decl d sign) + invEnv empty_named_context in let (_,ownSign,mvb) = List.fold_left (fun (avoid,sign,mvb) (mv,mvty) -> let h = next_ident_away (id_of_string "H") avoid in - (h::avoid, add_var_decl (h,mvty) sign, (mv,mkVar h)::mvb)) + (h::avoid, add_named_assum (h,mvty) sign, (mv,mkVar h)::mvb)) (ids_of_context invEnv, ownSign, []) meta_types in let invProof = diff --git a/tactics/refine.ml b/tactics/refine.ml index 62e872184e..faa49b3e2d 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -120,7 +120,7 @@ let replace_in_array env a = let fresh env n = let id = match n with Name x -> x | _ -> id_of_string "_" in - next_global_ident_away id (ids_of_var_context (var_context env)) + next_global_ident_away id (ids_of_named_context (named_context env)) let rec compute_metamap env c = match kind_of_term c with (* le terme est directement une preuve *) @@ -139,7 +139,7 @@ let rec compute_metamap env c = match kind_of_term c with | IsLambda (name,c1,c2) -> let v = fresh env name in let tj = Retyping.get_assumption_of env Evd.empty c1 in - let env' = push_var_decl (v,tj) env in + let env' = push_named_assum (v,tj) env in begin match compute_metamap env' (subst1 (mkVar v) c2) with (* terme de preuve complet *) | TH (_,_,[]) -> TH (c,[],[]) @@ -180,7 +180,7 @@ let rec compute_metamap env c = match kind_of_term c with let vi = List.rev (List.map (fresh env) fi) in let env' = List.fold_left - (fun env (v,ar) -> push_var_decl (v,Retyping.get_assumption_of env Evd.empty ar) env) + (fun env (v,ar) -> push_named_assum (v,Retyping.get_assumption_of env Evd.empty ar) env) env (List.combine vi (Array.to_list ai)) in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 1ed2e536b4..0c513c2cf7 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -65,7 +65,7 @@ let tclTRY_sign (tac : constr->tactic) sign gl = | [s] -> tac (mkVar s) (*added in order to get useful error messages *) | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) in - arec (ids_of_var_context sign) gl + arec (ids_of_named_context sign) gl let tclTRY_HYPS (tac : constr->tactic) gl = tclTRY_sign tac (pf_hyps gl) gl diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4b89938276..1f3ede3938 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -34,7 +34,7 @@ val tclWEAK_PROGRESS : tactic -> tactic val tclNTH_HYP : int -> (constr -> tactic) -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic val tclLAST_HYP : (constr -> tactic) -> tactic -val tclTRY_sign : (constr -> tactic) -> var_context -> tactic +val tclTRY_sign : (constr -> tactic) -> named_context -> tactic val tclTRY_HYPS : (constr -> tactic) -> tactic (*i diff --git a/tactics/tactics.ml b/tactics/tactics.ml index adf147b869..8264af76d2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -134,7 +134,7 @@ let dyn_mutual_cofix argsl gl = (* Reduction and conversion tactics *) (**************************************************************) -type 'a tactic_reduction = env -> evar_declarations -> constr -> constr +type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr (* The following two tactics apply an arbitrary reduction function either to the conclusion or to a @@ -585,7 +585,7 @@ let generalize_goal gl c cl = let generalize_dep c gl = let sign = pf_hyps gl in - let init_ids = ids_of_var_context (Global.var_context()) in + let init_ids = ids_of_named_context (Global.named_context()) in let rec seek toquant d = if List.exists (fun (id,_,_) -> occur_var_in_decl id d) toquant or dependent_in_decl c d then @@ -598,7 +598,7 @@ let generalize_dep c gl = let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in let tothin' = match kind_of_term c with - | IsVar id when mem_var_context id sign & not (List.mem id init_ids) + | IsVar id when mem_named_context id sign & not (List.mem id init_ids) -> id::tothin | _ -> tothin in @@ -669,10 +669,10 @@ let letin_abstract id c occ_ccl occ_hyps gl = (accu,Some hyp) in let (depdecls,marks,rest),_ = - fold_var_context_reverse abstract (([],[],occ_hyps),None) env in + fold_named_context_reverse abstract (([],[],occ_hyps),None) env in if rest <> [] then begin let id = fst (List.hd rest) in - if mem_var_context id (var_context env) + if mem_named_context id (named_context env) then error ("Hypothesis "^(string_of_id id)^" occurs twice") else error ("No such hypothesis : " ^ (string_of_id id)) end; @@ -687,7 +687,7 @@ let letin_tac with_eq name c occ_ccl occ_hyps gl = let env = pf_env gl in let used_ids = ids_of_context env in let id = next_global_ident_away x used_ids in - if mem_var_context id (var_context env) then + if mem_named_context id (named_context env) then error "New variable is already declared"; let (depdecls,marks,ccl)= letin_abstract id c occ_ccl occ_hyps gl in let t = pf_type_of gl c in @@ -1218,7 +1218,7 @@ let cook_sign hyp0 indvars env = else Some hyp in - let _ = fold_var_context seek_deps env None in + let _ = fold_named_context seek_deps env None in (* 2nd pass from R to L: get left hyp of [hyp0] and [lhyps] *) let compute_lstatus lhyp (hyp,_,_ as d) = if hyp = hyp0 then raise (Shunt lhyp); @@ -1229,7 +1229,7 @@ let cook_sign hyp0 indvars env = (Some hyp) in try - let _ = fold_var_context_reverse compute_lstatus None env in + let _ = fold_named_context_reverse compute_lstatus None env in anomaly "hyp0 not found" with Shunt lhyp0 -> let statuslists = (!lstatus,List.rev !rstatus) in @@ -1290,7 +1290,7 @@ let get_constructors varname (elimc,elimt) mind mindpath = let induction_from_context hyp0 gl = (*test suivant sans doute inutile car protégé par le letin_tac avant appel*) - if List.mem hyp0 (ids_of_var_context (Global.var_context())) then + if List.mem hyp0 (ids_of_named_context (Global.named_context())) then errorlabstrm "induction" [< 'sTR "Cannot generalize a global variable" >]; let env = pf_env gl in let tmptyp0 = pf_get_hyp_typ gl hyp0 in @@ -1321,7 +1321,7 @@ let induction_with_atomization_of_ind_arg hyp0 = let new_induct c gl = match kind_of_term c with - | IsVar id when not (mem_var_context id (Global.var_context())) -> + | IsVar id when not (mem_named_context id (Global.named_context())) -> tclORELSE (tclTHEN (intros_until id) (tclLAST_HYP simplest_elim)) (induction_with_atomization_of_ind_arg id) gl @@ -1645,15 +1645,15 @@ let dyn_transitivity = function let abstract_subproof name tac gls = let env = Global.env() in - let current_sign = Global.var_context() + let current_sign = Global.named_context() and global_sign = pf_hyps gls in let sign = List.fold_right (fun (id,_,_ as d) s -> - if mem_var_context id current_sign then s else add_var d s) - global_sign empty_var_context + if mem_named_context id current_sign then s else add_named_decl d s) + global_sign empty_named_context in let na = next_global_ident_away name - (ids_of_var_context global_sign) in + (ids_of_named_context global_sign) in let concl = List.fold_left (fun t d -> mkNamedProd_or_LetIn d t) (pf_concl gls) sign in let env' = change_hyps (fun _ -> current_sign) env in @@ -1672,7 +1672,7 @@ let abstract_subproof name tac gls = Declare.construct_reference newenv CCI na in exact_no_check (applist (lemme, - List.map mkVar (List.rev (ids_of_var_context sign)))) + List.map mkVar (List.rev (ids_of_named_context sign)))) gls let tclABSTRACT name_op tac gls = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index e7e15881d0..b41c07ec37 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -94,7 +94,7 @@ val dyn_exact_check : tactic_arg list -> tactic (*s Reduction tactics. *) -type 'a tactic_reduction = env -> evar_declarations -> constr -> constr +type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr val reduct_in_hyp : 'a tactic_reduction -> identifier -> tactic val reduct_option : 'a tactic_reduction -> identifier option -> tactic diff --git a/tactics/tauto.ml b/tactics/tauto.ml index 7e99167e71..6f7499057d 100644 --- a/tactics/tauto.ml +++ b/tactics/tauto.ml @@ -1762,7 +1762,7 @@ let search env id = try mkRel (fst (lookup_rel_id id (Environ.rel_context env))) with Not_found -> - if mem_var_context id (Environ.var_context env) then + if mem_named_context id (Environ.named_context env) then mkVar id else global_reference CCI id @@ -1851,7 +1851,7 @@ let t_exacto = ref (TVar "#") let tautoOR ti gls = let thyp = pf_hyps gls in - hipvar := ids_of_var_context thyp; + hipvar := ids_of_named_context thyp; let but = pf_concl gls in let seq = (constr_lseq gls thyp, constr_rseq gls but) in let vp = lisvarprop (ante seq) in diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 320e8d56f3..4943756e3d 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -93,7 +93,7 @@ let clenv_constrain_with_bindings bl clause = let add_prod_rel sigma (t,env) = match kind_of_term t with | IsProd (na,t1,b) -> - (b,push_rel_decl (na,Retyping.get_assumption_of env sigma t1) env) + (b,push_rel_assum (na,Retyping.get_assumption_of env sigma t1) env) | IsLetIn (na,c1,t1,b) -> (b,push_rel_def (na,c1,Retyping.get_assumption_of env sigma t1) env) | _ -> failwith "add_prod_rel" diff --git a/toplevel/command.ml b/toplevel/command.ml index 1fd4fc4034..6150f0c024 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -141,7 +141,7 @@ let build_mutual lparams lnamearconstrs finite = let raw_arity = mkProdCit lparams arityc in let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in let arity = Typeops.assumption_of_type_judgment arj in - let env' = Environ.push_rel_decl (Name recname,arity) env in + let env' = Environ.push_rel_assum (Name recname,arity) env in (env', (arity::arl))) (env0,[]) lnamearconstrs in @@ -218,7 +218,7 @@ let build_recursive lnameargsardef = let arity = Typeops.assumption_of_type_judgment arj in declare_variable recname (SectionLocalDecl arj.utj_val,NeverDischarge,false); - (Environ.push_var_decl (recname,arity) env, (arity::arl))) + (Environ.push_named_assum (recname,arity) env, (arity::arl))) (env0,[]) lnameargsardef with e -> States.unfreeze fs; raise e @@ -286,7 +286,7 @@ let build_corecursive lnameardef = let arity = Typeops.assumption_of_type_judgment arj in declare_variable recname (SectionLocalDecl arj.utj_val,NeverDischarge,false); - (Environ.push_var_decl (recname,arity) env, (arity::arl))) + (Environ.push_named_assum (recname,arity) env, (arity::arl))) (env0,[]) lnameardef with e -> States.unfreeze fs; raise e diff --git a/toplevel/command.mli b/toplevel/command.mli index fb9071d0f7..263d670324 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -56,4 +56,4 @@ theorem under the name [name] and gives it the strength of a remark *) val save_anonymous_remark : bool -> string -> unit -val get_current_context : unit -> Proof_type.evar_declarations * Environ.env +val get_current_context : unit -> Proof_type.enamed_declarations * Environ.env diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 17ccac01d5..2cfd2ca647 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -236,7 +236,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = (Array.map (expmod_type oldenv modlist) (mind_user_lc mip)))) mib.mind_packets in - let hyps' = map_var_context (expmod_constr oldenv modlist) mib.mind_hyps in + let hyps' = map_named_context (expmod_constr oldenv modlist) mib.mind_hyps in let (inds',modl) = abstract_inductive ids_to_discard hyps' inds in let lmodif_one_mind i = let nbc = Array.length (mind_nth_type_packet mib i).mind_consnames in @@ -261,7 +261,7 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb = let body = expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in let typ = expmod_type oldenv modlist cb.const_type in - let hyps = map_var_context (expmod_constr oldenv modlist) cb.const_hyps in + let hyps = map_named_context (expmod_constr oldenv modlist) cb.const_hyps in let (body',typ',modl) = abstract_constant ids_to_discard hyps (body,typ) in let mods = [ (ConstRef osecsp, DO_ABSTRACT(ConstRef nsecsp,modl)) ] in (body', body_of_type typ', mods) @@ -403,7 +403,7 @@ let close_section _ s = let (sec_sp,decls) = close_section s in let (ops,ids,_) = List.fold_left (process_item oldenv sec_sp) ([],[],[]) decls in - Global.pop_vars ids; + Global.pop_named_decls ids; List.iter process_operation (List.rev ops) diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index 92fb1bd93b..aecec0c251 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -30,19 +30,19 @@ module Make = functor (P : Printer) -> struct (**** let sign_it_with f sign e = - snd (fold_var_context - (fun (id,v,t) (sign,e) -> (add_var (id,v,t) sign, f id t sign e)) - sign (empty_var_context,e)) + snd (fold_named_context + (fun (id,v,t) (sign,e) -> (add_named_decl (id,v,t) sign, f id t sign e)) + sign (empty_named_context,e)) let dbenv_it_with f env e = snd (dbenv_it - (fun na t (env,e) -> (add_rel (na,t) env, f na t env e)) + (fun na t (env,e) -> (add_rel_decl (na,t) env, f na t env e)) env (gLOB(get_globals env),e)) ****) let pr_env k env = let sign_env = - fold_var_context + fold_named_context (fun env (id,_,t) pps -> let pidt = print_decl k env (id,t) in [< pps ; 'fNL ; pidt >]) env [< >] @@ -56,7 +56,7 @@ module Make = functor (P : Printer) -> struct [< sign_env; db_env >] let pr_ne_ctx header k env = - if rel_context env = [] && var_context env = [] then + if rel_context env = [] && named_context env = [] then [< >] else [< header; pr_env k env >] diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b7bd4ecfe4..1fe9d21aba 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -95,7 +95,7 @@ let explain_generalization k ctx (name,var) j = let ctx = make_all_name_different ctx in let pe = pr_ne_context_of [< 'sTR"in environment" >] k ctx in let pv = prtype_env ctx var in - let (pc,pt) = prjudge_env (push_rel_decl (name,var) ctx) j in + let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in [< 'sTR"Illegal generalization: "; pe; 'fNL; 'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC; 'sTR"over"; 'bRK(1,1); pc; 'sTR","; 'sPC; 'sTR"it has type"; 'sPC; pt; diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 171f31dae4..6276438e10 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -15,7 +15,7 @@ open G_minicoq let (env : safe_environment ref) = ref empty_environment -let lookup_var id = +let lookup_named id = let rec look n = function | [] -> mkVar id | (Name id')::_ when id = id' -> Rel n @@ -23,10 +23,10 @@ let lookup_var id = in look 1 -let args sign = Array.of_list (List.map mkVar (ids_of_var_context sign)) +let args sign = Array.of_list (List.map mkVar (ids_of_named_context sign)) let rec globalize bv c = match kind_of_term c with - | IsVar id -> lookup_var id bv + | IsVar id -> lookup_named id bv | IsConst (sp, _) -> let cb = lookup_constant sp !env in mkConst (sp, args cb.const_hyps) | IsMutInd (sp,_ as spi, _) -> @@ -59,7 +59,7 @@ let parameter id t = let variable id t = let t = globalize [] t in - env := push_var_decl (id,t) !env; + env := push_named_assum (id,t) !env; mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; print_id id; 'sPC; 'sTR"is declared"; 'fNL >]) diff --git a/toplevel/record.ml b/toplevel/record.ml index f23430ae4b..321f9bf31b 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -73,7 +73,7 @@ let typecheck_params_and_field ps fs = (fun (env,newps) (id,t) -> let tj = type_judgment_of_rawconstr Evd.empty env t in let ass = Typeops.assumption_of_type_judgment tj in - (Environ.push_var_decl (id,ass) env,(id,tj.Environ.utj_val)::newps)) + (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newps)) (env0,[]) ps in let env2,newfs = @@ -81,7 +81,7 @@ let typecheck_params_and_field ps fs = (fun (env,newfs) (id,t) -> let tj = type_judgment_of_rawconstr Evd.empty env t in let ass = Typeops.assumption_of_type_judgment tj in - (Environ.push_var_decl (id,ass) env,(id,tj.Environ.utj_val)::newfs)) (env1,[]) fs + (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newfs)) (env1,[]) fs in List.rev(newps),List.rev(newfs) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a1db3b78a1..afe871641e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -48,13 +48,13 @@ let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - mSGNL(Refiner.print_script true evc (Global.var_context()) pf) + mSGNL(Refiner.print_script true evc (Global.named_context()) pf) let show_prooftree () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - mSG(Refiner.print_proof evc (Global.var_context()) pf) + mSG(Refiner.print_proof evc (Global.named_context()) pf) let show_open_subgoals () = let pfts = get_pftreestate () in @@ -591,7 +591,7 @@ let _ = | (n::l) -> aux (Tacmach.traverse n pts) l in let pts = aux pts (l@[-1]) in let pf = proof_of_pftreestate pts in - mSG (Refiner.print_script true evc (Global.var_context()) pf)) + mSG (Refiner.print_script true evc (Global.named_context()) pf)) let _ = add "ExplainProofTree" @@ -608,7 +608,7 @@ let _ = | (n::l) -> aux (Tacmach.traverse n pts) l in let pts = aux pts (l@[-1]) in let pf = proof_of_pftreestate pts in - mSG (Refiner.print_proof evc (Global.var_context()) pf)) + mSG (Refiner.print_proof evc (Global.named_context()) pf)) let _ = add "ShowProofs" |