From 6ceaf0176b2a61cd2ed7b358af1e34349a8041ce Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 19 May 2017 21:14:36 +0200
Subject: Moving "sym" on "eq" type to lib/util.ml.

---
 engine/eConstr.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'engine/eConstr.ml')

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
-- 
cgit v1.2.3