diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 9a0b56b84b..5c7659ac0e 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -22,7 +22,7 @@ let project x = x.sigma (* Getting env *) let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) -let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) +let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) let refiner pr goal_sigma = let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in @@ -198,10 +198,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.Named.t = pf_hyps goal in + let oldhyps = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in - let hyps:Context.Named.t list = + let hyps = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in let newhyps = |