diff options
| author | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
| commit | 835be3a05e28eb6e26f703a034f22b2c6c61acaa (patch) | |
| tree | 00ecf04840ba027c3c71f8503d9811c8a5dc1d2e /proofs/refiner.ml | |
| parent | 0980dbb1740c8d48d8ff0c516929f27f8cea854d (diff) | |
| parent | 2e6a89238dc7197057d0da80a16f4b4b1e41bfd8 (diff) | |
Merge PR#379: Introducing evar-insensitive constrs
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 = |