poly: remove unused attribute to STM nodes and vernac classificaiton

7 files changed, 27 insertions, 26 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 0b2e55941..335e04b91 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -448,7 +448,7 @@ type vernac_type =
   | VtStm of vernac_control * vernac_part_of_script
   | VtUnknown
 and vernac_qed_type = VtKeep | VtDrop (* Qed/Admitted, Abort *)
-and vernac_start = string * opacity_guarantee * Id.t list * polymorphic
+and vernac_start = string * opacity_guarantee * Id.t list
 and vernac_sideff_type = Id.t list
 and vernac_is_alias = bool
 and vernac_part_of_script = bool
diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4
index c7db26fb8..9137c3d28 100644
--- a/plugins/Derive/g_derive.ml4
+++ b/plugins/Derive/g_derive.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
-let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[], false),VtLater)
+let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command
 | [ "Derive" ident(f) "From" constr(init) "Upto" constr(r) "As" ident(lemma) ] ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 21d0b9f3d..d77385321 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -165,7 +165,7 @@ VERNAC COMMAND EXTEND Function
              (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
-             Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids, false), VtLater)
+             Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
          | x -> x ]
     -> [ do_generate_principle false (List.map snd recsl) ]
 END
diff --git a/stm/stm.ml b/stm/stm.ml
index 0136e5210..dcb1de3fb 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -79,7 +79,7 @@ type branch_type =
   | `Proof of proof_mode * depth
   | `Edit of proof_mode * Stateid.t * Stateid.t ]
 type cmd_t = ast * Id.t list
-type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list * Decl_kinds.polymorphic
+type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
 type qed_t = {
   qast : ast;
   keep : vernac_qed_type;
@@ -245,7 +245,7 @@ end = struct
   let print_dag vcs () =
     let fname = "stm_" ^ process_id () in
     let string_of_transaction = function
-      | Cmd (t, _) | Fork (t, _,_,_,_) ->
+      | Cmd (t, _) | Fork (t, _,_,_) ->
           (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
       | Sideff (Some t) ->
           sprintf "Sideff(%s)"
@@ -777,7 +777,7 @@ end = struct
           | Some (_, cur) ->
               match VCS.visit cur with
               | { step = `Cmd ( { loc }, _) } 
-              | { step = `Fork ( { loc }, _, _, _, _) } 
+              | { step = `Fork ( { loc }, _, _, _) } 
               | { step = `Qed ( { qast = { loc } }, _) } 
               | { step = `Sideff (`Ast ( { loc }, _)) } ->
                   let start, stop = Loc.unloc loc in
@@ -1182,11 +1182,11 @@ let collect_proof cur hd brkind id =
     match last, view.step with
     | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next
     | _, `Alias _ -> `Sync (no_name,`Alias)
-    | _, `Fork(_,_,_,_::_::_,_)-> `Sync (no_name,`MutualProofs)
-    | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_,_) ->
+    | _, `Fork(_,_,_,_::_::_)-> `Sync (no_name,`MutualProofs)
+    | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) ->
         `Sync (no_name,`Doesn'tGuaranteeOpacity)
     | Some (parent, ({ expr = VernacProof(_,Some _)} as v)),
-      `Fork (_, hd', GuaranteesOpacity, ids,_) ->
+      `Fork (_, hd', GuaranteesOpacity, ids) ->
         let name = name ids in
         let time = get_hint_bp_time name in
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
@@ -1194,7 +1194,7 @@ let collect_proof cur hd brkind id =
         then `ASync (parent,Some v,accn,name)
         else `Sync (name,`Policy)
     | Some (parent, ({ expr = VernacProof(t,None)} as v)),
-      `Fork (_, hd', GuaranteesOpacity, ids, _) when
+      `Fork (_, hd', GuaranteesOpacity, ids) when
        not (State.is_cached parent) &&
        !Flags.compilation_mode = Flags.BuildVi ->
         (try
@@ -1206,7 +1206,7 @@ let collect_proof cur hd brkind id =
           then `ASync (parent,Some v,accn,name)
           else `Sync (name,`Policy)
         with Not_found -> `Sync (no_name,`NoHint))
-    | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids, _) ->
+    | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
         let time = get_hint_bp_time name in
@@ -1274,7 +1274,7 @@ let known_state ?(redefine_qed=false) ~cache id =
       | `Cmd (x,_) -> (fun () ->
             reach view.next; vernac_interp id x
           ), cache
-      | `Fork (x,_,_,_,_) -> (fun () ->
+      | `Fork (x,_,_,_) -> (fun () ->
             reach view.next; vernac_interp id x;
             wall_clock_last_fork := Unix.gettimeofday ()
           ), `Yes
@@ -1422,7 +1422,7 @@ end = struct
         let ids =
           if id = Stateid.initial || id = Stateid.dummy then [] else
           match VCS.visit id with
-          | { step = `Fork (_,_,_,l,_) } -> l
+          | { step = `Fork (_,_,_,l) } -> l
           | { step = `Cmd (_,l) } -> l
           | _ -> [] in
         match f acc (id, vcs, ids) with
@@ -1712,11 +1712,11 @@ let process_transaction ~tty verbose c (loc, expr) =
           anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
 
       (* Proof *)
-      | VtStartProof (mode, guarantee, names, poly), w ->
+      | VtStartProof (mode, guarantee, names), w ->
           let id = VCS.new_node () in
           let bname = VCS.mk_branch_name x in
           VCS.checkout VCS.Branch.master;
-          VCS.commit id (Fork (x, bname, guarantee, names, poly));
+          VCS.commit id (Fork (x, bname, guarantee, names));
           VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
           Proof_global.activate_proof_mode mode;
           Backtrack.record (); if w == VtNow then finish (); `Ok
@@ -1773,7 +1773,7 @@ let process_transaction ~tty verbose c (loc, expr) =
                Proof_global.there_are_pending_proofs ()
             then begin
               let bname = VCS.mk_branch_name x in
-              VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[],false));
+              VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[]));
               VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
               Proof_global.activate_proof_mode "Classic";
             end else begin
@@ -1995,7 +1995,7 @@ let get_script prf =
        Stateid.equal id Stateid.dummy then acc else
     let view = VCS.visit id in
     match view.step with
-    | `Fork (_,_,_,ns,_) when test ns -> acc
+    | `Fork (_,_,_,ns) when test ns -> acc
     | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
     | `Sideff (`Ast (x,_)) ->
          find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f51f5d2a0..8ba01a7b2 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -48,7 +48,8 @@ let elide_part_of_script_and_now (a, _) =
 
 let make_polymorphic (a, b as x) =
   match a with
-  | VtStartProof (x, _, ids, _) -> (VtStartProof (x, Doesn'tGuaranteeOpacity, ids, true), b)
+  | VtStartProof (x, _, ids) ->
+      VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
   | _ -> x
 
 let undo_classifier = ref (fun _ -> assert false)
@@ -103,23 +104,23 @@ let rec classify_vernac e =
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
     | VernacDefinition (_,(_,i),ProveBody _) ->
-        VtStartProof("Classic",GuaranteesOpacity,[i], false), VtLater
+        VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
     | VernacStartTheoremProof (_,l,_) ->
         let ids = 
           CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
-        VtStartProof ("Classic",GuaranteesOpacity,ids, false), VtLater
-    | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[],false), VtLater
+        VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+    | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
     | VernacFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
-        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids, false), VtLater
+        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
-        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids,false), VtLater
+        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 27233ea57..b715be9e6 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -256,11 +256,11 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
     => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ]
     -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
-    => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n], false), VtLater) ]
+    => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
     -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ]
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
-    => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n], false), VtLater) ]
+    => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
     -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ]
 END
 
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index 061f7ba5d..2354aa332 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -54,7 +54,7 @@ GEXTEND Gram
 
 open Obligations
 
-let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[],false), VtLater)
+let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater)
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
 | [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] ->