From 87b510e5b0f363724eae5db9f177f167a3586015 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Mar 2014 18:26:26 +0100
Subject: Fixing pervasive comparisons

---
 interp/notation_ops.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 57fc15f8e2..bd61ba28fc 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -512,12 +512,6 @@ let rec alpha_var id1 id2 = function
   | _::idl -> alpha_var id1 id2 idl
   | [] -> Id.equal id1 id2
 
-let compare_var v1 v2 =
-  match v1, v2 with
-  | GHole _, _ -> (true,true)
-  | _, GHole _ -> (false,false)
-  | _, _ -> (true,Pervasives.(=) v1 v2 (** FIXME *))
-
 let add_env alp (sigma,sigmalist,sigmabinders) var v =
   (* Check that no capture of binding variables occur *)
   if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match;
-- 
cgit v1.2.3