diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 9b16fe3f..bc82e9ef 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -420,7 +420,7 @@ module New = struct (* Try the first tactic that does not fail in a list of tactics *) let rec tclFIRST = function - | [] -> tclZERO (Errors.UserError ("Tacticals.New.tclFIRST",str"No applicable tactic.")) + | [] -> tclZEROMSG (str"No applicable tactic.") | t::rest -> tclORELSE0 t (tclFIRST rest) let rec tclFIRST_PROGRESS_ON tac = function @@ -430,10 +430,7 @@ module New = struct let rec tclDO n t = if n < 0 then - tclZERO (Errors.UserError ( - "Refiner.tclDO", - str"Wrong argument : Do needs a positive integer.") - ) + tclZEROMSG (str"Wrong argument : Do needs a positive integer.") else if n = 0 then tclUNIT () else if n = 1 then t else tclTHEN t (tclDO (n-1) t) @@ -456,7 +453,7 @@ module New = struct let tclCOMPLETE t = t >>= fun res -> (tclINDEPENDENT - (tclZERO (Errors.UserError ("",str"Proof is not complete."))) + (tclZEROMSG (str"Proof is not complete.")) ) <*> tclUNIT res @@ -596,12 +593,14 @@ module New = struct (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - Proofview.Goal.nf_enter begin fun gl -> - let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in - (** FIXME: evar leak. *) + Proofview.Goal.nf_enter + begin fun gl -> let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Proofview.Goal.nf_enter begin fun gl -> + let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in (* applying elimination_scheme just a little modified *) - let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in + let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv @@ -618,7 +617,8 @@ module New = struct | Var id -> string_of_id id | _ -> "\b" in - error ("The elimination combinator " ^ name_elim ^ " is unknown.") + errorlabstrm "Tacticals.general_elim_then_using" + (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain indmv elimclause indclause in let branchsigns = compute_construtor_signatures isrec ind in @@ -649,11 +649,11 @@ module New = struct Proofview.tclTHEN (Clenvtac.clenv_refine false clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end + end) end let elimination_then tac c = Proofview.Goal.nf_enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | None -> true,gl_make_elim |