diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index fb22da83aa..1778221b02 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -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) |