diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-09-17 18:43:54 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-09-17 18:54:45 -0400 |
| commit | 05f30d597443a6709d8df916e962f977a553c8ca (patch) | |
| tree | 19b2b2aacb9dc3cb3ddd6c1b147a730890966025 /src/Reflection/Reify.v | |
| parent | 1bacc083da890d7289f1ee54a41996db7a787a92 (diff) | |
Add reserved notation for Let, change #
We reserve [a # b] in Notations.v, and make it's level compatible with
the notation declared in the std lib for Q.
Diffstat (limited to 'src/Reflection/Reify.v')
| -rw-r--r-- | src/Reflection/Reify.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index e202cc804..19d3e9a5a 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -108,7 +108,7 @@ Ltac debug_leave_reify_rec e := Ltac reifyf base_type_code interp_base_type op var e := let reify_rec e := reifyf base_type_code interp_base_type op var e in - let mkLet ex eC := constr:(Let (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in + let mkLetIn ex eC := constr:(LetIn (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in let mkPair ex ey := constr:(Pair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex ey) in let mkVar T ex := constr:(Var (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in let mkConst T ex := constr:(Const (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in @@ -120,7 +120,7 @@ Ltac reifyf base_type_code interp_base_type op var e := | let x := ?ex in @?eC x => let ex := reify_rec ex in let eC := reify_rec eC in - mkLet ex eC + mkLetIn ex eC | pair ?a ?b => let a := reify_rec a in let b := reify_rec b in |