diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index feb3bf018..52d5c9c91 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -188,7 +188,7 @@ let is_reversible_pattern bound depth f l = (* Precondition: rels in env are for inductive types only *) let add_free_rels_until strict strongly_strict revpat bound env m pos acc = let rec frec rig (env,depth as ed) c = - let hd = if strict then whd_betadeltaiota env c else c in + let hd = if strict then whd_all env c else c in let c = if strongly_strict then hd else c in match kind_of_term hd with | Rel n when (n < bound+depth) && (n >= depth) -> @@ -236,7 +236,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rigid = ref true in let open Context.Rel.Declaration in let rec aux env avoid n names t = - let t = whd_betadeltaiota env t in + let t = whd_all env t in match kind_of_term t with | Prod (na,a,b) -> let na',avoid' = find_displayed_name_in all avoid na (names,b) in @@ -250,7 +250,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = add_free_rels_until strict strongly_strict revpat n env t Conclusion v else v in - match kind_of_term (whd_betadeltaiota env t) with + match kind_of_term (whd_all env t) with | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all [] na ([],b) in let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in |