aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml23
-rw-r--r--proofs/evar_refiner.ml8
-rw-r--r--proofs/goal.ml23
-rw-r--r--proofs/goal.mli3
-rw-r--r--proofs/goal_select.ml68
-rw-r--r--proofs/goal_select.mli26
-rw-r--r--proofs/logic.ml68
-rw-r--r--proofs/pfedit.ml26
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_bullet.ml68
-rw-r--r--proofs/proof_bullet.mli19
-rw-r--r--proofs/proof_global.ml3
-rw-r--r--proofs/proofs.mllib1
-rw-r--r--proofs/refine.ml16
-rw-r--r--proofs/tacmach.mli2
15 files changed, 219 insertions, 137 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 03ff580ad3..aeaf16723b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -62,9 +62,6 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
exception NotExtensibleClause
-let mk_freelisted c =
- map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c))
-
let clenv_push_prod cl =
let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
let rec clrec typ = match EConstr.kind cl.evd typ with
@@ -73,7 +70,7 @@ let clenv_push_prod cl =
let mv = new_meta () in
let dep = not (noccurn (cl_sigma cl) 1 u) in
let na' = if dep then na else Anonymous in
- let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in
+ let e' = meta_declare mv t ~name:na' cl.evd in
let concl = if dep then subst1 (mkMeta mv) u else u in
let def = applist (cl.templval.rebus,[mkMeta mv]) in
{ templval = mk_freelisted def;
@@ -107,8 +104,7 @@ let clenv_environments evd bound t =
let mv = new_meta () in
let dep = not (noccurn evd 1 t2) in
let na' = if dep then na else Anonymous in
- let t1 = EConstr.Unsafe.to_constr t1 in
- let e' = meta_declare mv t1 ~name:na' e in
+ let e' = meta_declare mv t1 ~name:na' e in
clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
(if dep then (subst1 (mkMeta mv) t2) else t2)
| (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
@@ -167,13 +163,13 @@ let clenv_assign mv rhs clenv =
user_err Pp.(str "clenv_assign: circularity in unification");
try
if meta_defined clenv.evd mv then
- if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
+ if not (EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
error_incompatible_inst clenv mv
else
clenv
else
let st = (Conv,TypeNotProcessed) in
- {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
+ {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
with Not_found ->
user_err Pp.(str "clenv_assign: undefined meta")
@@ -218,7 +214,7 @@ let clenv_assign mv rhs clenv =
*)
let clenv_metas_in_type_of_meta evd mv =
- (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas
+ (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
let dependent_in_type_of_metas clenv mvs =
List.fold_right
@@ -288,11 +284,11 @@ let adjust_meta_source evd mv = function
in situations like "ex_intro (fun x => P) ?ev p" *)
let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
if Metaset.mem mv t.freemetas then
- let f,l = decompose_app evd (EConstr.of_constr t.rebus) in
+ let f,l = decompose_app evd t.rebus in
match EConstr.kind evd f with
| Meta mv'' ->
(match meta_opt_fvalue evd mv'' with
- | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l
+ | Some (c,_) -> match_name c.rebus l
| None -> None)
| _ -> None
else None in
@@ -502,7 +498,6 @@ let clenv_assign_binding clenv k c =
let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in
let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
- let c = EConstr.Unsafe.to_constr c in
{ clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
let clenv_match_args bl clenv =
@@ -515,7 +510,7 @@ let clenv_match_args bl clenv =
(fun clenv {CAst.loc;v=(b,c)} ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
- if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
+ if EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv
else error_already_defined b
else
clenv_assign_binding clenv k c)
@@ -677,7 +672,7 @@ let define_with_type sigma env ev c =
let j = Environ.make_judge c ty in
let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in
let (ev, _) = destEvar sigma ev in
- let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
+ let sigma = Evd.define ev j.Environ.uj_val sigma in
sigma
let solve_evar_clause env sigma hyp_only clause = function
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0d197c92c5..c80f370fdc 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -25,8 +25,6 @@ open Ltac_pretype
type glob_constr_ltac_closure = ltac_var_map * glob_constr
let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
- let t1 = EConstr.of_constr t1 in
- let t2 = EConstr.of_constr t2 in
try Evar.equal (head_evar sigma t1) evk
with NoHeadEvar ->
try Evar.equal (head_evar sigma t2) evk
@@ -35,12 +33,12 @@ let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
let define_and_solve_constraints evk c env evd =
if Termops.occur_evar evd evk c then
Pretype_errors.error_occur_check env evd evk c;
- let evd = define evk (EConstr.Unsafe.to_constr c) evd in
+ let evd = define evk c evd in
let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in
match
List.fold_left
(fun p (pbty,env,t1,t2) -> match p with
- | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2)
+ | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2
| UnifFailure _ as x -> x) (Success evd)
pbs
with
@@ -59,7 +57,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
Pretyping.fail_evar = false;
Pretyping.expand_evars = true } in
try Pretyping.understand_ltac flags
- env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
+ env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
with e when CErrors.noncritical e ->
let loc = Glob_ops.loc_of_glob_constr rawc in
user_err ?loc
diff --git a/proofs/goal.ml b/proofs/goal.ml
index ba7e458f3a..1440d1636b 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -48,7 +48,7 @@ module V82 = struct
(* Access to ".evar_concl" *)
let concl evars gl =
let evi = Evd.find evars gl in
- EConstr.of_constr evi.Evd.evar_concl
+ evi.Evd.evar_concl
(* Access to ".evar_extra" *)
let extra evars gl =
@@ -61,7 +61,6 @@ module V82 = struct
be shelved. It must not appear as a future_goal, so the future
goals are restored to their initial value after the evar is
created. *)
- let concl = EConstr.Unsafe.to_constr concl in
let prev_future_goals = Evd.save_future_goals evars in
let evi = { Evd.evar_hyps = hyps;
Evd.evar_concl = concl;
@@ -86,7 +85,7 @@ module V82 = struct
if not (Evarutil.occur_evar_upto sigma evk c) then ()
else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
in
- Evd.define evk (EConstr.Unsafe.to_constr c) sigma
+ Evd.define evk c sigma
(* Instantiates a goal with an open term, using name of goal for evk' *)
let partial_solution_to sigma evk evk' c =
@@ -100,7 +99,9 @@ module V82 = struct
let same_goal evars1 gl1 evars2 gl2 =
let evi1 = Evd.find evars1 gl1 in
let evi2 = Evd.find evars2 gl2 in
- Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl &&
+ let c1 = EConstr.Unsafe.to_constr evi1.Evd.evar_concl in
+ let c2 = EConstr.Unsafe.to_constr evi2.Evd.evar_concl in
+ Constr.equal c1 c2 &&
Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
let weak_progress glss gls =
@@ -117,20 +118,6 @@ module V82 = struct
with a good implementation of them.
*)
- (* Used for congruence closure *)
- let new_goal_with sigma gl extra_hyps =
- let evi = Evd.find sigma gl in
- let hyps = evi.Evd.evar_hyps in
- let new_hyps =
- List.fold_right Environ.push_named_context_val extra_hyps hyps in
- let filter = evi.Evd.evar_filter in
- let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in
- let new_evi =
- { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
- let new_evi = Typeclasses.mark_unresolvable new_evi in
- let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
- { Evd.it = evk ; sigma = sigma; }
-
(* Used by the compatibility layer and typeclasses *)
let nf_evar sigma gl =
let evi = Evd.find sigma gl in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index dc9863156c..b8c979ad7a 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -64,9 +64,6 @@ module V82 : sig
(* Principal part of tclNOTSAMEGOAL *)
val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
- (* Used for congruence closure *)
- val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma
-
(* Used by the compatibility layer and typeclasses *)
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
new file mode 100644
index 0000000000..65a94a2c60
--- /dev/null
+++ b/proofs/goal_select.ml
@@ -0,0 +1,68 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \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 Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+ different type than [goal_reference] mostly because if it makes sense
+ to print a goal that is out of focus (or already solved) it doesn't
+ make sense to apply a tactic to it. Hence it the types may look very
+ similar, they do not seem to mean the same thing. *)
+type t =
+ | SelectAlreadyFocused
+ | SelectNth of int
+ | SelectList of (int * int) list
+ | SelectId of Id.t
+ | SelectAll
+
+(* Default goal selector: selector chosen when a tactic is applied
+ without an explicit selector. *)
+let default_goal_selector = ref (SelectNth 1)
+let get_default_goal_selector () = !default_goal_selector
+
+let pr_range_selector (i, j) =
+ if i = j then Pp.int i
+ else Pp.(int i ++ str "-" ++ int j)
+
+let pr_goal_selector = function
+ | SelectAlreadyFocused -> Pp.str "!"
+ | SelectAll -> Pp.str "all"
+ | SelectNth i -> Pp.int i
+ | SelectList l ->
+ Pp.(str "["
+ ++ prlist_with_sep pr_comma pr_range_selector l
+ ++ str "]")
+ | SelectId id -> Names.Id.print id
+
+let parse_goal_selector = function
+ | "!" -> SelectAlreadyFocused
+ | "all" -> SelectAll
+ | i ->
+ let err_msg = "The default selector must be \"all\" or a natural number." in
+ begin try
+ let i = int_of_string i in
+ if i < 0 then CErrors.user_err Pp.(str err_msg);
+ SelectNth i
+ with Failure _ -> CErrors.user_err Pp.(str err_msg)
+ end
+
+let _ = let open Goptions in
+ declare_string_option
+ { optdepr = false;
+ optname = "default goal selector" ;
+ optkey = ["Default";"Goal";"Selector"] ;
+ optread = begin fun () ->
+ Pp.string_of_ppcmds
+ (pr_goal_selector !default_goal_selector)
+ end;
+ optwrite = begin fun n ->
+ default_goal_selector := parse_goal_selector n
+ end
+ }
diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli
new file mode 100644
index 0000000000..b1c5723885
--- /dev/null
+++ b/proofs/goal_select.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \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 Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+ different type than [goal_reference] mostly because if it makes sense
+ to print a goal that is out of focus (or already solved) it doesn't
+ make sense to apply a tactic to it. Hence it the types may look very
+ similar, they do not seem to mean the same thing. *)
+type t =
+ | SelectAlreadyFocused
+ | SelectNth of int
+ | SelectList of (int * int) list
+ | SelectId of Id.t
+ | SelectAll
+
+val pr_goal_selector : t -> Pp.t
+val get_default_goal_selector : unit -> t
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e5294715e0..4934afa837 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -289,7 +289,15 @@ let collect_meta_variables c =
let rec collrec deep acc c = match kind c with
| Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
| Cast(c,_,_) -> collrec deep acc c
- | (App _| Case _) -> Constr.fold (collrec deep) acc c
+ | Case(ci,p,c,br) ->
+ (* Hack assuming only two situations: the legacy one that branches,
+ if with Metas, are Meta, and the new one with eta-let-expanded
+ branches *)
+ let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in
+ Array.fold_left (collrec deep)
+ (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c)
+ br
+ | App _ -> Constr.fold (collrec deep) acc c
| Proj (_, c) -> collrec deep acc c
| _ -> Constr.fold (collrec true) acc c
in
@@ -387,12 +395,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| Case (ci,p,c,lf) ->
let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
- let (acc'',sigma, rbranches) =
- Array.fold_left2
- (fun (lacc,sigma,bacc) ty fi ->
- let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
- (acc',sigma,[]) lbrty lf
- in
+ let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
let lf' = Array.rev_of_list rbranches in
let ans =
if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -440,12 +443,7 @@ and mk_hdgoals sigma goal goalacc trm =
| Case (ci,p,c,lf) ->
let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
- let (acc'',sigma,rbranches) =
- Array.fold_left2
- (fun (lacc,sigma,bacc) ty fi ->
- let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
- (acc',sigma,[]) lbrty lf
- in
+ let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
let lf' = Array.rev_of_list rbranches in
let ans =
if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -497,6 +495,50 @@ and mk_casegoals sigma goal goalacc p c =
let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
(acc'',lbrty,conclty,sigma,p',c')
+and treat_case sigma goal ci lbrty lf acc' =
+ let rec strip_outer_cast c = match kind c with
+ | Cast (c,_,_) -> strip_outer_cast c
+ | _ -> c in
+ let decompose_app_vect c = match kind c with
+ | App (f,cl) -> (f, cl)
+ | _ -> (c,[||]) in
+ let env = Goal.V82.env sigma goal in
+ Array.fold_left3
+ (fun (lacc,sigma,bacc) ty fi l ->
+ if isMeta (strip_outer_cast fi) then
+ (* Support for non-eta-let-expanded Meta as found in *)
+ (* destruct/case with an non eta-let expanded elimination scheme *)
+ let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in
+ r,s,(fi'::bacc)
+ else
+ (* Deal with a branch in expanded form of the form
+ Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as
+ if it were not so, so as to preserve compatibility with when
+ destruct/case generated schemes of the form
+ Case(ci,p,c,[|Meta;...;Meta|];
+ CAUTION: it does not deal with the general case of eta-zeta
+ reduced branches having a form different from Meta, as it
+ would be theoretically the case with third-party code *)
+ let n = List.length l in
+ let ctx, body = Term.decompose_lam_n_decls n fi in
+ let head, args = decompose_app_vect body in
+ (* Strip cast because clenv_cast_meta adds a cast when the branch is
+ eta-expanded but when not when the branch has the single-meta
+ form [Meta] *)
+ let head = strip_outer_cast head in
+ if isMeta head then begin
+ assert (args = Context.Rel.to_extended_vect mkRel 0 ctx);
+ let head' = lift (-n) head in
+ let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in
+ let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in
+ (r,s,fi'::bacc)
+ end
+ else
+ (* Supposed to be meta-free *)
+ let sigma, t'ty = goal_type_of env sigma fi in
+ let sigma = check_conv_leq_goal env sigma fi t'ty ty in
+ (lacc,sigma,fi::bacc))
+ (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
let convert_hyp check sign sigma d =
let id = NamedDecl.get_id d in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 8725f51cd7..03c0969faa 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -100,11 +100,23 @@ let solve ?with_end_tac gi info_lvl tac pr =
| None -> tac
| Some _ -> Proofview.Trace.record_info_trace tac
in
- let tac = match gi with
- | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
- | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac
- | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
- | Vernacexpr.SelectAll -> tac
+ let tac = let open Goal_select in match gi with
+ | SelectAlreadyFocused ->
+ let open Proofview.Notations in
+ Proofview.numgoals >>= fun n ->
+ if n == 1 then tac
+ else
+ let e = CErrors.UserError
+ (None,
+ Pp.(str "Expected a single focused goal but " ++
+ int n ++ str " goals are focused."))
+ in
+ Proofview.tclZERO e
+
+ | SelectNth i -> Proofview.tclFOCUS i i tac
+ | SelectList l -> Proofview.tclFOCUSLIST l tac
+ | SelectId id -> Proofview.tclFOCUSID id tac
+ | SelectAll -> tac
in
let tac =
if use_unification_heuristics () then
@@ -121,7 +133,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
with
Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof")
-let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
+let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
let instantiate_nth_evar_com n com =
Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
@@ -233,7 +245,7 @@ let apply_implicit_tactic tac = (); fun env sigma evk ->
(Environ.named_context env) ->
let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
(try
- let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
+ let c = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr evi.evar_concl) in
let c = EConstr.of_constr c in
if Evarutil.has_undefined_evars sigma c then raise Exit;
let (ans, _, ctx) =
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 65cde3a3ae..805635dfa4 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -75,7 +75,7 @@ val current_proof_statement :
tac] applies [tac] to all subgoals. *)
val solve : ?with_end_tac:unit Proofview.tactic ->
- Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
+ Goal_select.t -> int option -> unit Proofview.tactic ->
Proof.t -> Proof.t * bool
(** [by tac] applies tactic [tac] to the 1st subgoal of the current
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index e22d382f7d..cc3e79f858 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -10,19 +10,22 @@
open Proof
-type t = Vernacexpr.bullet
+type t =
+ | Dash of int
+ | Star of int
+ | Plus of int
let bullet_eq b1 b2 = match b1, b2 with
-| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
-| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
-| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
+| Dash n1, Dash n2 -> n1 = n2
+| Star n1, Star n2 -> n1 = n2
+| Plus n1, Plus n2 -> n1 = n2
| _ -> false
let pr_bullet b =
match b with
- | Vernacexpr.Dash n -> Pp.(str (String.make n '-'))
- | Vernacexpr.Star n -> Pp.(str (String.make n '*'))
- | Vernacexpr.Plus n -> Pp.(str (String.make n '+'))
+ | Dash n -> Pp.(str (String.make n '-'))
+ | Star n -> Pp.(str (String.make n '*'))
+ | Plus n -> Pp.(str (String.make n '+'))
type behavior = {
@@ -195,52 +198,5 @@ let put p b =
let suggest p =
(!current_behavior).suggest p
-(**********************************************************)
-(* *)
-(* Default goal selector *)
-(* *)
-(**********************************************************)
-
-
-(* Default goal selector: selector chosen when a tactic is applied
- without an explicit selector. *)
-let default_goal_selector = ref (Vernacexpr.SelectNth 1)
-let get_default_goal_selector () = !default_goal_selector
-
-let pr_range_selector (i, j) =
- if i = j then Pp.int i
- else Pp.(int i ++ str "-" ++ int j)
-
-let pr_goal_selector = function
- | Vernacexpr.SelectAll -> Pp.str "all"
- | Vernacexpr.SelectNth i -> Pp.int i
- | Vernacexpr.SelectList l ->
- Pp.(str "["
- ++ prlist_with_sep pr_comma pr_range_selector l
- ++ str "]")
- | Vernacexpr.SelectId id -> Names.Id.print id
-
-let parse_goal_selector = function
- | "all" -> Vernacexpr.SelectAll
- | i ->
- let err_msg = "The default selector must be \"all\" or a natural number." in
- begin try
- let i = int_of_string i in
- if i < 0 then CErrors.user_err Pp.(str err_msg);
- Vernacexpr.SelectNth i
- with Failure _ -> CErrors.user_err Pp.(str err_msg)
- end
-
-let _ =
- Goptions.(declare_string_option{optdepr = false;
- optname = "default goal selector" ;
- optkey = ["Default";"Goal";"Selector"] ;
- optread = begin fun () ->
- Pp.string_of_ppcmds
- (pr_goal_selector !default_goal_selector)
- end;
- optwrite = begin fun n ->
- default_goal_selector := parse_goal_selector n
- end
- })
-
+let pr_goal_selector = Goal_select.pr_goal_selector
+let get_default_goal_selector = Goal_select.get_default_goal_selector
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index ffbaa0fac9..a09a7ec1d2 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -14,7 +14,10 @@
(* *)
(**********************************************************)
-type t = Vernacexpr.bullet
+type t =
+ | Dash of int
+ | Star of int
+ | Plus of int
(** A [behavior] is the data of a put function which
is called when a bullet prefixes a tactic, a suggest function
@@ -42,12 +45,8 @@ val register_behavior : behavior -> unit
val put : Proof.t -> t -> Proof.t
val suggest : Proof.t -> Pp.t
-(**********************************************************)
-(* *)
-(* Default goal selector *)
-(* *)
-(**********************************************************)
-
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t
-val get_default_goal_selector : unit -> Vernacexpr.goal_selector
-
+(** Deprecated *)
+val pr_goal_selector : Goal_select.t -> Pp.t
+[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"]
+val get_default_goal_selector : unit -> Goal_select.t
+[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"]
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d6c0e33414..842003bc86 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -83,6 +83,7 @@ type proof_ending =
| Proved of Vernacexpr.opacity_flag *
Misctypes.lident option *
proof_object
+
type proof_terminator = proof_ending -> unit
type closed_proof = proof_object * proof_terminator
@@ -340,7 +341,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
have existential variables in the initial types of goals, we need to
normalise them for the kernel. *)
let subst_evar k =
- Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in
+ Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in
let nf = Universes.nf_evars_and_universes_opt_subst subst_evar
(UState.subst universes) in
let make_body =
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 058e839b47..197f71ca91 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_type
Logic
Refine
Proof
+Goal_select
Proof_bullet
Proof_global
Redexpr
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 909556b1ee..5a2d82977e 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -15,7 +15,7 @@ open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
let extract_prefix env info =
- let ctx1 = List.rev (Environ.named_context env) in
+ let ctx1 = List.rev (EConstr.named_context env) in
let ctx2 = List.rev (Evd.evar_context info) in
let rec share l1 l2 accu = match l1, l2 with
| d1 :: l1, d2 :: l2 ->
@@ -29,21 +29,21 @@ let typecheck_evar ev env sigma =
let info = Evd.find sigma ev in
(** Typecheck the hypotheses. *)
let type_hyp (sigma, env) decl =
- let t = EConstr.of_constr (NamedDecl.get_type decl) in
+ let t = NamedDecl.get_type decl in
let evdref = ref sigma in
let _ = Typing.e_sort_of env evdref t in
let () = match decl with
| LocalAssum _ -> ()
- | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
+ | LocalDef (_,body,_) -> Typing.e_check env evdref body t
in
- (!evdref, Environ.push_named decl env)
+ (!evdref, EConstr.push_named decl env)
in
let (common, changed) = extract_prefix env info in
- let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+ let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
(** Typecheck the conclusion *)
let evdref = ref sigma in
- let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
+ let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
!evdref
let typecheck_proof c concl env sigma =
@@ -106,7 +106,6 @@ let generic_refine ~typecheck f gl =
let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
(** Proceed to the refinement *)
- let c = EConstr.Unsafe.to_constr c in
let sigma = match Proofview.Unsafe.advance sigma self with
| None ->
(** Nothing to do, the goal has been solved by side-effect *)
@@ -124,7 +123,8 @@ let generic_refine ~typecheck f gl =
(** Mark goals *)
let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
- let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in
+ let trace () = Pp.(hov 2 (str"simple refine"++spc()++
+ Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in
Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
Proofview.Unsafe.tclEVARS sigma <*>
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 770d0940a3..de96f85104 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -95,7 +95,7 @@ val pr_glls : goal list sigma -> Pp.t
(* Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
- val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference
+ val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t
(** FIXME: encapsulate the level in an existential type. *)
val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 17:30:27 +0000