Remove [Infer] option of records.

Dead code formerly used by the now defunct [autoinstances].

8 files changed, 22 insertions, 27 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 7f3417443..37048005f 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
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3437256ed..f7f049884 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -200,7 +200,7 @@ GEXTEND Gram
         indl = LIST1 inductive_definition SEP "with" ->
 	  let (k,f) = f in
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
-          VernacInductive (priv,f,false,indl)
+          VernacInductive (priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (None, recs)
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -222,13 +222,13 @@ GEXTEND Gram
 
   gallina_ext:
     [ [ priv = private_token; 
-	b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
+	b = record_token; oc = opt_coercion; name = identref;
         ps = binders;
 	s = OPT [ ":"; s = lconstr -> s ];
 	cfs = [ ":="; l = constructor_list_or_record_decl -> l
 	  | -> RecordDecl (None, []) ] ->
 	  let (recf,indf) = b in
-	    VernacInductive (priv,indf,infer,[((oc,name),ps,s,recf,cfs),[]])
+	    VernacInductive (priv,indf,[((oc,name),ps,s,recf,cfs),[]])
   ] ]
   ;
   thm_token:
@@ -272,9 +272,6 @@ GEXTEND Gram
       | "CoInductive" -> (CoInductive,CoFinite)
       | "Variant" -> (Variant,BiFinite) ] ]
   ;
-  infer_token:
-    [ [ IDENT "Infer" -> true | -> false ] ]
-  ;
   private_token:
     [ [ IDENT "Private" -> true | -> false ] ]
   ;
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 507ba1970..2ef3c34ed 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1416,7 +1416,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,false,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1431,7 +1431,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,false,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    Errors.print reraise
 	in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 514017d45..5ef7eb710 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -623,7 +623,7 @@ let rec pr_vernac = function
       hov 2
         (pr_assumption_token (n > 1) stre ++ spc() ++
         pr_ne_params_list pr_lconstr_expr l)
-  | VernacInductive (p,f,i,l) ->
+  | VernacInductive (p,f,l) ->
       let pr_constructor (coe,(id,c)) =
         hov 2 (pr_lident id ++ str" " ++
                (if coe then str":>" else str":") ++
@@ -641,7 +641,6 @@ let rec pr_vernac = function
       let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
 	hov 0 (
 	    str key ++ spc() ++
-	      (if i then str"Infer " else str"") ++
               (if coe then str"> " else str"") ++ pr_lident id ++
               pr_and_type_binders_arg indpar ++ spc() ++
 	      Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 5bbd857d9..ce9c2b3ff 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -134,7 +134,7 @@ let rec classify_vernac e =
         let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
         VtSideff ids, VtLater    
     | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
-    | VernacInductive (_,_,_,l) ->
+    | VernacInductive (_,_,l) ->
         let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 56e8c1492..f3565a721 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -319,7 +319,7 @@ let structure_signature ctx =
 
 open Typeclasses
 
-let declare_structure finite infer poly ctx id idbuild paramimpls params arity fieldimpls fields
+let declare_structure finite poly ctx id idbuild paramimpls params arity fieldimpls fields
     ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
   let args = Termops.extended_rel_list nfields params in
@@ -357,7 +357,7 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map pi1 ctx)))
 
-let declare_class finite def infer poly ctx id idbuild paramimpls params arity fieldimpls fields
+let declare_class finite def poly ctx id idbuild paramimpls params arity fieldimpls fields
     ?(kind=StructureComponent) ?name is_coe coers priorities sign =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -399,7 +399,7 @@ let declare_class finite def infer poly ctx id idbuild paramimpls params arity f
 	  cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
 	let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
-	let ind = declare_structure BiFinite infer poly ctx (snd id) idbuild paramimpls
+	let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
 	  params arity fieldimpls fields
 	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
 	in
@@ -434,7 +434,7 @@ open Vernacexpr
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions 
    or subinstances *)
-let definition_structure (kind,poly,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let cfs,priorities = List.split cfs in
   let coers,fs = List.split cfs in
@@ -455,14 +455,14 @@ let definition_structure (kind,poly,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,i
   let sign = structure_signature (fields@params) in
     match kind with
     | Class def ->
-	let gr = declare_class finite def infer poly ctx (loc,idstruc) idbuild
+	let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
 	  implpars params arity implfs fields is_coe coers priorities sign in
 	gr
     | _ ->
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite infer poly ctx idstruc 
+	let ind = declare_structure finite poly ctx idstruc 
 	  idbuild implpars params arity implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index dac8636cb..873e1ff0c 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -26,7 +26,7 @@ val declare_projections :
   (Name.t * bool) list * constant option list
 
 val declare_structure : Decl_kinds.recursivity_kind ->
-  bool (**infer?*) -> bool (** polymorphic?*) -> Univ.universe_context ->
+  bool (** polymorphic?*) -> Univ.universe_context ->
   Id.t -> Id.t ->
   manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
   Impargs.manual_explicitation list list -> rel_context -> (** fields *)
@@ -37,6 +37,6 @@ val declare_structure : Decl_kinds.recursivity_kind ->
   inductive
 
 val definition_structure :
-  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
+  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * lident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a5803a24d..adfccb502 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -512,7 +512,7 @@ let vernac_assumption locality poly (local, kind) l nl =
   let status = do_assumptions kind nl l in
   if not status then Pp.feedback Feedback.AddedAxiom
 
-let vernac_record k poly finite infer struc binders sort nameopt cfs =
+let vernac_record k poly finite struc binders sort nameopt cfs =
   let const = match nameopt with
     | None -> add_prefix "Build_" (snd (snd struc))
     | Some (_,id as lid) ->
@@ -523,9 +523,9 @@ let vernac_record k poly finite infer struc binders sort nameopt cfs =
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure (k,poly,finite,infer,struc,binders,cfs,const,sort))
+    ignore(Record.definition_structure (k,poly,finite,struc,binders,cfs,const,sort))
 
-let vernac_inductive poly lo finite infer indl =
+let vernac_inductive poly lo finite indl =
   if Dumpglob.dump () then
     List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
       match cstrs with
@@ -542,13 +542,13 @@ let vernac_inductive poly lo finite infer indl =
       Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
       vernac_record (match b with Class true -> Class false | _ -> b)
-	poly finite infer id bl c oc fs
+	poly finite id bl c oc fs
   | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
       let f =
 	let (coe, ((loc, id), ce)) = l in
 	let coe' = if coe then Some true else None in
 	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
-      in vernac_record (Class true) poly finite infer id bl c None [f]
+      in vernac_record (Class true) poly finite id bl c None [f]
   | [ ( id , bl , c , Class true, _), _ ] ->
       Errors.error "Definitional classes must have a single method"
   | [ ( id , bl , c , Class false, Constructors _), _ ] ->
@@ -1774,7 +1774,7 @@ let interp ?proof locality poly c =
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
-  | VernacInductive (priv,finite,infer,l) -> vernac_inductive poly priv finite infer l
+  | VernacInductive (priv,finite,l) -> vernac_inductive poly priv finite l
   | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
   | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
   | VernacScheme l -> vernac_scheme l