aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli5
-rw-r--r--parsing/g_obligations.ml42
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--tactics/g_rewrite.ml44
-rw-r--r--toplevel/stm.ml24
-rw-r--r--toplevel/vernac_classifier.ml10
6 files changed, 26 insertions, 21 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index d1ed1d4abb..4f666a8014 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -441,7 +441,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 * Id.t list
+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
@@ -453,6 +453,9 @@ and vernac_control =
| VtObserve of Stateid.t
| VtBack of Stateid.t
| VtPG
+and opacity_guarantee =
+ | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
+ | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
type vernac_when =
| VtNow
| VtLater
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index a0d4771f13..fe024d409d 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -60,7 +60,7 @@ let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
open Obligations
-let classify_obbl _ = Vernacexpr.VtStartProof ("Classic",[]), Vernacexpr.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) ] ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index b317cec0d5..3e4f67498f 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -167,7 +167,7 @@ VERNAC COMMAND EXTEND Function
(Vernacexpr.VernacFixpoint(None, List.map snd recsl))
with
| Vernacexpr.VtSideff ids, _ when hard ->
- Vernacexpr.VtStartProof ("Classic", ids), Vernacexpr.VtLater
+ Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
| x -> x ]
-> [ do_generate_principle false (List.map snd recsl) ]
END
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 846bba1d46..31defcafb3 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -244,11 +244,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",[n]), Vernacexpr.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",[n]), Vernacexpr.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/stm.ml b/toplevel/stm.ml
index 0730c08ee4..d8f9052563 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -67,7 +67,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 * Id.t list
+type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
type qed_t = {
qast : ast;
keep : vernac_qed_type;
@@ -232,7 +232,7 @@ end = struct (* {{{ *)
let print_dag vcs () = (* {{{ *)
let fname = "stm" ^ string_of_int (max 0 !Flags.coq_slave_mode) 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)"
@@ -1014,13 +1014,14 @@ let collect_proof cur hd id =
match last, view.step with
| _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next
| _, `Alias _ -> `NotOptimizable `Alias
- | _, `Fork(_,_,_::_::_)->
+ | _, `Fork(_,_,_,_::_::_)->
`NotOptimizable `MutualProofs (* TODO: enderstand where we need that *)
- | Some (parent, (_,_,VernacProof(_,Some _) as v)), `Fork (_, hd', ids) ->
+ | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) -> `NotOptimizable `Doesn'tGuaranteeOpacity
+ | Some (parent, (_,_,VernacProof(_,Some _) as v)), `Fork (_, hd', GuaranteesOpacity, ids) ->
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
if delegate_policy_check accn then `Optimizable (parent,Some v,accn,ids)
else `NotOptimizable `TooShort
- | Some (parent, _), `Fork (_, hd', ids) ->
+ | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) ->
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
if delegate_policy_check accn then `MaybeOptimizable (parent, accn,ids)
else `NotOptimizable `TooShort
@@ -1042,6 +1043,7 @@ let string_of_reason = function
| `NestedProof -> "NestedProof"
| `Immediate -> "Immediate"
| `Alias -> "Alias"
+ | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity"
| _ -> "Unknown Reason"
let known_state ?(redefine_qed=false) ~cache id =
@@ -1075,7 +1077,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
), `Yes
| `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
@@ -1212,7 +1214,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
@@ -1470,11 +1472,11 @@ let process_transaction ~tty verbose c (loc, expr) =
anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
(* Proof *)
- | VtStartProof (mode, names), 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, names));
+ 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
@@ -1531,7 +1533,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,[]));
+ 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
@@ -1742,7 +1744,7 @@ let get_script prf =
if Stateid.equal id Stateid.initial || Stateid.equal id Stateid.dummy then acc else
let view = VCS.visit id in
match view.step with
- | `Fork (_,_,ns) when List.mem prf ns -> acc
+ | `Fork (_,_,_,ns) when List.mem prf ns -> acc
| `Qed (qed, proof) -> find [pi3 qed.qast, (VCS.get_info id).n_goals] proof
| `Sideff (`Ast (x,_)) ->
find ((pi3 x, (VCS.get_info id).n_goals)::acc) view.next
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml
index 2e04d14302..4ef157a64a 100644
--- a/toplevel/vernac_classifier.ml
+++ b/toplevel/vernac_classifier.ml
@@ -94,23 +94,23 @@ let rec classify_vernac e =
| VernacSolveExistential _ -> VtProofStep, VtLater
(* StartProof *)
| VernacDefinition (_,(_,i),ProveBody _) ->
- VtStartProof("Classic",[i]), VtLater
+ VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
| VernacStartTheoremProof (_,l,_) ->
let ids =
CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
- VtStartProof ("Classic", ids), VtLater
- | VernacGoal _ -> VtStartProof ("Classic",[]), 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",ids), 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",ids), 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) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 11:27:00 +0000