diff options
| author | Pierre-Marie Pédrot | 2014-03-01 18:26:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-01 22:45:39 +0100 |
| commit | 87b510e5b0f363724eae5db9f177f167a3586015 (patch) | |
| tree | 204c7ad1e1ba38945ab58d74e28d8cf67201fe71 /interp | |
| parent | bca756eaebf16b6145c65b53629219d2a0a8b1ba (diff) | |
Fixing pervasive comparisons
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 8 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 6 |
2 files changed, 7 insertions, 7 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index a9206b9338..867e233950 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -116,6 +116,12 @@ let normalize_scope sc = type scope_elem = Scope of scope_name | SingleNotation of string type scopes = scope_elem list +let scope_eq s1 s2 = match s1, s2 with +| Scope s1, Scope s2 +| SingleNotation s1, SingleNotation s2 -> String.equal s1 s2 +| Scope _, SingleNotation _ +| SingleNotation _, Scope _ -> false + let scope_stack = ref [] let current_scopes () = !scope_stack @@ -136,7 +142,7 @@ let open_scope i (_,(local,op,sc)) = in scope_stack := if op then sc :: !scope_stack - else List.except Pervasives.(=) sc !scope_stack (* FIXME *) + else List.except scope_eq sc !scope_stack let cache_scope o = open_scope 1 o 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; |