diff options
| author | Hugo Herbelin | 2014-10-16 19:34:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-16 22:28:42 +0200 |
| commit | 3c2723f77f5ab070f8232ce0cc626875120cfe41 (patch) | |
| tree | e52b630876715c95e44b294e9c2dc17ab6ceff83 | |
| parent | 4158d921d506ce931ec940c55005f0698be9616b (diff) | |
In convert_concl/convert_hyp: nf_enter -> enter.
(Maybe one of the source of inefficiency introduced on Oct 9 - see e.g. CoLoR.)
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d131e2d33d..26b05c68ec 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -120,7 +120,7 @@ let introduction = Tacmach.introduction let refine = Tacmach.refine let convert_concl ?(check=true) ty k = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let conclty = Proofview.Goal.raw_concl gl in @@ -139,7 +139,7 @@ let convert_concl ?(check=true) ty k = end let convert_hyp ?(check=true) d = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let ty = Proofview.Goal.raw_concl gl in |