diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 9 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
2 files changed, 9 insertions, 2 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index af3227729e..e51415abb1 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -100,9 +100,16 @@ let is_ground_env evd env = | _ -> true in List.for_all is_ground_decl (rel_context env) && List.for_all is_ground_decl (named_context env) + (* Memoization is safe since evar_map and environ are applicative structures *) -let is_ground_env = memo1_2 is_ground_env +let memo f = + let m = ref None in + fun x y -> match !m with + | Some (x', y', r) when x == x' && y == y' -> r + | _ -> let r = f x y in m := Some (x, y, r); r + +let is_ground_env = memo is_ground_env (* Return the head evar if any *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 4062117b0f..de6873ba3d 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -82,7 +82,7 @@ let mis_is_recursive_subset listind rarg = Array.exists one_is_rec (dest_subterms rarg) let mis_is_recursive (ind,mib,mip) = - mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1)) + mis_is_recursive_subset (List.interval 0 (mib.mind_ntypes - 1)) mip.mind_recargs let mis_nf_constructor_type (ind,mib,mip) j = |