aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.ml')
-rw-r--r--engine/eConstr.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 54d3ce6cf..0771c8354 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -731,8 +731,6 @@ let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d
open Context
open Environ
-let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl
-
let cast_rel_decl :
type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt =
fun Refl x -> x