diff options
| author | Gaëtan Gilbert | 2020-02-06 17:11:07 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 53cabaf1e26bfc13e5a45dfeb90ad6a858344c32 (patch) | |
| tree | e38575cd92b44ce331f0532a5c89dcb387d4e750 | |
| parent | c38e60243a3cee5d23c76fd78362b7c352c3d8ca (diff) | |
unsafe_type_of -> get_type_of in Equality.build_injrec
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 0eb0a30486..de7e755e5a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1311,7 +1311,7 @@ let make_iterated_tuple env sigma dflt (z,zty) = sigma, (tuple,tuplety,dfltval) let rec build_injrec env sigma dflt c = function - | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c) + | [] -> make_iterated_tuple env sigma dflt (c,get_type_of env sigma c) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in |