diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 4 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 6 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 4 | ||||
| -rw-r--r-- | plugins/quote/quote.ml | 18 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 8 |
5 files changed, 21 insertions, 19 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 |