Add notations for type reification

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.