From a93104d5462894d5d0651aa2e04e12c311eb5897 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 3 Sep 2014 18:16:21 +0200
Subject: Remove [Infer] option of records.

Dead code formerly used by the now defunct [autoinstances].---
 intf/vernacexpr.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'intf')

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
-- 
cgit v1.2.3