diff options
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 44beaa3ee..c033b4c88 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -329,6 +329,9 @@ Module Compilers. constr:(type_primitive rt) end. + Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing). + Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing). + Module Export Notations. Export Coercions. Delimit Scope ctype_scope with ctype. |