File tree Expand file tree Collapse file tree 1 file changed +7
-7
lines changed
Expand file tree Collapse file tree 1 file changed +7
-7
lines changed Original file line number Diff line number Diff line change 1- From MetaCoq .Template Require Import All .
2- Import MCMonadNotation .
1+ From MetaRocq .Template Require Import All .
2+ Import MRMonadNotation .
33
44(* Unquoting evars. *)
5- MetaCoq Run (mlet t <- tmUnquote (tEvar fresh_evar_id []) ;; tmPrint t).
6- MetaCoq Run (mlet t <- tmUnquoteTyped nat (tEvar fresh_evar_id []) ;; tmPrint t).
5+ MetaRocq Run (mlet t <- tmUnquote (tEvar fresh_evar_id []) ;; tmPrint t).
6+ MetaRocq Run (mlet t <- tmUnquoteTyped nat (tEvar fresh_evar_id []) ;; tmPrint t).
77
88(* Unquoting evars, with typeclass resolution. *)
99Existing Class nat.
1010Existing Instance O.
1111
12- MetaCoq Quote Definition quoted_nat := nat.
13- MetaCoq Run (
12+ MetaRocq Quote Definition quoted_nat := nat.
13+ MetaRocq Run (
1414 mlet t <- tmUnquote (tCast (tEvar fresh_evar_id []) Cast quoted_nat) ;;
1515 tmEval cbv t
1616).
17- MetaCoq Run (
17+ MetaRocq Run (
1818 mlet t <- tmUnquoteTyped nat (tEvar fresh_evar_id []) ;;
1919 tmEval cbv t
2020).
You can’t perform that action at this time.
0 commit comments