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 /tactics/class_tactics.ml | |
| parent | d4b344acb23f19b089098b7788f37ea22bc07b81 (diff) | |
Proofview.Goal primitive now return EConstrs.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6c45bef1c6..bf4e53b103 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -249,7 +249,6 @@ let unify_resolve_refine poly flags = { enter = begin fun gls ((c, t, ctx),n,clenv) -> let env = Proofview.Goal.env gls in let concl = Proofview.Goal.concl gls in - let concl = EConstr.of_constr concl in Refine.refine ~unsafe:true { Sigma.run = fun sigma -> let sigma = Sigma.to_evar_map sigma in let sigma, term, ty = @@ -363,7 +362,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = Proofview.Goal.nf_enter { enter = begin fun gl -> let tacs = e_trivial_resolve db_list local_db secvars only_classes - (project gl) (EConstr.of_constr (pf_concl gl)) in + (project gl) (pf_concl gl) in tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) end} in @@ -1002,7 +1001,6 @@ module Search = struct let open Proofview.Notations in let env = Goal.env gl in let concl = Goal.concl gl in - let concl = EConstr.of_constr concl in let sigma = Goal.sigma gl in let s = Sigma.to_evar_map sigma in let unique = not info.search_dep || is_unique env s concl in |