diff options
| author | Arnaud Spiwack | 2014-09-08 12:52:05 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-12-12 16:08:44 +0100 |
| commit | 724797b1f0e7051a52f30ff0cc432db2cc9345ec (patch) | |
| tree | 66038674337785c918a71941d38c19bd62323083 /tactics | |
| parent | a417d138c0a8abc028486c20d59e4f2e82f456ef (diff) | |
Extend the syntax of simpl with a delta flag.
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 |
4 files changed, 11 insertions, 8 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 93768c10ac..4f23e35204 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -210,7 +210,7 @@ let initial_atomic () = let () = List.iter iter [ "red", TacReduce(Red false,nocl); "hnf", TacReduce(Hnf,nocl); - "simpl", TacReduce(Simpl None,nocl); + "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl); "compute", TacReduce(Cbv Redops.all_flags,nocl); "intro", TacIntroMove(None,MoveLast); "intros", TacIntroPattern []; diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 48f5c65ff9..7d609e1a53 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -399,7 +399,9 @@ let intern_red_expr ist = function | Cbn f -> Cbn (intern_flag ist f) | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) - | Simpl o -> Simpl (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) + | Simpl (f,o) -> + Simpl (intern_flag ist f, + Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c76c28dbfc..e774316a66 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -710,8 +710,9 @@ let interp_red_expr ist env sigma = function (fun c sigma -> interp_constr_with_occurrences ist env sigma c) l sigma in sigma , Pattern l_interp - | Simpl o -> - sigma , Simpl (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) + | Simpl (f,o) -> + sigma , Simpl (interp_flag ist env sigma f, + Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) | CbvVm o -> sigma , CbvVm (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) | CbvNative o -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3a0baf2946..40228c4df5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -467,7 +467,7 @@ let bind_red_expr_occurrences occs nbcl redexp = let has_at_clause = function | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l - | Simpl (Some (occl,_)) -> occl != AllOccurrences + | Simpl (_,Some (occl,_)) -> occl != AllOccurrences | _ -> false in if occs == AllOccurrences then if nbcl > 1 && has_at_clause redexp then @@ -490,11 +490,11 @@ let bind_red_expr_occurrences occs nbcl redexp = error_illegal_clause () else Pattern [(occs,c)] - | Simpl (Some (occl,c)) -> + | Simpl (f,Some (occl,c)) -> if occl != AllOccurrences then error_illegal_clause () else - Simpl (Some (occs,c)) + Simpl (f,Some (occs,c)) | CbvVm (Some (occl,c)) -> if occl != AllOccurrences then error_illegal_clause () @@ -506,7 +506,7 @@ let bind_red_expr_occurrences occs nbcl redexp = else CbvNative (Some (occs,c)) | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _ - | ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None | CbvNative None -> + | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None -> error_occurrences_not_unsupported () | Unfold [] | Pattern [] -> assert false |