From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 31 Oct 2017 17:04:02 +0100 Subject: Add relevance marks on binders. Kernel should be mostly correct, higher levels do random stuff at times. --- proofs/clenv.ml | 9 +++++---- proofs/proof_global.ml | 5 +++-- proofs/tacmach.ml | 2 +- proofs/tacmach.mli | 2 +- 4 files changed, 10 insertions(+), 8 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 9540d3de44..2d2113b636 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -15,6 +15,7 @@ open Names open Nameops open Termops open Constr +open Context open Namegen open Environ open Evd @@ -69,7 +70,7 @@ let clenv_push_prod cl = | Prod (na,t,u) -> let mv = new_meta () in let dep = not (noccurn (cl_sigma cl) 1 u) in - let na' = if dep then na else Anonymous in + let na' = if dep then na.binder_name else Anonymous in let e' = meta_declare mv t ~name:na' cl.evd in let concl = if dep then subst1 (mkMeta mv) u else u in let def = applist (cl.templval.rebus,[mkMeta mv]) in @@ -103,7 +104,7 @@ let clenv_environments evd bound t = | (n, Prod (na,t1,t2)) -> let mv = new_meta () in let dep = not (noccurn evd 1 t2) in - let na' = if dep then na else Anonymous in + let na' = if dep then na.binder_name else Anonymous in let e' = meta_declare mv t1 ~name:na' e in clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) t2) else t2) @@ -277,7 +278,7 @@ let adjust_meta_source evd mv = function | loc,Evar_kinds.VarInstance id -> let rec match_name c l = match EConstr.kind evd c, l with - | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id + | Lambda ({binder_name=Name id},_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id | Lambda (_,_,c), a::l -> match_name c l | _ -> None in (* This is very ad hoc code so that an evar inherits the name of the binder @@ -623,7 +624,7 @@ let make_evar_clause env sigma ?len t = hole_type = t1; hole_deps = dep; (* We fix it later *) - hole_name = na; + hole_name = na.binder_name; } in let t2 = if dep then subst1 ev t2 else t2 in clrec (sigma, hole :: holes) inst (pred n) t2 diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a47fa78f4d..6174b75a96 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -19,6 +19,7 @@ open Util open Pp open Names +open Context module NamedDecl = Context.Named.Declaration @@ -198,10 +199,10 @@ let set_used_variables l = let vars_of = Environ.global_vars_set in let aux env entry (ctx, all_safe as orig) = match entry with - | LocalAssum (x,_) -> + | LocalAssum ({binder_name=x},_) -> if Id.Set.mem x all_safe then orig else (ctx, all_safe) - | LocalDef (x,bo, ty) as decl -> + | LocalDef ({binder_name=x},bo, ty) as decl -> if Id.Set.mem x all_safe then orig else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in if Id.Set.subset vars all_safe diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index df90354717..8196f5e198 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -172,7 +172,7 @@ module New = struct let env = Proofview.Goal.env gl in let sign = Environ.named_context env in List.map (function LocalAssum (id,x) - | LocalDef (id,_,x) -> id, EConstr.of_constr x) + | LocalDef (id,_,x) -> id.Context.binder_name, EConstr.of_constr x) sign let pf_last_hyp gl = diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 213ed7bfda..1454140dd7 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -29,7 +29,7 @@ val pf_concl : Goal.goal sigma -> types val pf_env : Goal.goal sigma -> env val pf_hyps : Goal.goal sigma -> named_context (*i val pf_untyped_hyps : Goal.goal sigma -> (Id.t * constr) list i*) -val pf_hyps_types : Goal.goal sigma -> (Id.t * types) list +val pf_hyps_types : Goal.goal sigma -> (Id.t Context.binder_annot * types) list val pf_nth_hyp_id : Goal.goal sigma -> int -> Id.t val pf_last_hyp : Goal.goal sigma -> named_declaration val pf_ids_of_hyps : Goal.goal sigma -> Id.t list -- cgit v1.2.3