aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/btauto/refl_btauto.ml4
-rw-r--r--plugins/cc/cctac.ml6
-rw-r--r--plugins/omega/coq_omega.ml4
-rw-r--r--plugins/quote/quote.ml18
-rw-r--r--plugins/setoid_ring/newring.ml48
-rw-r--r--proofs/goal.ml33
-rw-r--r--proofs/goal.mli24
-rw-r--r--proofs/proof.ml2
-rw-r--r--proofs/proofview.ml155
-rw-r--r--proofs/proofview.mli57
-rw-r--r--proofs/tacmach.ml53
-rw-r--r--proofs/tacmach.mli30
-rw-r--r--tactics/auto.ml8
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml4
-rw-r--r--tactics/contradiction.ml12
-rw-r--r--tactics/elim.ml2
-rw-r--r--tactics/eqdecide.ml44
-rw-r--r--tactics/equality.ml42
-rw-r--r--tactics/evar_tactics.ml4
-rw-r--r--tactics/extratactics.ml414
-rw-r--r--tactics/inv.ml12
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/refine.ml6
-rw-r--r--tactics/rewrite.ml9
-rw-r--r--tactics/tacinterp.ml221
-rw-r--r--tactics/tacinterp.mli6
-rw-r--r--tactics/tacticals.ml19
-rw-r--r--tactics/tactics.ml135
-rw-r--r--toplevel/auto_ind_decl.ml19
30 files changed, 441 insertions, 476 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 46a7e596c..4585468ad 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -217,7 +217,7 @@ module Btauto = struct
Tacticals.tclFAIL 0 msg gl
let try_unification env =
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
let eq = Lazy.force eq in
let t = decomp_term concl in
match t with
@@ -230,7 +230,7 @@ module Btauto = struct
Tacticals.New.tclFAIL 0 msg
let tac =
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
let eq = Lazy.force eq in
let bool = Lazy.force Bool.typ in
let t = decomp_term concl in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 63b6375e1..e120de478 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -348,7 +348,7 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
let discriminate_tac cstr p =
let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>- fun intype ->
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
let outsort = mkType (Termops.new_univ ()) in
Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>- fun xid ->
Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) >>- fun tid ->
@@ -394,7 +394,7 @@ let cc_tactic depth additionnal_terms =
let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
discriminate_tac cstr p
| Incomplete ->
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
let metacnt = ref 0 in
let newmeta _ = incr metacnt; _M !metacnt in
let terms_to_complete =
@@ -451,7 +451,7 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
*)
let f_equal =
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
let cut_eq c1 c2 =
let ty = Termops.refresh_universes (type_of c1) in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 512e372bb..adc1d9ee3 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1781,11 +1781,11 @@ let destructure_hyps =
| e when catchable_exception e -> loop lit
end
in
- Goal.hyps >>- fun hyps ->
+ Proofview.Goal.hyps >>- fun hyps ->
loop (Environ.named_context_of_val hyps)
let destructure_goal =
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
Tacmach.New.of_old decidability >>- fun decidability ->
let rec loop t =
match destructurate_prop t with
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 0cf4d3bb4..80053ea4d 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -227,7 +227,9 @@ let compute_ivs f cs =
| Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
let (args3, body3) = decompose_lam body2 in
let nargs3 = List.length args3 in
- Tacmach.New.pf_apply Reductionops.is_conv >- fun is_conv ->
+ Goal.env >- fun env ->
+ Goal.defs >- fun sigma ->
+ let is_conv = Reductionops.is_conv env sigma in
Goal.return
begin match decomp_term body3 with
| Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
@@ -452,10 +454,10 @@ let quote_terms ivs lc =
let quote f lid =
Tacmach.New.pf_global f >>- fun f ->
- Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl ->
- compute_ivs f cl >>- fun ivs ->
- Goal.concl >>- fun concl ->
- quote_terms ivs [concl] >>- fun quoted_terms ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>- fun cl ->
+ Proofview.Goal.lift (compute_ivs f cl) >>- fun ivs ->
+ Proofview.Goal.concl >>- fun concl ->
+ Proofview.Goal.lift (quote_terms ivs [concl]) >>- fun quoted_terms ->
let (p, vm) = match quoted_terms with
| [p], vm -> (p,vm)
| _ -> assert false
@@ -466,9 +468,9 @@ let quote f lid =
let gen_quote cont c f lid =
Tacmach.New.pf_global f >>- fun f ->
- Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl ->
- compute_ivs f cl >>- fun ivs ->
- quote_terms ivs [c] >>- fun quoted_terms ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>- fun cl ->
+ Proofview.Goal.lift (compute_ivs f cl) >>- fun ivs ->
+ Proofview.Goal.lift (quote_terms ivs [c]) >>- fun quoted_terms ->
let (p, vm) = match quoted_terms with
| [p], vm -> (p,vm)
| _ -> assert false
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 907cd474c..011aba5d7 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -798,8 +798,8 @@ let ltac_ring_structure e =
open Proofview.Notations
let ring_lookup (f:glob_tactic_expr) lH rl t =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let rl = make_args_list rl t in
let e = find_ring_structure env sigma rl in
let rl = carg (make_term_list e.ring_carrier rl) in
@@ -1119,8 +1119,8 @@ let ltac_field_structure e =
field_simpl_eq_in_ok;cond_ok;pretac;posttac]
let field_lookup (f:glob_tactic_expr) lH rl t =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let rl = make_args_list rl t in
let e = find_field_structure env sigma rl in
let rl = carg (make_term_list e.field_carrier rl) in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 988c10d27..da5cb6b19 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -352,39 +352,6 @@ let env env _ _ _ = env
let defs _ rdefs _ _ =
!rdefs
-(* Cf mli for more detailed comment.
- [null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
- to communicate whether or not the value is defined in the particular context. *)
-exception UndefinedHere
-(* no handler: this should never be allowed to reach toplevel *)
-let null _ _ _ _ = raise UndefinedHere
-
-let plus s1 s2 env rdefs goal info =
- try s1 env rdefs goal info
- with UndefinedHere -> s2 env rdefs goal info
-
-(* Equality of two goals *)
-let equal_pointer { content = e1 } { content = e2 } = Evar.equal e1 e2
-
-let here goal value _ _ goal' _ =
- if equal_pointer goal goal' then
- value
- else
- raise UndefinedHere
-
-(* arnaud: voir à la passer dans Util ? *)
-let rec list_mem_with eq x = function
- | y::_ when eq x y -> true
- | _::l -> list_mem_with eq x l
- | [] -> false
-
-let here_list goals value _ _ goal' _ =
- if list_mem_with equal_pointer goal' goals then
- value
- else
- raise UndefinedHere
-
-
(*** Conversion in goals ***)
let convert_hyp check (id,b,bt as d) env rdefs gl info =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 718d23ccc..216e12f3a 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -147,30 +147,6 @@ val env : Environ.env sensitive
(* [defs] is the [Evd.evar_map] at the current evaluation point *)
val defs : Evd.evar_map sensitive
-(* These four functions serve as foundation for the goal sensitive part
- of the tactic monad (see Proofview).
- [here] is a special sort of [return]: [here g a] is the value [a], but
- does not have any value (it raises an exception) if evaluated in
- any other goal than [g].
- [here_list] is the same, except with a list of goals rather than a single one.
- [plus a b] is the same as [a] if [a] is defined in the current goal, otherwise
- it is [b]. Effectively it's defined in the goals where [a] and [b] are defined.
- [null] is defined in no goal. (it is a neutral element for [plus]). *)
-(* spiwack: these primitives are a bit hackish, but I couldn't find another way
- to pass information between goals, like for an intro tactic which gives to
- each goal the name of the variable it introduce.
- In pratice, in my experience, the primitives given in Proofview (in terms of
- [here] and [plus]) are sufficient to define any tactics, hence these might
- be another example of communication primitives between Goal and Proofview.
- Still, I can't see a way to prevent using the Proofview primitive to read
- a goal sensitive value out of its valid context. *)
-val null : 'a sensitive
-
-val plus : 'a sensitive -> 'a sensitive -> 'a sensitive
-
-val here : goal -> 'a -> 'a sensitive
-
-val here_list : goal list -> 'a -> 'a sensitive
(*** Additional functions ***)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 712845f58..89f3638a1 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -252,7 +252,7 @@ let initial_goals p = Proofview.initial_goals p.proofview
let run_tactic env tac pr =
let sp = pr.proofview in
- let tacticced_proofview = Proofview.apply env tac sp in
+ let (_,tacticced_proofview) = Proofview.apply env tac sp in
{ pr with proofview = tacticced_proofview }
let emit_side_effects eff pr =
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 388778ff7..1fbce62df 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -201,7 +201,7 @@ type +'a tactic = Environ.env -> 'a Inner.t
(* Applies a tactic to the current proofview. *)
let apply env t sp =
let next = Backtrack.run (Inner.run (t env) sp) in
- next.Inner.state
+ next.Inner.result , next.Inner.state
(*** tacticals ***)
@@ -272,15 +272,10 @@ let tclFOCUS i j t env =
(* arnaud: vérifier les commentaires de dispatch vis-à-vis de l'ordre
d'évaluation des buts. Ne pas oublier le mli *)
+(* arnaud: commenter [tclDISPATCHL] *)
(* Dispatch tacticals are used to apply a different tactic to each goal under
consideration. They come in two flavours:
- [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic].
- [tclDISPATCHS] takes a list of ['a sensitive tactic] and returns and returns
- and ['a sensitive tactic] where the ['a sensitive] interpreted in a goal [g]
- corresponds to that of the tactic which created [g].
- It is to be noted that the return value of [tclDISPATCHS ts] makes only
- sense in the goals immediatly built by it, and would cause an anomaly
- is used otherwise. *)
+ [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic]. *)
exception SizeMismatch
let _ = Errors.register_handler begin function
| SizeMismatch -> Errors.error "Incorrect number of goals."
@@ -312,31 +307,12 @@ let rec tclDISPATCHGEN null join tacs env =
tclDISPATCHGEN null join tacs env >>= fun x ->
Inner.get >>= fun step' ->
Inner.set {step' with comb=step.comb@step'.comb} >>
- Inner.return (join x y)
+ Inner.return (join y x)
| _ , _ -> tclZERO SizeMismatch env
let unitK () () = ()
let tclDISPATCH = tclDISPATCHGEN () unitK
-(* This is a helper function for the dispatching tactics (like [tclGOALBIND] and
- [tclDISPATCHS]). It takes an ['a sensitive] value, and returns a tactic
- whose return value is, again, ['a sensitive] but only has value in the
- (unmodified) goals under focus. *)
-let here_s b env =
- (* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- Inner.get >>= fun step ->
- Inner.return (Goal.bind (Goal.here_list step.comb b) (fun b -> b))
-
-(* see .mli for documentation. *)
-let tclDISPATCHS tacs =
- let tacs =
- List.map begin fun tac ->
- tclBIND tac here_s
- end tacs
- in
- tclDISPATCHGEN Goal.null Goal.plus tacs
-
let tclDISPATCHL tacs =
let tacs =
List.map begin fun tac ->
@@ -363,43 +339,6 @@ let tclEXTEND tacs1 rtac tacs2 env =
let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
tclDISPATCH tacs env
-(* [tclGOALBIND] and [tclGOALBINDU] are sorts of bind which take a
- [Goal.sensitive] as a first argument, the tactic then acts on each goal separately.
- Allows backtracking between goals. *)
-
-(* [list_of_sensitive s k] where [s] is and ['a Goal.sensitive] [k]
- has type ['a -> 'b] returns the list of ['b] obtained by evualating
- [s] to each goal successively and applying [k] to each result. *)
-let list_of_sensitive s k env step =
- Goal.list_map begin fun defs g ->
- let (a,defs) = Goal.eval s env defs g in
- (k a) , defs
- end step.comb step.solution
-(* In form of a tactic *)
-let list_of_sensitive s k env =
- (* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- let (>>) = Inner.seq in
- Inner.get >>= fun step ->
- try
- let (tacs,defs) = list_of_sensitive s k env step in
- Inner.set { step with solution = defs; } >>
- Inner.return tacs
- with e when Errors.noncritical e ->
- tclZERO e env
-
-let tclGOALBIND s k =
- (* spiwack: the first line ensures that the value returned by the tactic [k] will
- not "escape its scope". *)
- let k a = tclBIND (k a) here_s in
- tclBIND (list_of_sensitive s k) begin fun tacs ->
- tclDISPATCHGEN Goal.null Goal.plus tacs
- end
-
-let tclGOALBINDU s k =
- tclBIND (list_of_sensitive s k) begin fun tacs ->
- tclDISPATCHGEN () unitK tacs
- end
(* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
everything is done in one step. *)
@@ -427,21 +366,6 @@ let sensitive_on_proofview s env step =
with e when Errors.noncritical e ->
tclZERO e env
-(* spiwack: [lift_sensitive] is probably a better abstraction
- than [tclGOALBIND]. *)
-let lift_sensitive s env =
- (* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- let (>>) = Inner.seq in
- Inner.get >>= fun step ->
- let (res,sigma) =
- Goal.list_map begin fun sigma g ->
- Goal.eval s env step.solution g
- end step.comb step.solution
- in
- Inner.set { step with solution=sigma } >>
- Inner.return res
-
(* arnaud: on pourrait regarder la liste de buts aussi, mais je
ne sais pas encore comment. Pour l'instant on fait au plus
simple. *)
@@ -499,13 +423,36 @@ let tclTIMEOUT n t g =
let in_proofview p k =
k p.solution
+
+(* spiwack: to help using `bind' like construct consistently. A glist
+ is promissed to have exactly one element per goal when it is
+ produced. *)
+type 'a glist = 'a list
+
module Notations = struct
let (>-) = Goal.bind
- let (>>-) = tclGOALBINDU
- let (>>--) = tclGOALBIND
let (>=) = tclBIND
- let (>>=) t k = t >= fun s -> s >>- k
- let (>>==) t k = t >= fun s -> s >>-- k
+ let (>>-) t k =
+ (* spiwack: the application of List.map may raise errors, as this
+ combinator is mostly used in porting historical tactic code,
+ where the error flow is somewhat hard to follow, hence the
+ try/with *)
+ t >= fun l ->
+ try tclDISPATCH (List.map k l)
+ with e when Errors.noncritical e -> tclZERO e
+ let (>>--) t k =
+ (* spiwack: the application of List.map may raise errors, as this
+ combinator is mostly used in porting historical tactic code,
+ where the error flow is somewhat hard to follow, hence the
+ try/with *)
+ begin
+ t >= fun l ->
+ try tclDISPATCHL (List.map k l)
+ with e when Errors.noncritical e -> tclZERO e
+ end >= fun l' ->
+ tclUNIT (List.flatten l')
+ let (>>=) = (>>-)
+ let (>>==) = (>>--)
let (<*>) = tclTHEN
let (<+>) = tclOR
end
@@ -515,15 +462,8 @@ let rec list_map f = function
| [] -> tclUNIT []
| a::l ->
f a >= fun a' ->
- list_map f l >= fun l' ->
- tclUNIT (a'::l')
-
-let rec sensitive_list_map f = function
- | [] -> tclUNIT (Goal.return [])
- | a::l ->
- f a >>== fun a' ->
- sensitive_list_map f l >>== fun l' ->
- tclUNIT (Goal.return (a'::l'))
+ list_map f l >= fun l' ->
+ tclUNIT (a'::l')
(*** Compatibility layer with <= 8.2 tactics ***)
@@ -600,12 +540,39 @@ module V82 = struct
let of_tactic t gls =
let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
- let final = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
+ let (_,final) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
{ Evd.sigma = final.solution ; it = final.comb }
end
+module Goal = struct
+
+ type 'a u = 'a list
+
+ let lift s env =
+ (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+ let (>>=) = Inner.bind in
+ let (>>) = Inner.seq in
+ Inner.get >>= fun step ->
+ try
+ let (res,sigma) =
+ Goal.list_map begin fun sigma g ->
+ Goal.eval s env sigma g
+ end step.comb step.solution
+ in
+ Inner.set { step with solution=sigma } >>
+ Inner.return res
+ with e when Errors.noncritical e ->
+ tclZERO e env
+
+ let return x = lift (Goal.return x)
+ let concl = lift Goal.concl
+ let hyps = lift Goal.hyps
+ let env = lift Goal.env
+end
+
+
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6165b02a9..93d1f2bb6 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -118,7 +118,7 @@ val unfocus : focus_context -> proofview -> proofview
type +'a tactic
(* Applies a tactic to the current proofview. *)
-val apply : Environ.env -> 'a tactic -> proofview -> proofview
+val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview
(*** tacticals ***)
@@ -167,9 +167,6 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
sense in the goals immediatly built by it, and would cause an anomaly
is used otherwise. *)
val tclDISPATCH : unit tactic list -> unit tactic
-(* arnaud: quick hack to fix the order of goal solving to comply with Ltac.
- it will probably have to go. *)
-val tclDISPATCHS : 'a Goal.sensitive tactic list -> 'a Goal.sensitive tactic
val tclDISPATCHL : 'a tactic list -> 'a list tactic
(* [tclEXTEND b r e] is a variant to [tclDISPATCH], where the [r] tactic
@@ -178,18 +175,9 @@ val tclDISPATCHL : 'a tactic list -> 'a list tactic
is applied to every goal in between. *)
val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
-(* A sort of bind which takes a [Goal.sensitive] as a first argument,
- the tactic then acts on each goal separately.
- Allows backtracking between goals. *)
-val tclGOALBIND : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
-val tclGOALBINDU : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
-
(* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic
-(* [lift_sensitive s] returns the list corresponding to the evaluation
- of [s] on each of the focused goals *)
-val lift_sensitive : 'a Goal.sensitive -> 'a list tactic
(* [tclPROGRESS t] behaves has [t] as long as [t] progresses. *)
val tclPROGRESS : 'a tactic -> 'a tactic
@@ -197,7 +185,10 @@ val tclPROGRESS : 'a tactic -> 'a tactic
(* [tclEVARMAP] doesn't affect the proof, it returns the current evar_map. *)
val tclEVARMAP : Evd.evar_map tactic
-(* [tclENV] doesn't affect the proof, it returns the current evar_map. *)
+(* [tclENV] doesn't affect the proof, it returns the current
+ environment. It is not the environment of a particular goal,
+ rather the "global" environment of the proof. The goal-wise
+ environment is returned by {!Proofview.Goal.env}. *)
val tclENV : Environ.env tactic
(* [tclTIMEOUT n t] runs [t] for at most [n] seconds, succeeds if [t]
@@ -206,31 +197,36 @@ val tclENV : Environ.env tactic
val tclTIMEOUT : int -> unit tactic -> unit tactic
val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic
-val sensitive_list_map : ('a -> 'b Goal.sensitive tactic) -> 'a list -> 'b list Goal.sensitive tactic
(*** Commands ***)
val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
+(* spiwack: to help using `bind' like construct consistently. A glist
+ is promissed to have exactly one element per goal when it is
+ produced. *)
+type 'a glist = private 'a list
+
(* Notations for building tactics. *)
module Notations : sig
(* Goal.bind *)
val (>-) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive) -> 'b Goal.sensitive
- (* tclGOALBINDU *)
- val (>>-) : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
- (* tclGOALBIND *)
- val (>>--) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+ (* [t >>- k] is [tclBIND t (fun l -> tclDISPATCH (List.map k l))] *)
+ val (>>-) : 'a glist tactic -> ('a -> unit tactic) -> unit tactic
+ (* arnaud: commenter *)
+ val (>>--) : 'a glist tactic -> ('a -> 'b glist tactic) -> 'b glist tactic
(* tclBIND *)
val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+ (* arnaud: commentaire à mettre à jour *)
(* [(>>=)] (and its goal sensitive variant [(>>==)]) "binds" in one step the
tactic monad and the goal-sensitive monad.
It is strongly advised to use it everytieme an ['a Goal.sensitive tactic]
needs a bind, since it usually avoids to delay the interpretation of the
goal sensitive value to a location where it does not make sense anymore. *)
- val (>>=) : 'a Goal.sensitive tactic -> ('a -> unit tactic) -> unit tactic
- val (>>==) : 'a Goal.sensitive tactic -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+ val (>>=) : 'a glist tactic -> ('a -> unit tactic) -> unit tactic
+ val (>>==) : 'a glist tactic -> ('a -> 'b glist tactic) -> 'b glist tactic
(* tclTHEN *)
val (<*>) : unit tactic -> 'a tactic -> 'a tactic
@@ -238,6 +234,7 @@ module Notations : sig
val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
end
+
(*** Compatibility layer with <= 8.2 tactics ***)
module V82 : sig
type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
@@ -267,3 +264,21 @@ module V82 : sig
expected for a tactic obtained from {!V82.tactic} though. *)
val of_tactic : 'a tactic -> tac
end
+
+
+module Goal : sig
+
+ (* [lift_sensitive s] returns the list corresponding to the evaluation
+ of [s] on each of the focused goals *)
+ val lift : 'a Goal.sensitive -> 'a glist tactic
+
+
+ (* [lift (Goal.return x)] *)
+ val return : 'a -> 'a glist tactic
+ (* [lift Goal.concl] *)
+ val concl : Term.constr glist tactic
+ (* [lift Goal.hyps] *)
+ val hyps : Environ.named_context_val glist tactic
+ (* [lift Goal.env] *)
+ val env : Environ.env glist tactic
+end
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index d08dfd67d..a50c06b39 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -208,28 +208,37 @@ module New = struct
open Proofview.Notations
let pf_apply f =
- Goal.env >- fun env ->
- Goal.defs >- fun sigma ->
- Goal.return (f env sigma)
+ Proofview.Goal.lift begin
+ Goal.env >- fun env ->
+ Goal.defs >- fun sigma ->
+ Goal.return (f env sigma)
+ end
let of_old f =
- Goal.V82.to_sensitive f
+ Proofview.Goal.lift (Goal.V82.to_sensitive f)
- let pf_global id =
+ let pf_global_sensitive id =
Goal.hyps >- fun hyps ->
let hyps = Environ.named_context_of_val hyps in
Goal.return (Constrintern.construct_reference hyps id)
- let pf_ids_of_hyps =
+ let pf_global id =
+ Proofview.Goal.lift (pf_global_sensitive id)
+
+ let pf_ids_of_hyps_sensitive =
Goal.hyps >- fun hyps ->
- let hyps = Environ.named_context_of_val hyps in
- Goal.return (ids_of_named_context hyps)
+ let hyps = Environ.named_context_of_val hyps in
+ Goal.return (ids_of_named_context hyps)
+ let pf_ids_of_hyps =
+ Proofview.Goal.lift pf_ids_of_hyps_sensitive
let pf_get_new_id id =
- pf_ids_of_hyps >- fun ids ->
- Goal.return (next_ident_away id ids)
+ Proofview.Goal.lift begin
+ pf_ids_of_hyps_sensitive >- fun ids ->
+ Goal.return (next_ident_away id ids)
+ end
- let pf_get_hyp id =
+ let pf_get_hyp_sensitive id =
Goal.hyps >- fun hyps ->
let hyps = Environ.named_context_of_val hyps in
let sign =
@@ -237,18 +246,26 @@ module New = struct
with Not_found -> Errors.error ("No such hypothesis: " ^ (string_of_id id))
in
Goal.return sign
+ let pf_get_hyp id =
+ Proofview.Goal.lift (pf_get_hyp_sensitive id)
- let pf_get_hyp_typ id =
- pf_get_hyp id >- fun (_,_,ty) ->
+ let pf_get_hyp_typ_sensitive id =
+ pf_get_hyp_sensitive id >- fun (_,_,ty) ->
Goal.return ty
+ let pf_get_hyp_typ id =
+ Proofview.Goal.lift (pf_get_hyp_typ_sensitive id)
let pf_hyps_types =
- Goal.env >- fun env ->
- let sign = Environ.named_context env in
- Goal.return (List.map (fun (id,_,x) -> (id, x)) sign)
+ Proofview.Goal.lift begin
+ Goal.env >- fun env ->
+ let sign = Environ.named_context env in
+ Goal.return (List.map (fun (id,_,x) -> (id, x)) sign)
+ end
let pf_last_hyp =
- Goal.hyps >- fun hyps ->
- Goal.return (List.hd (Environ.named_context_of_val hyps))
+ Proofview.Goal.lift begin
+ Goal.hyps >- fun hyps ->
+ Goal.return (List.hd (Environ.named_context_of_val hyps))
+ end
end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index b3e442abc..7c96bd93b 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -134,19 +134,29 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds
(* Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
+ open Goal
+ open Proofview
+
+ val pf_apply : (env -> evar_map -> 'a) -> 'a glist tactic
+ val pf_global_sensitive : identifier -> constr sensitive
+ val pf_global : identifier -> constr glist tactic
+ val of_old : (Proof_type.goal Evd.sigma -> 'a) -> 'a glist tactic
+
+ val pf_get_new_id : identifier -> identifier glist tactic
+ val pf_ids_of_hyps_sensitive : identifier list sensitive
+ val pf_ids_of_hyps : identifier list glist tactic
+ val pf_hyps_types : (identifier * types) list glist tactic
+
+ val pf_get_hyp_sensitive : identifier -> named_declaration sensitive
+ val pf_get_hyp : identifier -> named_declaration glist tactic
+ val pf_get_hyp_typ_sensitive : identifier -> types sensitive
+ val pf_get_hyp_typ : identifier -> types glist tactic
+ val pf_last_hyp : named_declaration glist tactic
+end
+
- val pf_apply : (env -> evar_map -> 'a) -> 'a Goal.sensitive
- val pf_global : identifier -> constr Goal.sensitive
- val of_old : (Proof_type.goal Evd.sigma -> 'a) -> 'a Goal.sensitive
- val pf_get_new_id : identifier -> identifier Goal.sensitive
- val pf_ids_of_hyps : identifier list Goal.sensitive
- val pf_hyps_types : (identifier * types) list Goal.sensitive
- val pf_get_hyp : identifier -> named_declaration Goal.sensitive
- val pf_get_hyp_typ : identifier -> types Goal.sensitive
- val pf_last_hyp : named_declaration Goal.sensitive
-end
diff --git a/tactics/auto.ml b/tactics/auto.ml
index c770df051..8115376c9 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1276,13 +1276,13 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
let rec trivial_fail_db dbg mod_delta db_list local_db =
let intro_tac =
Tacticals.New.tclTHEN (dbg_intro dbg)
- ( Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ ( Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
Tacmach.New.pf_last_hyp >>- fun hyp ->
let hintl = make_resolve_hyp env sigma hyp
in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db))
in
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
Tacticals.New.tclFIRST
((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac::
(List.map Tacticals.New.tclCOMPLETE
@@ -1434,7 +1434,7 @@ let search d n mod_delta db_list local_db =
if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d))
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
- ( Goal.concl >>- fun concl ->
+ ( Proofview.Goal.concl >>- fun concl ->
let d' = incr_dbg d in
Tacticals.New.tclFIRST
(List.map
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 329198ccc..8a09ff789 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -114,7 +114,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
(* let's check at once if id exists (to raise the appropriate error) *)
- Goal.sensitive_list_map Tacmach.New.pf_get_hyp idl >>- fun _ ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive idl) >>- fun _ ->
let general_rewrite_in id =
let id = ref id in
let to_be_cleared = ref false in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 71f8c2ba8..f1ebdc638 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -83,9 +83,9 @@ let rec eq_constr_mod_evars x y =
| _, _ -> compare_constr eq_constr_mod_evars x y
let progress_evars t =
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
let check =
- Goal.concl >>- fun newconcl ->
+ Proofview.Goal.concl >>- fun newconcl ->
if eq_constr_mod_evars concl newconcl
then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)")
else Proofview.tclUNIT ()
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 565f30cfb..ed1661910 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -44,12 +44,12 @@ let filter_hyp f tac =
| [] -> raise Not_found
| (id,_,t)::rest when f t -> tac id
| _::rest -> seek rest in
- Goal.hyps >>- fun hyps ->
+ Proofview.Goal.hyps >>- fun hyps ->
seek (Environ.named_context_of_val hyps)
let contradiction_context =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let rec seek_neg l = match l with
| [] -> Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
| (id,_,typ)::rest ->
@@ -69,7 +69,7 @@ let contradiction_context =
| e -> Proofview.tclZERO e
end)
| _ -> seek_neg rest in
- Goal.hyps >>- fun hyps ->
+ Proofview.Goal.hyps >>- fun hyps ->
let hyps = Environ.named_context_of_val hyps in
seek_neg hyps
@@ -79,8 +79,8 @@ let is_negation_of env sigma typ t =
| _ -> false
let contradiction_term (c,lbind as cl) =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
let typ = type_of c in
let _, ccl = splay_prod env sigma typ in
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 0e30daf6d..a784264f0 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -111,7 +111,7 @@ let head_in =
let decompose_these c l =
let indl = (*List.map inductive_of*) l in
- head_in >>- fun head_in ->
+ Proofview.Goal.lift head_in >>- fun head_in ->
general_decompose (fun (_,t) -> head_in indl t) c
let decompose_nonrec c =
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index ac6e944fb..cc6547bc3 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -130,7 +130,7 @@ let solveArg eqonleft op a1 a2 tac =
let solveEqBranch rectype =
Proofview.tclORELSE
begin
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) ->
let (mib,mip) = Global.lookup_inductive rectype in
let nparams = mib.mind_nparams in
@@ -155,7 +155,7 @@ let hd_app c = match kind_of_term c with
let decideGralEquality =
Proofview.tclORELSE
begin
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
match_eqdec concl >= fun eqonleft,_,c1,c2,typ ->
Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>- fun headtyp ->
begin match kind_of_term headtyp with
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 897285f25..0ad306aba 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -224,11 +224,11 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
let cs =
Goal.env >- fun env ->
Goal.concl >- fun concl ->
- Tacmach.New.of_old (
+ Goal.V82.to_sensitive (
(if not all then instantiate_lemma else instantiate_lemma_all frzevars)
env ) >- fun instantiate_lemma ->
let typ =
- match cls with None -> Goal.return concl | Some id -> Tacmach.New.pf_get_hyp_typ id
+ match cls with None -> Goal.return concl | Some id -> Tacmach.New.pf_get_hyp_typ_sensitive id
in
typ >- fun typ ->
Goal.return (instantiate_lemma c t l l2r typ)
@@ -240,7 +240,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
(Proofview.V82.tactic (general_elim_clause with_evars frzevars cls c elim)))
tac
in
- cs >>- fun cs ->
+ Proofview.Goal.lift cs >>- fun cs ->
if firstonly then
Tacticals.New.tclFIRST (List.map try_clause cs)
else
@@ -324,7 +324,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
| _ -> assert false
let type_of_clause = function
- | None -> Goal.concl
+ | None -> Proofview.Goal.concl
| Some id -> Tacmach.New.pf_get_hyp_typ id
let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
@@ -359,8 +359,8 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
if occs != AllOccurrences then (
rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
else
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let ctype = get_type_of env sigma c in
let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
match match_with_equality_type t with
@@ -449,10 +449,10 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
(* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
let ids =
let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
- Tacmach.New.pf_ids_of_hyps >- fun ids_of_hyps ->
+ Tacmach.New.pf_ids_of_hyps_sensitive >- fun ids_of_hyps ->
Goal.return (Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps)
in
- ids >>- fun ids ->
+ Proofview.Goal.lift ids >>- fun ids ->
do_hyps_atleastonce ids
in
if cl.concl_occs == NoOccurrences then do_hyps else
@@ -465,8 +465,8 @@ type delayed_open_constr_with_bindings =
let general_multi_multi_rewrite with_evars l cl tac =
let do1 l2r f =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let sigma,c = f env sigma in
Tacticals.New.tclWITHHOLES with_evars
(general_multi_rewrite l2r with_evars ?tac c) sigma cl in
@@ -846,8 +846,8 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
- Goal.env >>- fun env ->
- Goal.concl >>- fun concl ->
+ Proofview.Goal.env >>- fun env ->
+ Proofview.Goal.concl >>- fun concl ->
match find_positions env sigma t1 t2 with
| Inr _ ->
Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality."))
@@ -872,9 +872,9 @@ let onEquality with_evars tac (c,lbindc) =
(tac (eq,eqn,eq_args) eq_clause')
let onNegatedEquality with_evars tac =
- Goal.concl >>- fun ccl ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.concl >>- fun ccl ->
+ Proofview.Goal.env >>- fun env ->
match kind_of_term (hnf_constr env sigma ccl) with
| Prod (_,t,u) when is_empty_type u ->
Tacticals.New.tclTHEN introf
@@ -1265,7 +1265,7 @@ let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id)))
let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>- fun sort ->
let sigma = clause.evd in
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
match find_positions env sigma t1 t2 with
| Inl (cpath, (_,dirn), _) ->
discr_positions env sigma u clause cpath dirn sort
@@ -1509,9 +1509,9 @@ let is_eq_x gl x (id,_,c) =
erase hyp and x; proceed by generalizing all dep hyps *)
let subst_one dep_proof_ok x (hyp,rhs,dir) =
- Goal.env >>- fun env ->
- Goal.hyps >>- fun hyps ->
- Goal.concl >>- fun concl ->
+ Proofview.Goal.env >>- fun env ->
+ Proofview.Goal.hyps >>- fun hyps ->
+ Proofview.Goal.concl >>- fun concl ->
let hyps = Environ.named_context_of_val hyps in
(* The set of hypotheses using x *)
let depdecls =
@@ -1554,7 +1554,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
au bon endroit. Il faut convertir test en une Proofview.tactic
pour la gestion des exceptions. *)
let subst_one_var dep_proof_ok x =
- Goal.hyps >>- fun hyps ->
+ Proofview.Goal.hyps >>- fun hyps ->
let hyps = Environ.named_context_of_val hyps in
Tacmach.New.pf_get_hyp x >>- fun (_,xval,_) ->
(* If x has a body, simply replace x with body and clear x *)
@@ -1651,7 +1651,7 @@ let rewrite_multi_assumption_cond cond_eq_term cl =
with | Failure _ | UserError _ -> arec rest
end
in
- Goal.hyps >>- fun hyps ->
+ Proofview.Goal.hyps >>- fun hyps ->
let hyps = Environ.named_context_of_val hyps in
arec hyps
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 1234fe72b..80b06b2fb 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -53,8 +53,8 @@ let instantiate n (ist,rawc) ido gl =
open Proofview.Notations
let let_evar name typ =
let src = (Loc.ghost,Evar_kinds.GoalEvar) in
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let sigma',evar = Evarutil.new_evar sigma env ~src typ in
Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
(Tactics.letin_tac None name evar None Locusops.nowhere)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ae0bdfe44..71b2bdfb6 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -116,7 +116,7 @@ END
open Proofview.Notations
let discrHyp id =
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
discr_main {it = Term.mkVar id,NoBindings; sigma = sigma;}
let injection_main c =
@@ -161,7 +161,7 @@ TACTIC EXTEND einjection_as
END
let injHyp id =
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
injection_main { it = Term.mkVar id,NoBindings; sigma = sigma; }
TACTIC EXTEND dependent_rewrite
@@ -667,8 +667,8 @@ let mkCaseEq a : unit Proofview.tactic =
Tacticals.New.tclTHENLIST
[Proofview.V82.tactic (Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
begin
- Goal.concl >>- fun concl ->
- Goal.env >>- fun env ->
+ Proofview.Goal.concl >>- fun concl ->
+ Proofview.Goal.env >>- fun env ->
Proofview.V82.tactic begin
change_in_concl None
(Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)
@@ -678,7 +678,7 @@ let mkCaseEq a : unit Proofview.tactic =
let case_eq_intros_rewrite x =
- begin
+ Proofview.Goal.lift begin
Goal.concl >- fun concl ->
Goal.return (nb_prod concl)
end >>- fun n ->
@@ -686,7 +686,7 @@ let case_eq_intros_rewrite x =
Tacticals.New.tclTHENLIST [
mkCaseEq x;
begin
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
Tacmach.New.pf_ids_of_hyps >>- fun hyps ->
let n' = nb_prod concl in
Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) >>- fun h ->
@@ -721,7 +721,7 @@ let destauto_in id =
destauto ctype
TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Goal.concl >>- fun concl -> destauto concl ]
+| [ "destauto" ] -> [ Proofview.Goal.concl >>- fun concl -> destauto concl ]
| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
END
diff --git a/tactics/inv.ml b/tactics/inv.ml
index c9d54f84f..644f527a0 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -443,9 +443,9 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
let raw_inversion inv_kind id status names =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
- Goal.concl >>- fun concl ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
+ Proofview.Goal.concl >>- fun concl ->
let c = mkVar id in
Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>- fun reduce_to_atomic_ind ->
Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
@@ -522,11 +522,11 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
* back to their places in the hyp-list. *)
let invIn k names ids id =
- Goal.sensitive_list_map Tacmach.New.pf_get_hyp ids >>- fun hyps ->
- Goal.concl >>- fun concl ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>- fun hyps ->
+ Proofview.Goal.concl >>- fun concl ->
let nb_prod_init = nb_prod concl in
let intros_replace_ids =
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
let nb_of_new_hyp =
nb_prod concl - (List.length hyps + nb_prod_init)
in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 00cf4e997..786f92736 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -284,9 +284,9 @@ let lemInv id c gls =
let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
let lemInvIn id c ids =
- Goal.sensitive_list_map Tacmach.New.pf_get_hyp ids >>- fun hyps ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>- fun hyps ->
let intros_replace_ids =
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
let nb_of_new_hyp = nb_prod concl - List.length ids in
if nb_of_new_hyp < 1 then
intros_replacing ids
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 4a601e41e..61db456dd 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -315,7 +315,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) : unit Proofview.tactic =
(* let in without holes in the body => possibly dependent intro *)
| LetIn (Name id,c1,t1,c2), _ when not (isMeta (strip_outer_cast c1)) ->
- Goal.concl >>- fun c ->
+ Proofview.Goal.concl >>- fun c ->
let newc = mkNamedLetIn id c1 t1 c in
Tacticals.New.tclTHEN
(Proofview.V82.tactic (change_in_concl None newc))
@@ -382,8 +382,8 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) : unit Proofview.tactic =
(* Et finalement la tactique refine elle-même : *)
let refine (evd,c) =
- Goal.defs >>- fun sigma ->
- Goal.env >>- fun env ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals env evd in
let c = Evarutil.nf_evar evd c in
let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 65f29498c..fb9ca2507 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1326,8 +1326,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
++ fnl () ++ Himsg.explain_typeclass_error env e)))
- in
- Proofview.tclGOALBINDU info (fun i -> treat i)
+ in Proofview.Notations.(>>-) (Proofview.Goal.lift info) (fun i -> treat i)
let newtactic_init_setoid () =
try init_setoid (); Proofview.tclUNIT ()
@@ -1766,9 +1765,9 @@ let not_declared env ty rel =
str ty ++ str" relation. Maybe you need to require the Setoid library")
let setoid_proof ty fn fallback =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
- Goal.concl >>- fun concl ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
+ Proofview.Goal.concl >>- fun concl ->
Proofview.tclORELSE
begin
try
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 04624e1a1..45ece0ba4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -979,8 +979,7 @@ type 'a _matching_result =
{ s_sub : bound_ident_map * patvar_map ;
s_ctx : 'a ;
s_nxt : 'a matching_result }
-and 'a matching_result = 'a _matching_result Goal.sensitive Proofview.tactic
-
+and 'a matching_result = 'a _matching_result Proofview.glist Proofview.tactic
type 'a _extended_matching_result =
{ e_ctx : 'a;
@@ -1067,12 +1066,12 @@ let extend_gl_hyps { it=gl ; sigma=sigma } sign =
Goal.V82.new_goal_with sigma gl sign
(* Interprets an l-tac expression into a value *)
-let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument Goal.sensitive Proofview.tactic =
+let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument Proofview.glist Proofview.tactic =
let value_interp ist = match tac with
(* Immediate evaluation *)
| TacFun (it,body) ->
let v = VFun (extract_trace ist,ist.lfun,it,body) in
- Proofview.tclUNIT (Goal.return (of_tacvalue v))
+ (Proofview.Goal.return (of_tacvalue v))
| TacLetIn (true,l,u) -> interp_letrec ist l u
| TacLetIn (false,l,u) -> interp_letin ist l u
| TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr
@@ -1081,7 +1080,7 @@ let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument Goal.sens
(* Delayed evaluation *)
| t ->
let v = VFun (extract_trace ist,ist.lfun,[],t) in
- Proofview.tclUNIT (Goal.return (of_tacvalue v))
+ (Proofview.Goal.return (of_tacvalue v))
in check_for_interrupt ();
match curr_debug ist with
(* arnaud: todo: debug
@@ -1140,8 +1139,8 @@ and force_vrec ist v =
let v = to_tacvalue v in
match v with
| VRec (lfun,body) -> val_interp {ist with lfun = !lfun} body
- | v -> Proofview.tclUNIT (Goal.return (of_tacvalue v))
- else Proofview.tclUNIT (Goal.return v)
+ | v -> (Proofview.Goal.return (of_tacvalue v))
+ else (Proofview.Goal.return v)
and interp_ltac_reference loc' mustbetac ist = function
| ArgVar (loc,id) ->
@@ -1151,7 +1150,7 @@ and interp_ltac_reference loc' mustbetac ist = function
in
force_vrec ist v >>== fun v ->
let v = propagate_trace ist loc id v in
- if mustbetac then Proofview.tclUNIT (Goal.return (coerce_to_tactic loc id v)) else Proofview.tclUNIT (Goal.return v)
+ if mustbetac then (Proofview.Goal.return (coerce_to_tactic loc id v)) else (Proofview.Goal.return v)
| ArgArg (loc,r) ->
let ids = extract_ids [] ist.lfun in
let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in
@@ -1164,46 +1163,45 @@ and interp_tacarg ist arg =
let tac_of_old f =
Tacmach.New.of_old f >>-- fun (sigma,v) ->
Proofview.V82.tactic (tclEVARS sigma) <*>
- Proofview.tclUNIT (Goal.return v)
+ (Proofview.Goal.return v)
in
match arg with
| TacGeneric arg ->
- Goal.defs >>-- fun sigma ->
tac_of_old (fun gl ->
- Geninterp.generic_interp ist { gl with sigma = sigma } arg)
+ Geninterp.generic_interp ist gl arg)
| Reference r -> interp_ltac_reference dloc false ist r
| ConstrMayEval c ->
tac_of_old (fun gl -> interp_constr_may_eval ist gl c) >>== fun c_interp ->
- Proofview.tclUNIT (Goal.return (Value.of_constr c_interp))
+ (Proofview.Goal.return (Value.of_constr c_interp))
| MetaIdArg (loc,_,id) -> assert false
| TacCall (loc,r,[]) ->
interp_ltac_reference loc true ist r
| TacCall (loc,f,l) ->
- interp_ltac_reference loc true ist f >>== fun fv ->
Proofview.tclEVARMAP >= fun sigma ->
+ interp_ltac_reference loc true ist f >>== fun fv ->
List.fold_right begin fun a acc ->
interp_tacarg ist a >>== fun a_interp ->
- acc >>== fun acc -> Proofview.tclUNIT (Goal.return (a_interp::acc))
- end l (Proofview.tclUNIT (Goal.return [])) >>== fun largs ->
+ acc >>== fun acc -> (Proofview.Goal.return (a_interp::acc))
+ end l ((Proofview.Goal.return [])) >>== fun largs ->
interp_app loc ist fv largs
| TacExternal (loc,com,req,la) ->
List.fold_right begin fun a acc ->
interp_tacarg ist a >>== fun a_interp ->
- acc >>== fun acc -> Proofview.tclUNIT (Goal.return (a_interp::acc))
- end la (Proofview.tclUNIT (Goal.return [])) >>== fun la_interp ->
+ acc >>== fun acc -> (Proofview.Goal.return (a_interp::acc))
+ end la ((Proofview.Goal.return [])) >>== fun la_interp ->
tac_of_old (fun gl -> interp_external loc ist { gl with sigma=project gl } com req la_interp)
| TacFreshId l ->
Tacmach.New.of_old (fun gl -> pf_interp_fresh_id ist gl l) >>-- fun id ->
- Proofview.tclUNIT (Goal.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id)))
+ (Proofview.Goal.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id)))
| Tacexp t -> val_interp ist t
| TacDynamic(_,t) ->
let tg = (Dyn.tag t) in
if String.equal tg "tactic" then
val_interp ist (tactic_out t ist)
else if String.equal tg "value" then
- Proofview.tclUNIT (Goal.return (value_out t))
+ (Proofview.Goal.return (value_out t))
else if String.equal tg "constr" then
- Proofview.tclUNIT (Goal.return (Value.of_constr (constr_out t)))
+ (Proofview.Goal.return (Value.of_constr (constr_out t)))
else
Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp"
(str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")
@@ -1254,9 +1252,9 @@ and interp_app loc ist fv largs =
(fun () ->
str"evaluation returns"++fnl()++pr_value (Some (pf_env gl)) v);
*)
- if List.is_empty lval then Proofview.tclUNIT (Goal.return v) else interp_app loc ist v lval
+ if List.is_empty lval then (Proofview.Goal.return v) else interp_app loc ist v lval
else
- Proofview.tclUNIT (Goal.return (of_tacvalue (VFun(trace,newlfun,lvar,body))))
+ Proofview.Goal.return (of_tacvalue (VFun(trace,newlfun,lvar,body)))
| _ -> fail
else fail
@@ -1286,9 +1284,9 @@ and eval_with_fail ist is_lazy tac =
lfun = lfun;
extra = TacStore.set ist.extra f_trace trace; } in
let tac = eval_tactic ist t in
- catch_error_tac trace (tac <*> Proofview.tclUNIT (Goal.return (of_tacvalue VRTactic)))
- | _ -> Proofview.tclUNIT (Goal.return v)
- else Proofview.tclUNIT (Goal.return v))
+ catch_error_tac trace (tac <*> Proofview.Goal.return (of_tacvalue VRTactic))
+ | _ -> Proofview.Goal.return v
+ else Proofview.Goal.return v)
end
begin function
(** FIXME: Should we add [Errors.push]? *)
@@ -1318,24 +1316,19 @@ and interp_letin ist llc u =
interp_tacarg ist body >>== fun v ->
acc >>== fun acc ->
let () = check_is_value v in
- Proofview.tclUNIT (Goal.return (Id.Map.add id v acc))
+ Proofview.Goal.return (Id.Map.add id v acc)
in
- List.fold_right fold llc (Proofview.tclUNIT (Goal.return ist.lfun)) >>== fun lfun ->
+ List.fold_right fold llc (Proofview.Goal.return ist.lfun) >>== fun lfun ->
let ist = { ist with lfun } in
val_interp ist u
(* Interprets the Match Context expressions *)
and interp_match_goal ist lz lr lmr =
- (* arnaud: on va prier pour que je n'ai pas besoin de faire ça,
- sinon, je fais un truc ad-hoc
- let (gl,sigma) = Goal.V82.nf_evar (project goal) (sig_it goal) in
- let goal = { it = gl ; sigma = sigma; } in
- *)
- Goal.hyps >>-- fun hyps ->
+ Proofview.Goal.hyps >>-- fun hyps ->
let hyps = Environ.named_context_of_val hyps in
let hyps = if lr then List.rev hyps else hyps in
- Goal.concl >>-- fun concl ->
- Goal.env >>-- fun env ->
+ Proofview.Goal.concl >>-- fun concl ->
+ Proofview.Goal.env >>-- fun env ->
let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps =
let rec match_next_pattern next = match IStream.peek next with
| None -> Proofview.tclZERO PatternMatchingFailure
@@ -1418,7 +1411,7 @@ and interp_match_goal ist lz lr lmr =
(* Tries to match the hypotheses in a Match Context *)
and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
- Goal.env >>-- fun env ->
+ Proofview.Goal.env >>-- fun env ->
let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function
| hyp_pat::tl ->
let (hypname, _, pat as hyp_pat) =
@@ -1617,8 +1610,8 @@ and interp_match ist lz constr lmr =
Proofview.tclZERO e
end
end >>== fun csr ->
- Goal.env >>-- fun env ->
Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>-- fun env ->
let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
Proofview.tclORELSE
(apply_match ist csr ilr)
@@ -1629,7 +1622,7 @@ and interp_match ist lz constr lmr =
end >>== fun res ->
debugging_step ist (fun () ->
str "match expression returns " ++ pr_value (Some env) res);
- Proofview.tclUNIT (Goal.return res)
+ (Proofview.Goal.return res)
(* Interprets tactic expressions : returns a "constr" *)
and interp_ltac_constr ist e =
@@ -1646,7 +1639,7 @@ and interp_ltac_constr ist e =
| e -> Proofview.tclZERO e
end
end >>== fun result ->
- Goal.env >>-- fun env ->
+ Proofview.Goal.env >>-- fun env ->
let result = Value.normalize result in
try
let cresult = coerce_to_closed_constr env result in
@@ -1654,9 +1647,9 @@ and interp_ltac_constr ist e =
Pptactic.pr_glob_tactic env e ++ fnl() ++
str " has value " ++ fnl() ++
pr_constr_env env cresult);
- Proofview.tclUNIT (Goal.return cresult)
+ (Proofview.Goal.return cresult)
with CannotCoerceTo _ ->
- Goal.env >>-- fun env ->
+ Proofview.Goal.env >>-- fun env ->
Proofview.tclZERO (UserError ( "",
errorlabstrm ""
(str "Must evaluate to a closed term" ++ fnl() ++
@@ -1677,7 +1670,7 @@ and interp_atomic ist tac =
| TacIntrosUntil hyp ->
h_intros_until (interp_quantified_hypothesis ist hyp)
| TacIntroMove (ido,hto) ->
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>- fun mloc ->
h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
| TacAssumption -> Proofview.V82.tactic h_assumption
@@ -1706,8 +1699,8 @@ and interp_atomic ist tac =
gl
end
| TacApply (a,ev,cb,cl) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let sigma, l =
List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
in
@@ -1719,8 +1712,8 @@ and interp_atomic ist tac =
h_apply_in a ev l cl) in
Tacticals.New.tclWITHHOLES ev tac sigma l
| TacElim (ev,cb,cbo) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
Tacticals.New.tclWITHHOLES ev (h_elim ev cb) sigma cbo
@@ -1733,8 +1726,8 @@ and interp_atomic ist tac =
gl
end
| TacCase (ev,cb) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
Tacticals.New.tclWITHHOLES ev (h_case ev) sigma cb
| TacCaseType c ->
@@ -1746,10 +1739,10 @@ and interp_atomic ist tac =
gl
end
| TacFix (idopt,n) ->
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n)
| TacMutualFix (id,n,l) ->
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
Proofview.V82.tactic begin fun gl ->
let f sigma (id,n,c) =
let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
@@ -1766,10 +1759,10 @@ and interp_atomic ist tac =
gl
end
| TacCofix idopt ->
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt))
| TacMutualCofix (id,l) ->
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
Proofview.V82.tactic begin fun gl ->
let f sigma (id,c) =
let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
@@ -1794,8 +1787,8 @@ and interp_atomic ist tac =
gl
end
| TacAssert (t,ipat,c) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>- fun patt ->
Tacticals.New.tclTHEN
@@ -1803,8 +1796,8 @@ and interp_atomic ist tac =
(Tactics.forward (Option.map (interp_tactic ist) t)
(Option.map patt ipat) c)
| TacGeneralize cl ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
Proofview.V82.tactic begin fun gl ->
let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
tclWITHHOLES false (h_generalize_gen) sigma cl gl
@@ -1818,8 +1811,8 @@ and interp_atomic ist tac =
gl
end
| TacLetTac (na,c,clp,b,eqpat) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) >>- fun clp ->
Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) >>- fun eqpat ->
if Locusops.is_nowhere clp then
@@ -1835,14 +1828,14 @@ and interp_atomic ist tac =
(* Automation tactics *)
| TacTrivial (debug,lems,l) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
Auto.h_trivial ~debug
(interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
| TacAuto (debug,n,lems,l) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
(interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
@@ -1851,11 +1844,11 @@ and interp_atomic ist tac =
| TacSimpleInductionDestruct (isrec,h) ->
h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
| TacInductionDestruct (isrec,ev,(l,el,cls)) ->
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
let l =
Goal.sensitive_list_map begin fun (c,(ipato,ipats)) ->
- Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) >- fun c ->
- Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >- fun interp_intro_pattern ->
+ Goal.V82.to_sensitive (fun gl -> interp_induction_arg ist gl c) >- fun c ->
+ Goal.V82.to_sensitive (fun gl -> interp_intro_pattern ist gl) >- fun interp_intro_pattern ->
Goal.return begin
c,
(Option.map interp_intro_pattern ipato,
@@ -1863,8 +1856,8 @@ and interp_atomic ist tac =
end
end l
in
- l >>- fun l ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.lift l >>- fun l ->
let sigma,el =
Option.fold_map (interp_constr_with_bindings ist env) sigma el in
Tacmach.New.of_old (fun gl -> interp_clause ist gl) >>- fun interp_clause ->
@@ -1891,8 +1884,8 @@ and interp_atomic ist tac =
(Proofview.V82.tactic (tclEVARS sigma))
(Elim.h_decompose l c_interp)
| TacSpecialize (n,cb) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
Proofview.V82.tactic begin fun gl ->
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
tclWITHHOLES false (h_specialize n) sigma cb gl
@@ -1920,7 +1913,7 @@ and interp_atomic ist tac =
h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) gl
end
| TacRename l ->
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
Proofview.V82.tactic begin fun gl ->
h_rename (List.map (fun (id1,id2) ->
interp_hyp ist gl id1,
@@ -1934,25 +1927,25 @@ and interp_atomic ist tac =
(* Constructors *)
| TacLeft (ev,bl) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let sigma, bl = interp_bindings ist env sigma bl in
Tacticals.New.tclWITHHOLES ev (h_left ev) sigma bl
| TacRight (ev,bl) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let sigma, bl = interp_bindings ist env sigma bl in
Tacticals.New.tclWITHHOLES ev (h_right ev) sigma bl
| TacSplit (ev,_,bll) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
Tacticals.New.tclWITHHOLES ev (h_split ev) sigma bll
| TacAnyConstructor (ev,t) ->
Tactics.any_constructor ev (Option.map (interp_tactic ist) t)
| TacConstructor (ev,n,bl) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let sigma, bl = interp_bindings ist env sigma bl in
Tacticals.New.tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl
@@ -1986,8 +1979,8 @@ and interp_atomic ist tac =
gl
end
| TacChange (Some op,c,cl) ->
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
Proofview.V82.tactic begin fun gl ->
let sign,op = interp_typed_pattern ist env sigma op in
(* spiwack: (2012/04/18) the evar_map output by pf_interp_constr
@@ -2030,11 +2023,11 @@ and interp_atomic ist tac =
Equality.general_multi_multi_rewrite ev l cl
(Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)
| TacInversion (DepInversion (k,c,ids),hyp) ->
- Goal.defs >>- fun sigma ->
- begin match c with
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.lift begin match c with
| None -> Goal.return (sigma , None)
| Some c ->
- Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >- fun (sigma,c_interp) ->
+ Goal.V82.to_sensitive (fun gl -> pf_interp_constr ist gl c) >- fun (sigma,c_interp) ->
Goal.return (sigma , Some c_interp)
end >>- fun (sigma,c_interp) ->
Tacmach.New.of_old (interp_intro_pattern ist) >>- fun interp_intro_pattern ->
@@ -2060,7 +2053,7 @@ and interp_atomic ist tac =
(* For extensions *)
| TacExtend (loc,opn,l) ->
- Goal.defs >>- fun goal_sigma ->
+ Proofview.tclEVARMAP >= fun goal_sigma ->
let tac = lookup_tactic opn in
Tacmach.New.of_old begin fun gl ->
List.fold_right begin fun a (sigma,acc) ->
@@ -2071,38 +2064,34 @@ and interp_atomic ist tac =
Proofview.V82.tactic (tclEVARS sigma) <*>
tac args ist
| TacAlias (loc,s,l,(_,body)) ->
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
let rec f x = match genarg_tag x with
| IntOrVarArgType ->
- Proofview.tclUNIT (Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)))
+ (Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)))
| IdentArgType b ->
- Proofview.tclUNIT begin
+ Proofview.Goal.lift begin
Goal.return (value_of_ident (interp_fresh_ident ist env
(out_gen (glbwit (wit_ident_gen b)) x)))
end
| VarArgType ->
- Proofview.tclUNIT
- (Tacmach.New.of_old (fun gl -> mk_hyp_value ist gl (out_gen (glbwit wit_var) x)))
+ Tacmach.New.of_old (fun gl -> mk_hyp_value ist gl (out_gen (glbwit wit_var) x))
| RefArgType ->
- Proofview.tclUNIT begin
- Tacmach.New.of_old (fun gl ->
- Value.of_constr (constr_of_global
- (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))))
- end
-
+ Tacmach.New.of_old (fun gl ->
+ Value.of_constr (constr_of_global
+ (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))))
| GenArgType -> f (out_gen (glbwit wit_genarg) x)
| ConstrArgType ->
Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) >>-- fun (sigma,v) ->
Proofview.V82.tactic (tclEVARS sigma) <*>
- Proofview.tclUNIT (Goal.return v)
+ (Proofview.Goal.return v)
| OpenConstrArgType false ->
Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) >>-- fun (sigma,v) ->
Proofview.V82.tactic (tclEVARS sigma) <*>
- Proofview.tclUNIT (Goal.return v)
+ (Proofview.Goal.return v)
| ConstrMayEvalArgType ->
Tacmach.New.of_old (fun gl -> interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x)) >>-- fun (sigma,c_interp) ->
Proofview.V82.tactic (tclEVARS sigma) <*>
- Proofview.tclUNIT (Goal.return (Value.of_constr c_interp))
+ Proofview.Goal.return (Value.of_constr c_interp)
| ListArgType ConstrArgType ->
let wit = glbwit (wit_list wit_constr) in
Tacmach.New.of_old begin fun gl ->
@@ -2112,43 +2101,43 @@ and interp_atomic ist tac =
end (out_gen wit x) (project gl,[])
end >>-- fun (sigma,l_interp) ->
Proofview.V82.tactic (tclEVARS sigma) <*>
- Proofview.tclUNIT (Goal.return (in_gen (topwit (wit_list wit_genarg)) l_interp))
+ (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) l_interp))
| ListArgType VarArgType ->
let wit = glbwit (wit_list wit_var) in
- Proofview.tclUNIT (Tacmach.New.of_old (fun gl ->
+ Tacmach.New.of_old (fun gl ->
let ans = List.map (mk_hyp_value ist gl) (out_gen wit x) in
in_gen (topwit (wit_list wit_genarg)) ans
- ))
+ )
| ListArgType IntOrVarArgType ->
let wit = glbwit (wit_list wit_int_or_var) in
let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
- Proofview.tclUNIT (Goal.return (in_gen (topwit (wit_list wit_genarg)) ans))
+ (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans))
| ListArgType (IdentArgType b) ->
let wit = glbwit (wit_list (wit_ident_gen b)) in
let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
let ans = List.map mk_ident (out_gen wit x) in
- Proofview.tclUNIT (Goal.return (in_gen (topwit (wit_list wit_genarg)) ans))
+ (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans))
| ListArgType t ->
(* arnaud: unsafe, faire avec des combinateurs. Dans la version originale c'était juste [Genarg.app_list f x] *)
fold_list begin fun a l ->
f a >>== fun a' ->
l >>== fun l ->
- Proofview.tclUNIT (Goal.return (a'::l))
- end x (Proofview.tclUNIT (Goal.return [])) >>== fun l ->
- Proofview.tclUNIT (Goal.return (in_gen
- (topwit (wit_list (Obj.magic t)))
- l))
+ Proofview.Goal.return (a'::l)
+ end x (Proofview.Goal.return []) >>== fun l ->
+ Proofview.Goal.return (in_gen
+ (topwit (wit_list (Obj.magic t)))
+ l)
| ExtraArgType _ ->
(** Special treatment of tactics *)
if has_type x (glbwit wit_tactic) then
let tac = out_gen (glbwit wit_tactic) x in
val_interp ist tac >>== fun v ->
- Proofview.tclUNIT (Goal.return v)
+ Proofview.Goal.return v
else
Tacmach.New.of_old (fun gl ->
Geninterp.generic_interp ist gl x) >>-- fun (newsigma,v) ->
Proofview.V82.tactic (tclEVARS newsigma) <*>
- Proofview.tclUNIT (Goal.return v)
+ Proofview.Goal.return v
| QuantHypArgType | RedExprArgType
| OpenConstrArgType _ | ConstrWithBindingsArgType
| BindingsArgType
@@ -2158,9 +2147,9 @@ and interp_atomic ist tac =
let addvar (x, v) accu =
accu >>== fun accu ->
f v >>== fun v ->
- Proofview.tclUNIT (Goal.return (Id.Map.add x v accu))
+ Proofview.Goal.return (Id.Map.add x v accu)
in
- List.fold_right addvar l (Proofview.tclUNIT (Goal.return ist.lfun)) >>= fun lfun ->
+ List.fold_right addvar l (Proofview.Goal.return ist.lfun) >>= fun lfun ->
let trace = push_trace (loc,LtacNotationCall s) ist in
let ist = {
lfun = lfun;
@@ -2182,8 +2171,8 @@ let eval_tactic t =
let interp_tac_gen lfun avoid_ids debug t =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let extra = TacStore.set TacStore.empty f_debug debug in
let extra = TacStore.set extra f_avoid_ids avoid_ids in
let ist = { lfun = lfun; extra = extra } in
@@ -2203,8 +2192,8 @@ let eval_ltac_constr t =
(* Used to hide interpretation for pretty-print, now just launch tactics *)
let hide_interp t ot =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
gsigma = sigma; genv = env } in
let te = intern_pure_tactic ist t in
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index dffea3e65..9eb4b3650 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -77,10 +77,10 @@ val interp_genarg : interp_sign -> goal sigma -> glob_generic_argument ->
Evd.evar_map * typed_generic_argument
(** Interprets any expression *)
-val val_interp : interp_sign -> glob_tactic_expr -> value Goal.sensitive Proofview.tactic
+val val_interp : interp_sign -> glob_tactic_expr -> value Proofview.glist Proofview.tactic
(** Interprets an expression that evaluates to a constr *)
-val interp_ltac_constr : interp_sign -> glob_tactic_expr -> constr Goal.sensitive Proofview.tactic
+val interp_ltac_constr : interp_sign -> glob_tactic_expr -> constr Proofview.glist Proofview.tactic
(** Interprets redexp arguments *)
val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
@@ -106,7 +106,7 @@ val interp_tac_gen : value Id.Map.t -> Id.t list ->
val interp : raw_tactic_expr -> unit Proofview.tactic
-val eval_ltac_constr : raw_tactic_expr -> constr Goal.sensitive Proofview.tactic
+val eval_ltac_constr : raw_tactic_expr -> constr Proofview.glist Proofview.tactic
(** Hides interpretation for pretty-print *)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 412ed119f..b9a104b64 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -509,13 +509,16 @@ module New = struct
Proofview.V82.tactic (Refiner.tclEVARS sigma) <*> tac x <*> check_evars_if
let nthDecl m =
- Goal.hyps >- fun hyps ->
- let hyps = Environ.named_context_of_val hyps in
- try Goal.return (List.nth hyps (m-1))
- with Failure _ -> error "No such assumption."
+ Proofview.Goal.hyps >>== fun hyps ->
+ try
+ let hyps = Environ.named_context_of_val hyps in
+ (Proofview.Goal.return (List.nth hyps (m-1)))
+ with Failure _ -> tclZERO (UserError ("" , Pp.str"No such assumption."))
- let nthHypId m = nthDecl m >- fun (id,_,_) -> Goal.return id
- let nthHyp m = nthHypId m >- fun id -> Goal.return (mkVar id)
+ let nthHypId m = nthDecl m >>== fun (id,_,_) ->
+ Proofview.Goal.return id
+ let nthHyp m = nthHypId m >>== fun id ->
+ Proofview.Goal.return (mkVar id)
let onNthHypId m tac =
nthHypId m >>- tac
@@ -536,8 +539,8 @@ module New = struct
tac2 id
let fullGoal =
- Tacmach.New.pf_ids_of_hyps >- fun hyps ->
- Goal.return (None :: List.map Option.make hyps)
+ Tacmach.New.pf_ids_of_hyps >>== fun hyps ->
+ Proofview.Goal.return (None :: List.map Option.make hyps)
let tryAllHyps tac =
Tacmach.New.pf_ids_of_hyps >>- fun hyps ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c67e4b8d2..ba1b2d9dc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -426,14 +426,18 @@ let find_name loc decl = function
(* this case must be compatible with [find_intro_names] below. *)
Goal.env >- fun env ->
Goal.defs >- fun sigma ->
- Tacmach.New.of_old (fresh_id idl (default_id env sigma decl))
- | IntroBasedOn (id,idl) -> Tacmach.New.of_old (fresh_id idl id)
+ Goal.V82.to_sensitive (fresh_id idl (default_id env sigma decl))
+ | IntroBasedOn (id,idl) -> Goal.V82.to_sensitive (fresh_id idl id)
| IntroMustBe id ->
(* When name is given, we allow to hide a global name *)
- Tacmach.New.pf_ids_of_hyps >- fun ids_of_hyps ->
+ Goal.hyps >- fun hyps ->
+ let hyps = Environ.named_context_of_val hyps in
+ let ids_of_hyps = ids_of_named_context hyps in
let id' = next_ident_away id ids_of_hyps in
if not (Id.equal id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used.");
Goal.return id'
+let find_name loc decl x =
+ Proofview.Goal.lift (find_name loc decl x)
(* Returns the names that would be created by intros, without doing
intros. This function is supposed to be compatible with an
@@ -456,7 +460,7 @@ let build_intro_tac id dest tac = match dest with
| dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
- Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>- fun concl ->
match kind_of_term concl with
| Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
find_name loc (name,None,t) name_flag >>- fun name ->
@@ -1278,7 +1282,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
if i > nconstr then error "Not enough constructors."
let constructor_tac with_evars expctdnumopt i lbind =
- Goal.concl >>- fun cl ->
+ Proofview.Goal.concl >>- fun cl ->
Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>- fun reduce_to_quantified_ind ->
let (mind,redcl) = reduce_to_quantified_ind cl in
let nconstr =
@@ -1298,7 +1302,7 @@ let one_constructor i lbind = constructor_tac false None i lbind
let any_constructor with_evars tacopt =
let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
- Goal.concl >>- fun cl ->
+ Proofview.Goal.concl >>- fun cl ->
Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>- fun reduce_to_quantified_ind ->
let mind = fst (reduce_to_quantified_ind cl) in
let nconstr =
@@ -1393,7 +1397,7 @@ let rewrite_hyp l2r id =
Hook.get forward_subst_one true x (id,rhs,l2r) in
let clear_var_and_eq c =
tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
Tacmach.New.pf_apply whd_betadeltaiota >>- fun whd_betadeltaiota ->
let t = whd_betadeltaiota (type_of (mkVar id)) in
@@ -1504,39 +1508,42 @@ let make_id s = fresh_id [] (default_id_of_sort s)
let prepare_intros s ipat =
let make_id s = Tacmach.New.of_old (make_id s) in
let fresh_id l id = Tacmach.New.of_old (fresh_id l id) in
+ let (>>=) t k =
+ t >>== fun x ->
+ Proofview.Goal.return (k x)
+ in
match ipat with
| None ->
- make_id s >- fun id ->
- Goal.return (id , Proofview.tclUNIT ())
+ make_id s >>= fun id ->
+ id , Proofview.tclUNIT ()
| Some (loc,ipat) -> match ipat with
| IntroIdentifier id ->
- Goal.return (id, Proofview.tclUNIT ())
+ Proofview.Goal.return (id, Proofview.tclUNIT ())
| IntroAnonymous ->
- make_id s >- fun id ->
- Goal.return (id , Proofview.tclUNIT ())
+ make_id s >>= fun id ->
+ id , Proofview.tclUNIT ()
| IntroFresh id ->
- fresh_id [] id >- fun id ->
- Goal.return (id , Proofview.tclUNIT ())
+ fresh_id [] id >>= fun id ->
+ id , Proofview.tclUNIT ()
| IntroWildcard ->
- make_id s >- fun id ->
- Goal.return (id , Proofview.V82.tactic (clear_wildcards [dloc,id]))
+ make_id s >>= fun id ->
+ id , Proofview.V82.tactic (clear_wildcards [dloc,id])
| IntroRewrite l2r ->
- make_id s >- fun id ->
- Goal.return (id, Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl)
+ make_id s >>= fun id ->
+ id, Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
| IntroOrAndPattern ll ->
- make_id s >- fun id ->
- Goal.return (id ,
+ make_id s >>= fun id ->
+ id ,
Tacticals.New.onLastHypId
(intro_or_and_pattern loc true ll [] []
(fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
- )
| IntroInjection l ->
- make_id s >- fun id ->
- Goal.return (id ,
+ make_id s >>= fun id ->
+ id ,
Proofview.V82.tactic (onLastHypId
(intro_decomp_eq loc true l [] []
(fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
- ))
+ )
| IntroForthcoming _ -> user_err_loc
(loc,"",str "Introduction pattern for one hypothesis expected")
@@ -1881,39 +1888,41 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
(depdecls,lastlhyp,ccl,out test)
let letin_tac_gen with_eq name (sigmac,c) test ty occs =
- Goal.env >>- fun env ->
- Goal.hyps >>- fun hyps ->
+ Proofview.Goal.env >>- fun env ->
+ Proofview.Goal.hyps >>- fun hyps ->
let hyps = Environ.named_context_of_val hyps in
let id =
let t = match ty with Some t -> t | None -> typ_of env sigmac c in
let x = id_of_name_using_hdchar (Global.env()) t name in
if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) else
- if not (mem_named_context x hyps) then Goal.return x else
- error ("The variable "^(Id.to_string x)^" is already declared.") in
+ Proofview.Goal.lift begin
+ if not (mem_named_context x hyps) then Goal.return x else
+ error ("The variable "^(Id.to_string x)^" is already declared.")
+ end in
id >>- fun id ->
Tacmach.New.of_old (letin_abstract id c test occs) >>- fun (depdecls,lastlhyp,ccl,c) ->
- let t = match ty with Some t -> Goal.return t | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) in
+ let t = match ty with Some t -> (Proofview.Goal.return t) | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) in
t >>- fun t ->
let newcl = match with_eq with
| Some (lr,(loc,ido)) ->
let heq = match ido with
| IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id))
| IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base)
- | IntroIdentifier id -> Goal.return id
- | _ -> error"Expect an introduction pattern naming one hypothesis." in
- heq >- fun heq ->
+ | IntroIdentifier id -> (Proofview.Goal.return id)
+ | _ -> Proofview.tclZERO (UserError ("" , Pp.str"Expect an introduction pattern naming one hypothesis.")) in
+ heq >>== fun heq ->
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
let eq = applist (eqdata.eq,args) in
let refl = applist (eqdata.refl, [t;mkVar id]) in
- Goal.return begin
+ Proofview.Goal.return begin
mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)),
Tacticals.New.tclTHEN
(intro_gen loc (IntroMustBe heq) lastlhyp true false)
(Proofview.V82.tactic (thin_body [heq;id]))
end
| None ->
- Goal.return (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
+ (Proofview.Goal.return (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in
newcl >>- fun (newcl,eq_tac) ->
Tacticals.New.tclTHENLIST
[ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
@@ -1924,12 +1933,12 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs =
let make_eq_test c = (make_eq_test c,fun _ -> c)
let letin_tac with_eq name c ty occs =
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
letin_tac_gen with_eq name (sigma,c) (make_eq_test c) ty (occs,true)
let letin_pat_tac with_eq name c ty occs =
- Goal.env >>- fun env ->
- Goal.defs >>- fun sigma ->
+ Proofview.tclEVARMAP >= fun sigma ->
+ Proofview.Goal.env >>- fun env ->
letin_tac_gen with_eq name c
(make_pattern_test env sigma c)
ty (occs,true)
@@ -2095,7 +2104,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
let recpat = match names with
| [loc,IntroIdentifier id as pat] ->
let id' = next_ident_away (add_prefix "IH" id) avoid in
- Goal.return (pat, [dloc, IntroIdentifier id'])
+ (Proofview.Goal.return (pat, [dloc, IntroIdentifier id']))
| _ -> Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname deprec gl names) in
recpat >>- fun (recpat,names) ->
let dest = get_recarg_dest dests in
@@ -2152,7 +2161,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
let indtyp = reduce_to_atomic_ref indref tmptyp0 in
let argl = snd (decompose_app indtyp) in
let c = List.nth argl (i-1) in
- Goal.env >>- fun env ->
+ Proofview.Goal.env >>- fun env ->
match kind_of_term c with
| Var id when not (List.exists (occur_var env id) avoid) ->
atomize_one (i-1) ((mkVar id)::avoid)
@@ -2633,16 +2642,16 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
Proofview.tclUNIT () >= fun () -> (* delay for [check_required_library] *)
Coqlib.check_required_library Coqlib.jmeq_module_name;
let args =
- Tacmach.New.pf_get_new_id id >>-- fun oldid ->
- Tacmach.New.pf_get_hyp id >>-- fun (_, b, t) ->
- Proofview.tclUNIT
- begin match b with
+ Tacmach.New.pf_get_new_id id >>== fun oldid ->
+ Tacmach.New.pf_get_hyp id >>== fun (_, b, t) ->
+ Proofview.Goal.return begin
+ match b with
| None -> let f, args = decompose_app t in
- Goal.return (f, args, false, id, oldid)
+ (f, args, false, id, oldid)
| Some t ->
let f, args = decompose_app t in
- Goal.return (f, args, true, id, oldid)
- end
+ (f, args, true, id, oldid)
+ end
in
args >>= fun (f, args, def, id, oldid) ->
if List.is_empty args then Proofview.tclUNIT ()
@@ -3102,8 +3111,8 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t
hypotheses from the context *)
let apply_induction_in_context hyp0 elim indvars names induct_tac =
- Goal.env >>- fun env ->
- Goal.concl >>- fun concl ->
+ Proofview.Goal.env >>- fun env ->
+ Proofview.Goal.concl >>- fun concl ->
let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
let deps = List.map (on_pi3 refresh_universes_strict) deps in
let tmpcl = it_mkNamedProd_or_LetIn concl deps in
@@ -3259,15 +3268,15 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
(induction_with_atomization_of_ind_arg
isrec with_evars elim names (id,lbind) inhyps)
| _ ->
- Goal.env >>- fun env ->
+ Proofview.tclEVARMAP >= fun defs ->
+ Proofview.Goal.env >>- fun env ->
let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c)
Anonymous in
Tacmach.New.of_old (fresh_id [] x) >>- fun id ->
(* We need the equality name now *)
let with_eq = Option.map (fun eq -> (false,eq)) eqname in
(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
- Goal.env >>- fun env ->
- Goal.defs >>- fun defs ->
+ Proofview.Goal.env >>- fun env ->
Tacticals.New.tclTHEN
(* Warning: letin is buggy when c is not of inductive type *)
(letin_tac_gen with_eq (Name id) (sigma,c)
@@ -3517,9 +3526,11 @@ let reflexivity_red allowred =
let concl = if not allowred then Goal.concl
else
Goal.concl >- fun c ->
- Tacmach.New.pf_apply (fun env sigma ->whd_betadeltaiota env sigma c)
+ Goal.env >- fun env ->
+ Goal.defs >- fun sigma ->
+ Goal.return (whd_betadeltaiota env sigma c)
in
- concl >>- fun concl ->
+ Proofview.Goal.lift concl >>- fun concl ->
match match_with_equality_type concl with
| None -> Proofview.tclZERO NoEquationFound
| Some _ -> one_constructor 1 NoBindings
@@ -3572,9 +3583,11 @@ let symmetry_red allowred =
Goal.concl
else
Goal.concl >- fun c ->
- Tacmach.New.pf_apply (fun env sigma -> whd_betadeltaiota env sigma c)
+ Goal.env >- fun env ->
+ Goal.defs >- fun sigma ->
+ Goal.return (whd_betadeltaiota env sigma c)
in
- concl >>- fun concl ->
+ Proofview.Goal.lift concl >>- fun concl ->
match_with_equation concl >= fun with_eqn ->
match with_eqn with
| Some eq_data,_,_ ->
@@ -3639,13 +3652,15 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
(* This is probably not very useful any longer *)
let prove_transitivity hdcncl eq_kind t =
- begin match eq_kind with
+ Proofview.Goal.lift begin match eq_kind with
| MonomorphicLeibnizEq (c1,c2) ->
Goal.return (mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]))
| PolymorphicLeibnizEq (typ,c1,c2) ->
Goal.return (mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]))
| HeterogenousEq (typ1,c1,typ2,c2) ->
- Tacmach.New.pf_apply Typing.type_of >- fun type_of ->
+ Goal.env >- fun env ->
+ Goal.defs >- fun sigma ->
+ let type_of = Typing.type_of env sigma in
let typt = type_of t in
Goal.return
(mkApp(hdcncl, [| typ1; c1; typt ;t |]),
@@ -3667,9 +3682,11 @@ let transitivity_red allowred t =
Goal.concl
else
Goal.concl >- fun c ->
- Tacmach.New.pf_apply (fun env sigma -> whd_betadeltaiota env sigma c)
+ Goal.env >- fun env ->
+ Goal.defs >- fun sigma ->
+ Goal.return (whd_betadeltaiota env sigma c)
in
- concl >>- fun concl ->
+ Proofview.Goal.lift concl >>- fun concl ->
match_with_equation concl >= fun with_eqn ->
match with_eqn with
| Some eq_data,_,_ ->
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 8e49a5cfa..b37dd0398 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -552,12 +552,13 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
in
let fresh_id s =
- Tacmach.New.of_old begin fun gsig ->
+ Goal.V82.to_sensitive begin fun gsig ->
let fresh = fresh_id (!avoid) s gsig in
avoid := fresh::(!avoid); fresh
end
in
- Goal.sensitive_list_map fresh_id first_intros >>- fun fresh_first_intros ->
+ Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>- fun fresh_first_intros ->
+ let fresh_id s = Proofview.Goal.lift (fresh_id s) in
fresh_id (Id.of_string "x") >>- fun freshn ->
fresh_id (Id.of_string "y") >>- fun freshm ->
fresh_id (Id.of_string "Z") >>- fun freshz ->
@@ -591,7 +592,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
- Goal.concl >>- fun gl ->
+ Proofview.Goal.concl >>- fun gl ->
match (kind_of_term gl) with
| App (c,ca) -> (
match (kind_of_term c) with
@@ -682,12 +683,13 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s =
- Tacmach.New.of_old begin fun gsig ->
+ Goal.V82.to_sensitive begin fun gsig ->
let fresh = fresh_id (!avoid) s gsig in
avoid := fresh::(!avoid); fresh
end
in
- Goal.sensitive_list_map fresh_id first_intros >>- fun fresh_first_intros ->
+ Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>- fun fresh_first_intros ->
+ let fresh_id s = Proofview.Goal.lift (fresh_id s) in
fresh_id (Id.of_string "x") >>- fun freshn ->
fresh_id (Id.of_string "y") >>- fun freshm ->
fresh_id (Id.of_string "Z") >>- fun freshz ->
@@ -709,7 +711,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
Tacticals.New.tclTHENLIST [Proofview.V82.tactic (apply (andb_true_intro()));
simplest_split ;Auto.default_auto ]
);
- Goal.concl >>- fun gl ->
+ Proofview.Goal.concl >>- fun gl ->
(* assume the goal to be eq (eq_type ...) = true *)
match (kind_of_term gl) with
| App(c,ca) -> (match (kind_of_term ca.(1)) with
@@ -819,12 +821,13 @@ let compute_dec_tact ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s =
- Tacmach.New.of_old begin fun gsig ->
+ Goal.V82.to_sensitive begin fun gsig ->
let fresh = fresh_id (!avoid) s gsig in
avoid := fresh::(!avoid); fresh
end
in
- Goal.sensitive_list_map fresh_id first_intros >>- fun fresh_first_intros ->
+ Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>- fun fresh_first_intros ->
+ let fresh_id s = Proofview.Goal.lift (fresh_id s) in
fresh_id (Id.of_string "x") >>- fun freshn ->
fresh_id (Id.of_string "y") >>- fun freshm ->
fresh_id (Id.of_string "H") >>- fun freshH ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 16:57:11 +0000