aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/comSearch.ml9
-rw-r--r--vernac/declare.ml54
-rw-r--r--vernac/g_vernac.mlg2
-rw-r--r--vernac/ppvernac.ml1
-rw-r--r--vernac/search.ml21
-rw-r--r--vernac/search.mli2
-rw-r--r--vernac/vernac.mllib1
-rw-r--r--vernac/vernac_classifier.ml215
-rw-r--r--vernac/vernac_classifier.mli19
-rw-r--r--vernac/vernacentries.ml8
-rw-r--r--vernac/vernacexpr.ml1
-rw-r--r--vernac/vernacextend.ml2
-rw-r--r--vernac/vernacextend.mli2
-rw-r--r--vernac/vernacinterp.ml2
14 files changed, 246 insertions, 93 deletions
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index af51f4fafb..1b811f3db7 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -105,12 +105,6 @@ let () =
optread = (fun () -> !search_output_name_only);
optwrite = (:=) search_output_name_only }
-let deprecated_searchhead =
- CWarnings.create
- ~name:"deprecated-searchhead"
- ~category:"deprecated"
- (fun () -> Pp.str("SearchHead is deprecated. Use the headconcl: clause of Search instead."))
-
let interp_search env sigma s r =
let r = interp_search_restriction r in
let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in
@@ -138,9 +132,6 @@ let interp_search env sigma s r =
(Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
| SearchRewrite c ->
(Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
- | SearchHead c ->
- deprecated_searchhead ();
- (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
| Search sl ->
(Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |>
Search.prioritize_search) pr_search);
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c715304419..48aa329e5e 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -889,13 +889,6 @@ let add_hint local prg cst =
let locality = if local then Goptions.OptLocal else Goptions.OptExport in
Hints.add_hints ~locality [Id.to_string prg.prg_cinfo.CInfo.name] (unfold_entry cst)
-(* true = hide obligations *)
-let get_hide_obligations =
- Goptions.declare_bool_option_and_ref
- ~depr:true
- ~key:["Hide"; "Obligations"]
- ~value:false
-
let declare_obligation prg obl ~uctx ~types ~body =
let poly = prg.prg_info.Info.poly in
let univs = UState.univ_entry ~poly uctx in
@@ -1046,51 +1039,10 @@ let obligation_substitution expand prg =
let ints = intset_to (pred (Array.length obls)) in
obl_substitution expand obls ints
-let hide_obligation () =
- Coqlib.check_required_library ["Coq"; "Program"; "Tactics"];
- UnivGen.constr_of_monomorphic_global
- (Coqlib.lib_ref "program.tactics.obligation")
-
-(* XXX: Is this the right place? *)
-let rec prod_app t n =
- match
- Constr.kind
- (EConstr.Unsafe.to_constr
- (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t)))
- (* FIXME *)
- with
- | Prod (_, _, b) -> Vars.subst1 n b
- | LetIn (_, b, t, b') -> prod_app (Vars.subst1 b b') n
- | _ ->
- CErrors.user_err ~hdr:"prod_app"
- Pp.(str "Needed a product, but didn't find one" ++ fnl ())
-
-(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_applist t nL = List.fold_left prod_app t nL
-
-let replace_appvars subst =
- let rec aux c =
- let f, l = decompose_app c in
- if isVar f then
- try
- let c' = List.map (Constr.map aux) l in
- let t, b = Id.List.assoc (destVar f) subst in
- mkApp
- ( delayed_force hide_obligation
- , [|prod_applist t c'; Term.applistc b c'|] )
- with Not_found -> Constr.map aux c
- else Constr.map aux c
- in
- Constr.map aux
-
let subst_prog subst prg =
- if get_hide_obligations () then
- ( replace_appvars subst prg.prg_body
- , replace_appvars subst (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
- else
- let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
- ( Vars.replace_vars subst' prg.prg_body
- , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
+ let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
+ ( Vars.replace_vars subst' prg.prg_body
+ , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
let declare_definition ~pm prg =
let varsubst = obligation_substitution true prg in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5c329f60a9..f8a28332b1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -965,8 +965,6 @@ GRAMMAR EXTEND Gram
(* Searching the environment *)
| IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." ->
{ fun g -> VernacPrint (PrintAbout (qid,l,g)) }
- | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." ->
- { fun g -> VernacSearch (SearchHead c,g, l) }
| IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
{ fun g -> VernacSearch (SearchPattern c,g, l) }
| IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index ff4365c8d3..8e5942440b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -242,7 +242,6 @@ let pr_search a gopt b pr_p =
pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
++
match a with
- | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
| SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
| SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
| Search sl ->
diff --git a/vernac/search.ml b/vernac/search.ml
index 501e5b1a91..98e231de19 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -185,14 +185,6 @@ let rec pattern_filter pat ref env sigma typ =
| LetIn (_, _, _, typ) -> pattern_filter pat ref env sigma typ
| _ -> false
-let rec head_filter pat ref env sigma typ =
- let typ = Termops.strip_outer_cast sigma typ in
- if Constr_matching.is_matching_head env sigma pat typ then true
- else match EConstr.kind sigma typ with
- | Prod (_, _, typ)
- | LetIn (_, _, _, typ) -> head_filter pat ref env sigma typ
- | _ -> false
-
let full_name_of_reference ref =
let (dir,id) = repr_path (Nametab.path_of_global ref) in
DirPath.to_string dir ^ "." ^ Id.to_string id
@@ -274,19 +266,6 @@ let search_rewrite env sigma pat mods pr_search =
(** Search *)
-let search_by_head env sigma pat mods pr_search =
- let filter ref kind env typ =
- module_filter mods ref kind env sigma typ &&
- head_filter pat ref env sigma (EConstr.of_constr typ) &&
- blacklist_filter ref kind env sigma typ
- in
- let iter ref kind env typ =
- if filter ref kind env typ then pr_search ref kind env typ
- in
- generic_search env iter
-
-(** Search *)
-
let search env sigma items mods pr_search =
let filter ref kind env typ =
let eqb b1 b2 = if b1 then b2 else not b2 in
diff --git a/vernac/search.mli b/vernac/search.mli
index 09847f4e03..6557aa5986 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -47,8 +47,6 @@ val search_filter : glob_search_item -> filter_function
goal and the global environment for things matching [pattern] and
satisfying module exclude/include clauses of [modinout]. *)
-val search_by_head : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
- -> display_function -> unit
val search_rewrite : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
val search_pattern : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index cd0dd5e9a6..007a3b05fc 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -45,3 +45,4 @@ ComArguments
Vernacentries
ComTactic
Vernacinterp
+Vernac_classifier
diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml
new file mode 100644
index 0000000000..ffae2866c0
--- /dev/null
+++ b/vernac/vernac_classifier.ml
@@ -0,0 +1,215 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open CErrors
+open Util
+open Pp
+open CAst
+open Vernacextend
+open Vernacexpr
+
+let string_of_vernac_when = function
+ | VtLater -> "Later"
+ | VtNow -> "Now"
+
+let string_of_vernac_classification = function
+ | VtStartProof _ -> "StartProof"
+ | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w)
+ | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
+ | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)"
+ | VtQed VtDrop -> "Qed(drop)"
+ | VtProofStep { proof_block_detection } ->
+ "ProofStep " ^ Option.default "" proof_block_detection
+ | VtQuery -> "Query"
+ | VtMeta -> "Meta "
+ | VtProofMode _ -> "Proof Mode"
+
+let vtkeep_of_opaque = function
+ | Opaque -> VtKeepOpaque
+ | Transparent -> VtKeepDefined
+
+let idents_of_name : Names.Name.t -> Names.Id.t list =
+ function
+ | Names.Anonymous -> []
+ | Names.Name n -> [n]
+
+let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
+
+let options_affecting_stm_scheduling =
+ [ Attributes.universe_polymorphism_option_name;
+ stm_allow_nested_proofs_option_name;
+ Vernacinterp.proof_mode_opt_name;
+ Attributes.program_mode_option_name;
+ Proof_using.proof_using_opt_name;
+ ]
+
+let classify_vernac e =
+ let static_classifier ~atts e = match e with
+ (* Univ poly compatibility: we run it now, so that we can just
+ * look at Flags in stm.ml. Would be nicer to have the stm
+ * look at the entire dag to detect this option. *)
+ | VernacSetOption (_, l,_)
+ when CList.exists (CList.equal String.equal l)
+ options_affecting_stm_scheduling ->
+ VtSideff ([], VtNow)
+ (* Qed *)
+ | VernacAbort _ -> VtQed VtDrop
+ | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom)
+ | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque))
+ | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque)
+ (* Query *)
+ | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
+ | VernacCheckMayEval _ -> VtQuery
+ (* ProofStep *)
+ | VernacProof _
+ | VernacFocus _ | VernacUnfocus
+ | VernacSubproof _
+ | VernacCheckGuard
+ | VernacUnfocused
+ | VernacSolveExistential _ ->
+ VtProofStep { proof_block_detection = None }
+ | VernacBullet _ ->
+ VtProofStep { proof_block_detection = Some "bullet" }
+ | VernacEndSubproof ->
+ VtProofStep { proof_block_detection = Some "curly" }
+ (* StartProof *)
+ | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) ->
+ VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i)
+
+ | VernacDefinition (_,({v=i},_),ProveBody _) ->
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+ let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof(guarantee, idents_of_name i)
+ | VernacStartTheoremProof (_,l) ->
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+ let ids = List.map (fun (({v=i}, _), _) -> i) l in
+ let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof (guarantee,ids)
+ | VernacFixpoint (discharge,l) ->
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+ let guarantee =
+ if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+ else GuaranteesOpacity
+ in
+ let ids, open_proof =
+ List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} ->
+ id::l, b || body_def = None) ([],false) l in
+ if open_proof
+ then VtStartProof (guarantee,ids)
+ else VtSideff (ids, VtLater)
+ | VernacCoFixpoint (discharge,l) ->
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+ let guarantee =
+ if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+ else GuaranteesOpacity
+ in
+ let ids, open_proof =
+ List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } ->
+ id::l, b || body_def = None) ([],false) l in
+ if open_proof
+ then VtStartProof (guarantee,ids)
+ else VtSideff (ids, VtLater)
+ (* Sideff: apply to all open branches. usually run on master only *)
+ | VernacAssumption (_,_,l) ->
+ let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in
+ VtSideff (ids, VtLater)
+ | VernacPrimitive ((id,_),_,_) ->
+ VtSideff ([id.CAst.v], VtLater)
+ | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
+ | VernacInductive (_,l) ->
+ let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with
+ | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
+ | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
+ CList.map_filter (function
+ | AssumExpr({v=Names.Name n},_,_), _ -> Some n
+ | _ -> None) l) l in
+ VtSideff (List.flatten ids, VtLater)
+ | VernacScheme l ->
+ let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in
+ VtSideff (ids, VtLater)
+ | VernacCombinedScheme ({v=id},_) -> VtSideff ([id], VtLater)
+ | VernacBeginSection {v=id} -> VtSideff ([id], VtLater)
+ | VernacUniverse _ | VernacConstraint _
+ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
+ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
+ | VernacChdir _
+ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
+ | VernacArguments _
+ | VernacReserve _
+ | VernacGeneralizable _
+ | VernacSetOpacity _ | VernacSetStrategy _
+ | VernacSetOption _
+ | VernacAddOption _ | VernacRemoveOption _
+ | VernacMemOption _ | VernacPrintOption _
+ | VernacGlobalCheck _
+ | VernacDeclareReduction _
+ | VernacExistingClass _ | VernacExistingInstance _
+ | VernacRegister _
+ | VernacNameSectionHypSet _
+ | VernacComments _
+ | VernacDeclareInstance _ -> VtSideff ([], VtLater)
+ (* Who knows *)
+ | VernacLoad _ -> VtSideff ([], VtNow)
+ (* (Local) Notations have to disappear *)
+ | VernacEndSegment _ -> VtSideff ([], VtNow)
+ (* Modules with parameters have to be executed: can import notations *)
+ | VernacDeclareModule (exp,{v=id},bl,_)
+ | VernacDefineModule (exp,{v=id},bl,_,_) ->
+ VtSideff ([id], if bl = [] && exp = None then VtLater else VtNow)
+ | VernacDeclareModuleType ({v=id},bl,_,_) ->
+ VtSideff ([id], if bl = [] then VtLater else VtNow)
+ (* These commands alter the parser *)
+ | VernacDeclareCustomEntry _
+ | VernacOpenCloseScope _ | VernacDeclareScope _
+ | VernacDelimiters _ | VernacBindScope _
+ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
+ | VernacSyntaxExtension _
+ | VernacSyntacticDefinition _
+ | VernacRequire _ | VernacImport _ | VernacInclude _
+ | VernacDeclareMLModule _
+ | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow)
+ | VernacProofMode pm -> VtProofMode pm
+ | VernacInstance ((name,_),_,_,props,_) ->
+ let program, refine =
+ Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts)
+ in
+ if program || (props <> None && not refine) then
+ VtSideff (idents_of_name name.CAst.v, VtLater)
+ else
+ let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+ let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof (guarantee, idents_of_name name.CAst.v)
+ (* Stm will install a new classifier to handle these *)
+ | VernacBack _ | VernacAbortAll
+ | VernacUndoTo _ | VernacUndo _
+ | VernacResetName _ | VernacResetInitial
+ | VernacRestart -> VtMeta
+ (* What are these? *)
+ | VernacRestoreState _
+ | VernacWriteState _ -> VtSideff ([], VtNow)
+ (* Plugins should classify their commands *)
+ | VernacExtend (s,l) ->
+ try Vernacextend.get_vernac_classifier s l
+ with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
+ in
+ let static_control_classifier ({ CAst.v ; _ } as cmd) =
+ (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+ (* XXX why is Fail not always Query? *)
+ if Vernacprop.has_Fail cmd then
+ (match static_classifier ~atts:v.attrs v.expr with
+ | VtQuery | VtProofStep _ | VtSideff _
+ | VtMeta as x -> x
+ | VtQed _ -> VtProofStep { proof_block_detection = None }
+ | VtStartProof _ | VtProofMode _ -> VtQuery)
+ else
+ static_classifier ~atts:v.attrs v.expr
+
+ in
+ static_control_classifier e
diff --git a/vernac/vernac_classifier.mli b/vernac/vernac_classifier.mli
new file mode 100644
index 0000000000..61bf3a503a
--- /dev/null
+++ b/vernac/vernac_classifier.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Vernacextend
+
+val string_of_vernac_classification : vernac_classification -> string
+
+(** What does a vernacular do *)
+val classify_vernac : Vernacexpr.vernac_control -> vernac_classification
+
+(** *)
+val stm_allow_nested_proofs_option_name : string list
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1c774a35bf..481bc3071b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1215,9 +1215,11 @@ let msg_of_subsection ss id =
in
Pp.str kind ++ spc () ++ Id.print id
-let vernac_end_segment ~pm ({v=id} as lid) =
+let vernac_end_segment ~pm ~stack ({v=id} as lid) =
let ss = Lib.find_opening_node id in
let what_for = msg_of_subsection ss lid.v in
+ if Option.has_some stack then
+ CErrors.user_err (Pp.str "Command not supported (Open proofs remain)");
Declare.Obls.check_solved_obligations ~pm ~what_for;
match ss with
| Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
@@ -2173,9 +2175,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
VtNoProof(fun () ->
vernac_begin_section ~poly:(only_polymorphism atts) lid)
| VernacEndSegment lid ->
- VtReadProgram(fun ~pm ->
+ VtReadProgram(fun ~stack ~pm ->
unsupported_attributes atts;
- vernac_end_segment ~pm lid)
+ vernac_end_segment ~pm ~stack lid)
| VernacNameSectionHypSet (lid, set) ->
VtDefault(fun () ->
unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 2e360cf969..46acaf7264 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -75,7 +75,6 @@ type search_request =
type searchable =
| SearchPattern of constr_pattern_expr
| SearchRewrite of constr_pattern_expr
- | SearchHead of constr_pattern_expr
| Search of (bool * search_request) list
type locatable =
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index ed63332861..f320b65954 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -59,7 +59,7 @@ type typed_vernac =
| VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
| VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
| VtReadProof of (pstate:Declare.Proof.t -> unit)
- | VtReadProgram of (pm:Declare.OblState.t -> unit)
+ | VtReadProgram of (stack:Vernacstate.LemmaStack.t option -> pm:Declare.OblState.t -> unit)
| VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t)
| VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
| VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index e1e3b4cfe5..070c737882 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -77,7 +77,7 @@ type typed_vernac =
| VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
| VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
| VtReadProof of (pstate:Declare.Proof.t -> unit)
- | VtReadProgram of (pm:Declare.OblState.t -> unit)
+ | VtReadProgram of (stack:Vernacstate.LemmaStack.t option -> pm:Declare.OblState.t -> unit)
| VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t)
| VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
| VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 3a8a80d25a..e42775b76c 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -48,7 +48,7 @@ let interp_typed_vernac c ~pm ~stack =
vernac_require_open_lemma ~stack
(Vernacstate.LemmaStack.with_top ~f:(fun pstate -> f ~pstate));
stack, pm
- | VtReadProgram f -> f ~pm; stack, pm
+ | VtReadProgram f -> f ~stack ~pm; stack, pm
| VtModifyProgram f ->
let pm = f ~pm in stack, pm
| VtDeclareProgram f ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 15:42:40 +0000