diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 57fc15f8e..bd61ba28f 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; |