Remove the need for coercions in well-typing of Reify

2 files changed, 6 insertions, 13 deletions

diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v
index d74dd673a..e202cc804 100644
--- a/src/Reflection/Reify.v
+++ b/src/Reflection/Reify.v
@@ -2,20 +2,12 @@
 (** The reification procedure goes through [InputSyntax], which allows
     judgmental equality of the denotation of the reified term. *)
 Require Import Coq.Strings.String.
-Require Crypto.Reflection.Syntax.
-Require Crypto.Reflection.InputSyntax.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.InputSyntax.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 
-Module Export ReifyCoercions.
-  Global Coercion Syntax.Return : Syntax.exprf >-> Syntax.expr.
-  Global Coercion InputSyntax.Return : InputSyntax.exprf >-> InputSyntax.expr.
-  Global Coercion Syntax.Tflat : Syntax.flat_type >-> Syntax.type.
-End ReifyCoercions.
-
-Import Syntax InputSyntax.
-
 Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T.
 Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False.
 Arguments reify_var_for_in_is _ {T} _ _ {eT} _.
@@ -224,7 +216,8 @@ Ltac reify_abs base_type_code interp_base_type op var e :=
                         (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *)
     with fun _ v _ => @?C v => mkAbs t C end
   | ?x =>
-    reifyf_term x
+    let ret := reifyf_term x in
+    constr:(Return ret)
   end.
 
 Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e)
diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v
index 457c9fcfe..fd60e7906 100644
--- a/src/Reflection/TestCase.v
+++ b/src/Reflection/TestCase.v
@@ -40,9 +40,9 @@ Ltac Reify_rhs := Reify.Reify_rhs base_type interp_base_type op interp_op.
 Goal (flat_type base_type -> Type) -> False.
   intro var.
   let x := reifyf base_type interp_base_type op var 1%nat in pose x.
-  let x := Reify' 1%nat in unify x (fun var => Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1).
+  let x := Reify' 1%nat in unify x (fun var => Return (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)).
   let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x.
-  let x := Reify' (1 + 1)%nat in unify x (fun var => Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1))).
+  let x := Reify' (1 + 1)%nat in unify x (fun var => Return (Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))).
   let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x.
   let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))).
   let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x.