diff options
| author | Arnaud Spiwack | 2014-09-03 18:16:21 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-04 10:25:55 +0200 |
| commit | a93104d5462894d5d0651aa2e04e12c311eb5897 (patch) | |
| tree | 8619451aa37d699fc012f0e5f6509560d9c46726 /intf | |
| parent | 06e6a7b5a0d15f493a3f94fad905af2c44be9c09 (diff) | |
Remove [Infer] option of records.
Dead code formerly used by the now defunct [autoinstances].
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 7f3417443e..37048005fa 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -139,7 +139,6 @@ type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) type inductive_flag = Decl_kinds.recursivity_kind -type infer_flag = bool (* true = try to Infer record; false = nothing *) type onlyparsing_flag = Flags.compat_version option (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version @@ -298,7 +297,7 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * inline * simple_binder with_coercion list - | VernacInductive of private_flag * inductive_flag * infer_flag * (inductive_expr * decl_notation list) list + | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of |