diff options
| author | Pierre-Marie Pédrot | 2017-08-18 17:59:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-24 14:47:47 +0200 |
| commit | 0232b0de849998d3394a4e6a2ab6232a75897610 (patch) | |
| tree | 7c7d440f32775a1b394fff638abe78bb7e77a832 /theories | |
| parent | 0b2c0e58b45b2e78f8ad65ddbc7254e1fd9d07eb (diff) | |
Use references in reduction tactics.
We dynamically check that the provided references are indeed evaluable
ones, instead of ensuring this at internalization time.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Std.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/theories/Std.v b/theories/Std.v index 43ccb06192..dd81835c40 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -34,9 +34,11 @@ Ltac2 Type clause := { on_concl : occurrences; }. -Ltac2 Type evaluable_reference := [ -| EvalVarRef (ident) -| EvalConstRef (constant) +Ltac2 Type reference := [ +| VarRef (ident) +| ConstRef (constant) +| IndRef (inductive) +| ConstructRef (constructor) ]. Ltac2 Type red_flags := { @@ -46,7 +48,7 @@ Ltac2 Type red_flags := { rCofix : bool; rZeta : bool; rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) - rConst : evaluable_reference list + rConst : reference list }. Ltac2 Type 'a not_implemented. @@ -134,7 +136,7 @@ Ltac2 @ external simpl : red_flags -> (pattern * occurrences) option -> clause - 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 unfold : (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". |