diff options
Diffstat (limited to 'tactics/redexpr.ml')
| -rw-r--r-- | tactics/redexpr.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index b415b30de8..3ee85f6b1b 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -46,9 +46,6 @@ let cbv_native env sigma c = let whd_cbn = Cbn.whd_cbn -let strong_cbn flags = - strong_with_flags whd_cbn flags - let simplIsCbn = Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false @@ -248,11 +245,11 @@ let reduction_of_red_expr_val = function | Hnf -> (e_red hnf_constr,DEFAULTcast) | Simpl (f,o) -> let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in - let am = if simplIsCbn () then strong_cbn f else simpl in + let am = if simplIsCbn () then Cbn.norm_cbn f else simpl in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast) | Cbn f -> - (e_red (strong_cbn f), DEFAULTcast) + (e_red (Cbn.norm_cbn f), DEFAULTcast) | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) @@ -274,11 +271,14 @@ let reduction_of_red_expr env r = let error_illegal_clause () = CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.") +let error_multiple_patterns () = + CErrors.user_err Pp.(str "\"at\" clause in occurences not supported with multiple patterns or references.") + let error_illegal_non_atomic_clause () = CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.") -let error_occurrences_not_unsupported () = - CErrors.user_err Pp.(str "Occurrences not supported for this reduction tactic.") +let error_at_in_occurrences_not_supported () = + CErrors.user_err Pp.(str "\"at\" clause not supported for this reduction tactic.") let bind_red_expr_occurrences occs nbcl redexp = let open Locus in @@ -295,14 +295,14 @@ let bind_red_expr_occurrences occs nbcl redexp = else match redexp with | Unfold (_::_::_) -> - error_illegal_clause () + error_multiple_patterns () | Unfold [(occl,c)] -> if occl != AllOccurrences then error_illegal_clause () else Unfold [(occs,c)] | Pattern (_::_::_) -> - error_illegal_clause () + error_multiple_patterns () | Pattern [(occl,c)] -> if occl != AllOccurrences then error_illegal_clause () @@ -325,7 +325,7 @@ let bind_red_expr_occurrences occs nbcl redexp = CbvNative (Some (occs,c)) | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _ | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None -> - error_occurrences_not_unsupported () + error_at_in_occurrences_not_supported () | Unfold [] | Pattern [] -> assert false |