diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 63 |
1 files changed, 46 insertions, 17 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b571b347d..c430edf2e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -43,7 +43,7 @@ open Pretype_errors open Unification open Locus open Locusops -open Misctypes +open Tactypes open Proofview.Notations open Context.Named.Declaration @@ -1153,6 +1153,11 @@ let tactic_infer_flags with_evar = { Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + type 'a core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident @@ -1281,7 +1286,7 @@ let do_replace id = function let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) targetid id sigma0 clenv tac = - let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in + let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in let clenv = if with_classes then { clenv with evd = Typeclasses.resolve_typeclasses @@ -2258,7 +2263,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in - let branchsigns = compute_constructor_signatures false ind in + let branchsigns = compute_constructor_signatures ~rec_flag:false ind in let nv_with_let = Array.map List.length branchsigns in let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in let ll = get_and_check_or_and_pattern ?loc ll branchsigns in @@ -2645,6 +2650,15 @@ let insert_before decls lasthyp env = push_named d env) ~init:(reset_context env) env +let mk_eq_name env id {CAst.loc;v=ido} = + match ido with + | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env + | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env + | IntroIdentifier id -> + if List.mem id (ids_of_named_context (named_context env)) then + user_err ?loc (Id.print id ++ str" is already used."); + id + (* unsafe *) let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = @@ -2654,14 +2668,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = else LocalAssum (id,t) in match with_eq with - | Some (lr,{CAst.loc;v=ido}) -> - let heq = match ido with - | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env - | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env - | IntroIdentifier id -> - if List.mem id (ids_of_named_context (named_context env)) then - user_err ?loc (Id.print id ++ str" is already used."); - id in + | Some (lr,heq) -> let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in @@ -4196,7 +4203,7 @@ let induction_tac with_evars params indvars elim = let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - Clenvtac.clenv_refine with_evars resolved + Clenvtac.clenv_refine ~with_evars resolved end (* Apply induction "in place" taking into account dependent @@ -4396,7 +4403,8 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim match res with | None -> (* pattern not found *) - let with_eq = Option.map (fun eq -> (false,eq)) eqname in + let with_eq = Option.map (fun eq -> (false,mk_eq_name env id eq)) eqname in + let inhyps = if List.is_empty inhyps then inhyps else Option.fold_left (fun inhyps (_,heq) -> heq::inhyps) inhyps with_eq in (* we restart using bindings after having tried type-class resolution etc. on the term given by the user *) let flags = tactic_infer_flags (with_evars && (* do not give a success semantics to edestruct on an open term yet *) false) in @@ -4421,21 +4429,22 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim else Proofview.tclUNIT (); if isrec then Proofview.cycle (-1) else Proofview.tclUNIT () ]) - tac + (tac inhyps) in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac | Some (sigma', c) -> (* pattern found *) - let with_eq = Option.map (fun eq -> (false,eq)) eqname in (* TODO: if ind has predicate parameters, use JMeq instead of eq *) let env = reset_with_named_context sign env in + let with_eq = Option.map (fun eq -> (false,mk_eq_name env id eq)) eqname in + let inhyps = if List.is_empty inhyps then inhyps else Option.fold_left (fun inhyps (_,heq) -> heq::inhyps) inhyps with_eq in let tac = Tacticals.New.tclTHENLIST [ Refine.refine ~typecheck:false begin fun sigma -> mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None end; - tac + (tac inhyps) ] in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma') tac @@ -4485,7 +4494,7 @@ let induction_gen clear_flag isrec with_evars elim pose_induction_arg_then isrec with_evars info_arg elim id arg t inhyps cls (induction_with_atomization_of_ind_arg - isrec with_evars elim names id inhyps) + isrec with_evars elim names id) end (* Induction on a list of arguments. First make induction arguments @@ -5025,6 +5034,26 @@ let tclABSTRACT ?(opaque=true) name_op tac = else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in abstract_subproof ~opaque s gk tac +let constr_eq ~strict x y = + let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in + let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + match EConstr.eq_constr_universes env evd x y with + | Some csts -> + let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in + if strict then + if Evd.check_constraints evd csts then Proofview.tclUNIT () + else fail_universes + else + (match Evd.add_constraints evd csts with + | evd -> Proofview.Unsafe.tclEVARS evd + | exception Univ.UniverseInconsistency _ -> + fail_universes) + | None -> fail + end + let unify ?(state=full_transparent_state) x y = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in |