diff options
| author | Pierre-Marie Pédrot | 2016-11-20 22:16:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:34 +0100 |
| commit | e09f3b44bb381854b647a6d9debdeddbfc49177e (patch) | |
| tree | e7ba5807fa369b912cb36fe50bba97d33f7af5b5 /proofs/refine.ml | |
| parent | d4b344acb23f19b089098b7788f37ea22bc07b81 (diff) | |
Proofview.Goal primitive now return EConstrs.
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 11eabe0a90..32064aff50 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -77,7 +77,6 @@ let make_refine_enter ?(unsafe = true) f = let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in (** Save the [future_goals] state to restore them after the refinement. *) let prev_future_goals = Evd.future_goals sigma in @@ -146,7 +145,6 @@ let with_type env evd c t = let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let env = Proofview.Goal.env gl in let f = { run = fun h -> let Sigma (c, h, p) = f.run h in |