diff options
| author | Pierre-Marie Pédrot | 2014-03-25 19:27:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-26 12:46:20 +0100 |
| commit | 1dccf4412cf9f5903c6291e08f2001c895babfd1 (patch) | |
| tree | dc643bc580346bd4fee02d31e3f3c1acec6b855e /proofs/clenv.ml | |
| parent | 1d933c489d1f9d064fd54a4487754a86a0aed506 (diff) | |
Moving some tactic code to the new engine.
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 966d247e0e..444043dbe2 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -496,8 +496,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function let make_clenv_binding_env_apply env sigma n = make_clenv_binding_gen true n env sigma -let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma -let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma +let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma +let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma (****************************************************************) (* Pretty-print *) |