diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-30 21:17:02 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-14 14:37:22 +0100 |
| commit | 00e27eac9fe207d754952c1ddb0e12861ee293c9 (patch) | |
| tree | cf64342ebf48bf248124bbb54844a70b77d1fa0e /tactics/tacinterp.ml | |
| parent | 072aa1f8c4e3ff08d1343e1f068a41648c06b7fd (diff) | |
Moving is_quantified_hypothesis to new proof engine.
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 74ddd6b57..5f5adaafb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1852,7 +1852,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (* TODO: move sigma as a side-effect *) (* spiwack: the [*p] variants are for printing *) let cp = c in - let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in + let c = interp_induction_arg ist gl c in let ipato = interp_intro_pattern_naming_option ist env sigma ipato in let ipatsp = ipats in let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in |