diff options
Diffstat (limited to 'parsing/search.ml')
| -rw-r--r-- | parsing/search.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/search.ml b/parsing/search.ml index 78e549e13..e1723a1d1 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -56,7 +56,7 @@ let crible (fn : global_reference -> env -> constr -> unit) ref = match object_tag lobj with | "VARIABLE" -> (try - let ((idc,_,typ),_) = get_variable (basename sp) in + let (idc,_,typ) = get_variable (basename sp) in if (head_const typ) = const then fn (VarRef idc) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" |