diff options
| author | Pierre-Marie Pédrot | 2018-09-28 18:55:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-06 14:51:54 +0200 |
| commit | 45e14bdb854fe5da40c2ed1d9ca575ae8d435d36 (patch) | |
| tree | 7bc43cb8e9561e1355ad99ddd0f10004e1bdf7d4 /pretyping/unification.ml | |
| parent | 2089207415565e8a28816f53b61d9292d04f4c59 (diff) | |
Use lists instead of arrays in evar instances.
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 90dde01915..11163d6ede 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -82,7 +82,7 @@ let occur_meta_or_undefined_evar evd c = | Evar (ev,args) -> (match evar_body (Evd.find evd ev) with | Evar_defined c -> - occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args + occrec (EConstr.Unsafe.to_constr c); List.iter occrec args | Evar_empty -> raise Occur) | _ -> Constr.iter occrec c in try occrec c; false with Occur | Not_found -> true @@ -144,9 +144,9 @@ let abstract_list_all env evd typ c l = error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in evd,(p,typp) -let set_occurrences_of_last_arg args = +let set_occurrences_of_last_arg n = Evarconv.AtOccurrences AllOccurrences :: - List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified Abstraction.Abstract) args) + List.tl (List.init n (fun _ -> Evarconv.Unspecified Abstraction.Abstract)) let occurrence_test _ _ _ env sigma _ c1 c2 = match EConstr.eq_constr_universes env sigma c1 c2 with @@ -159,7 +159,8 @@ let abstract_list_all_with_dependencies env evd typ c l = let (evd, ev) = new_evar env evd typ in let evd,ev' = evar_absorb_arguments env evd (destEvar evd ev) l in let n = List.length l in - let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in + let () = assert (n <= List.length (snd ev')) in + let argoccs = set_occurrences_of_last_arg n in let evd,b = Evarconv.second_order_matching (Evarconv.default_flags_of TransparentState.empty) @@ -629,7 +630,7 @@ let subst_defined_metas_evars sigma (bl,el) c = substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl))) | Evar (evk,args) -> let eq c1 c2 = Constr.equal c1 (EConstr.Unsafe.to_constr c2) in - let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.for_all2 eq args args' in + let select (_,(evk',args'),_) = Evar.equal evk evk' && List.for_all2 eq args args' in (try substrec (EConstr.Unsafe.to_constr (pi3 (List.find select el))) with Not_found -> Constr.map substrec c) | _ -> Constr.map substrec c |