diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index fb22da83..11f2c594 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -400,8 +400,8 @@ let intern_red_expr ist = function | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r -let intern_in_hyp_as ist lf (clear,id,ipat) = - (clear,intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat) +let intern_in_hyp_as ist lf (id,ipat) = + (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat) let intern_hyp_list ist = List.map (intern_hyp ist) |