diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index a97ae8f65..732d06f8a 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -263,7 +263,7 @@ let pf_with_evars glsev k gls = tclTHEN (Refiner.tclEVARS evd) (k a) gls let pf_constr_of_global gr k = - pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k + pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k (** Tacticals of Ltac defined directly in term of Proofview *) module New = struct @@ -492,11 +492,13 @@ module New = struct Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) (* Select a subset of the goals *) - let tclSELECT = function - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id - | Vernacexpr.SelectAll -> fun tac -> tac + let tclSELECT = let open Goal_select in function + | SelectNth i -> Proofview.tclFOCUS i i + | SelectList l -> Proofview.tclFOCUSLIST l + | SelectId id -> Proofview.tclFOCUSID id + | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") + | SelectAlreadyFocused -> + anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") (* Check that holes in arguments have been resolved *) @@ -506,8 +508,8 @@ module New = struct let evi = Evd.find sigma evk in match Evd.evar_body evi with | Evd.Evar_empty -> Some (evk,evi) - | Evd.Evar_defined c -> match Constr.kind c with - | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk + | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with + | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk | _ -> (* We make the assumption that there is no way to refine an evar remaining after typing from the initial term given to @@ -709,7 +711,7 @@ module New = struct let gl_make_elim ind = begin fun gl -> let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in let (sigma, c) = pf_apply Evd.fresh_global gl gr in - (sigma, EConstr.of_constr c) + (sigma, c) end let gl_make_case_dep (ind, u) = begin fun gl -> @@ -769,7 +771,6 @@ module New = struct Proofview.tclEVARMAP >>= fun sigma -> Proofview.tclENV >>= fun env -> let (sigma, c) = Evd.fresh_global env sigma ref in - let c = EConstr.of_constr c in Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c end |