From 9330bf650ca602884c5c4c69c2fb3e94ee32838b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 14 Dec 2012 09:26:08 +0000
Subject: Implemented a full-fledged equality on [constr_expr]. By the way,
 some cleaning of the interface and moving of code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.mli | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 6e2c9e8832..28e7e2985f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -188,8 +188,3 @@ val parsing_explicit : bool ref
 
 (** Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
-
-(** Nothing to do here *)
-
-val explicitation_eq : explicitation -> explicitation -> bool
-
-- 
cgit v1.2.3