diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/indschemes.ml | 7 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
2 files changed, 1 insertions, 8 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 779926a7d7..41c44b126d 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -61,13 +61,6 @@ let _ = optkey = ["Nonrecursive";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; optwrite = (fun b -> bifinite_elim_flag := b) } -let _ = - declare_bool_option - { optdepr = true; (* compatibility 2014-09-03*) - optname = "automatic declaration of induction schemes for non-recursive types"; - optkey = ["Record";"Elimination";"Schemes"]; - optread = (fun () -> !bifinite_elim_flag) ; - optwrite = (fun b -> bifinite_elim_flag := b) } let case_flag = ref false let _ = diff --git a/vernac/record.ml b/vernac/record.ml index 1991a8640a..e21f53f55e 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -124,7 +124,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = match t with | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in - let sred = Reductionops.whd_all env sigma s in + let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with | Sort s' -> let s' = EConstr.ESorts.kind sigma s' in |