diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f4c3a1bb4..90492d50c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -505,7 +505,7 @@ let expand_alias_once aliases x = | [] -> None | l -> Some (list_last l) -let rec expansions_of_var aliases x = +let expansions_of_var aliases x = match get_alias_chain_of aliases x with | [] -> [x] | a::_ as l when isRel a || isVar a -> x :: List.rev l @@ -689,7 +689,7 @@ module Constrhash = Hashtbl.Make let hash = hash_constr end) -let rec constr_list_distinct l = +let constr_list_distinct l = let visited = Constrhash.create 23 in let rec loop = function | h::t -> |