diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bd66561dd..6fb962f2c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -265,7 +265,7 @@ let case_sign ity i = | [] -> acc | (c::rest) -> analrec (false::acc) rest in - let recarg = mis_recarg (lookup_mind_specif ity (Global.unsafe_env())) in + let recarg = mis_recarg (lookup_mind_specif ity (Global.env())) in analrec [] recarg.(i-1) let elim_sign ity i = @@ -277,7 +277,7 @@ let elim_sign ity i = | (Mrec k::rest) -> analrec ((j=k)::acc) rest | [] -> List.rev acc in - let recarg = mis_recarg (lookup_mind_specif ity (Global.unsafe_env())) in + let recarg = mis_recarg (lookup_mind_specif ity (Global.env())) in analrec [] recarg.(i-1) let sort_of_goal gl = |