From 00e27eac9fe207d754952c1ddb0e12861ee293c9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 30 Dec 2015 21:17:02 +0100 Subject: Moving is_quantified_hypothesis to new proof engine. --- tactics/tacinterp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/tacinterp.ml') 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 -- cgit v1.2.3