diff options
| author | Pierre-Marie Pédrot | 2017-08-05 15:42:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-05 16:21:40 +0200 |
| commit | 6e6f348958cc333040991ca3dc2525a7c91dc9c0 (patch) | |
| tree | e8f2ce6df313f3e94c3525333d285f87d2178fde /theories | |
| parent | dbaf8dd6b150619ac04b33ae4d581432cb5cefe0 (diff) | |
Exporting more reduction functions.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Std.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/Std.v b/theories/Std.v index 695ea26444..43ccb06192 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -130,9 +130,15 @@ Ltac2 @ external induction : evar_flag -> induction_clause list -> Ltac2 @ external red : clause -> unit := "ltac2" "tac_red". Ltac2 @ external hnf : clause -> unit := "ltac2" "tac_hnf". +Ltac2 @ external simpl : red_flags -> (pattern * occurrences) option -> clause -> unit := "ltac2" "tac_simpl". Ltac2 @ external cbv : red_flags -> clause -> unit := "ltac2" "tac_cbv". Ltac2 @ external cbn : red_flags -> clause -> unit := "ltac2" "tac_cbn". Ltac2 @ external lazy : red_flags -> clause -> unit := "ltac2" "tac_lazy". +Ltac2 @ external unfold : (evaluable_reference * occurrences) list -> clause -> unit := "ltac2" "tac_unfold". +Ltac2 @ external fold : constr list -> clause -> unit := "ltac2" "tac_fold". +Ltac2 @ external pattern : (constr * occurrences) list -> clause -> unit := "ltac2" "tac_pattern". +Ltac2 @ external vm : (pattern * occurrences) option -> clause -> unit := "ltac2" "tac_vm". +Ltac2 @ external native : (pattern * occurrences) option -> clause -> unit := "ltac2" "tac_native". Ltac2 @ external rewrite : evar_flag -> rewriting list -> clause -> (unit -> unit) option -> unit := "ltac2" "tac_rewrite". |