diff options
Diffstat (limited to 'tactics/inv.ml')
-rw-r--r-- | tactics/inv.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index d76c9a697..755494c2d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -14,6 +14,7 @@ open Util open Names open Term open Termops +open Constr open EConstr open Vars open Namegen @@ -25,7 +26,7 @@ open Tacticals.New open Tactics open Elim open Equality -open Misctypes +open Tactypes open Proofview.Notations module NamedDecl = Context.Named.Declaration @@ -124,12 +125,10 @@ let make_inv_predicate env evd indf realargs id status concl = in let eq_term = eqdata.Coqlib.eq in let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in - let eq = EConstr.of_constr eq in let eqn = applist (eq,[eqnty;lhs;rhs]) in let eqns = (Anonymous, lift n eqn) :: eqns in let refl_term = eqdata.Coqlib.refl in let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in - let refl_term = EConstr.of_constr refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in let args = refl :: args in @@ -294,7 +293,7 @@ let error_too_many_names pats = str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ str ": " ++ pr_enum (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ + (fun c -> Printer.pr_econstr_env env sigma (snd (c env (Evd.from_env env))))) pats ++ str ".") let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with @@ -333,7 +332,7 @@ let rec tclMAP_i allow_conj n tacfun = function (tacfun (get_names allow_conj a)) (tclMAP_i allow_conj (n-1) tacfun l) -let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id +let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter id (* invariant: ProjectAndApply is responsible for erasing the clause which it is given as input @@ -376,7 +375,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = [if as_mode then clear [id] else tclIDTAC; (tclMAP_i (false,false) neqns (function (idopt,_) -> tclTRY (tclTHEN - (intro_move_avoid idopt avoid MoveLast) + (intro_move_avoid idopt avoid Logic.MoveLast) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id)))))) @@ -405,7 +404,7 @@ let nLastDecls i tac = let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.enter begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in - let first_eq = ref MoveLast in + let first_eq = ref Logic.MoveLast in let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with | Some thin -> @@ -417,20 +416,20 @@ let rewrite_equations as_mode othin neqns names ba = (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx))); tclMAP_i (true,false) neqns (fun (idopt,names) -> (tclTHEN - (intro_move_avoid idopt avoid MoveLast) + (intro_move_avoid idopt avoid Logic.MoveLast) (onLastHypId (fun id -> tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) names; tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) let idopt = if as_mode then Some (NamedDecl.get_id d) else None in - intro_move idopt (if thin then MoveLast else !first_eq)) + intro_move idopt (if thin then Logic.MoveLast else !first_eq)) nodepids; (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)] | None -> (* simple inversion *) if as_mode then tclMAP_i (false,true) neqns (fun (idopt,_) -> - intro_move idopt MoveLast) names + intro_move idopt Logic.MoveLast) names else (tclTHENLIST [tclDO neqns intro; @@ -470,7 +469,7 @@ let raw_inversion inv_kind id status names = make_inv_predicate env evdref indf realargs id status concl in let sigma = !evdref in let (cut_concl,case_tac) = - if status != NoDep && (dependent sigma c concl) then + if status != NoDep && (local_occur_var sigma id concl) then Reductionops.beta_applist sigma (elim_predicate, realargs@[c]), case_then_using else @@ -498,9 +497,10 @@ let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( (strbrk "Inversion would require case analysis on sort " ++ - pr_sort Evd.empty k ++ + pr_sort sigma k ++ strbrk " which is not allowed for inductive definition " ++ pr_inductive env (fst i) ++ str ".")) | e -> Proofview.tclZERO ~info e |