diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 8 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/contradiction.ml | 12 | ||||
| -rw-r--r-- | tactics/elim.ml | 2 | ||||
| -rw-r--r-- | tactics/eqdecide.ml4 | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 42 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 14 | ||||
| -rw-r--r-- | tactics/inv.ml | 12 | ||||
| -rw-r--r-- | tactics/leminv.ml | 4 | ||||
| -rw-r--r-- | tactics/refine.ml | 6 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 9 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 221 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 6 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 19 | ||||
| -rw-r--r-- | tactics/tactics.ml | 135 |
17 files changed, 256 insertions, 248 deletions
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,_,_ -> |