aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli2
-rw-r--r--plugins/Derive/g_derive.ml42
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--stm/stm.ml28
-rw-r--r--stm/vernac_classifier.ml13
-rw-r--r--tactics/g_rewrite.ml44
-rw-r--r--toplevel/g_obligations.ml42
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) ] ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 14:42:06 +0000