diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 8 | ||||
| -rw-r--r-- | tactics/leminv.ml | 4 | ||||
| -rw-r--r-- | tactics/leminv.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 23 |
4 files changed, 21 insertions, 16 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index a572508d47..3ccbab874f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -56,7 +56,9 @@ let head_constr_bound sigma t = | _ -> raise Bound let head_constr sigma c = - try head_constr_bound sigma c with Bound -> user_err Pp.(str "Bound head variable.") + try head_constr_bound sigma c + with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \ + (co)inductive type, (co)inductive type constructor, or projection.") let decompose_app_bound sigma t = let t = strip_outer_cast sigma t in @@ -764,7 +766,9 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with let try_head_pattern c = try head_pattern_bound c - with BoundPattern -> user_err Pp.(str "Bound head variable.") + with BoundPattern -> + user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \ + an if, case, or let expression, an application, or a projection.") let with_uid c = { obj = c; uid = fresh_key () } diff --git a/tactics/leminv.ml b/tactics/leminv.ml index aeb80ae57c..967ec2a71b 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -248,9 +248,9 @@ let add_inversion_lemma_exn na com comsort bool tac = let env = Global.env () in let evd = ref (Evd.from_env env) in let c = Constrintern.interp_type_evars env evd com in - let sigma, sort = Pretyping.interp_sort !evd comsort in + let evd, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env !evd comsort in try - add_inversion_lemma na env sigma c sort bool tac + add_inversion_lemma na env evd c sort bool tac with | UserError (Some "Case analysis",s) -> (* Reference to Indrec *) user_err ~hdr:"Inv needs Nodep Prop Set" s diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 41b0e09b42..8745ad3979 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -15,5 +15,5 @@ val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic val add_inversion_lemma_exn : - Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> unit Proofview.tactic) -> + Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) -> unit diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 67bc55d3fe..5698312aef 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2249,14 +2249,15 @@ let one_constructor i lbind = constructor_tac false None i lbind Should be generalize in Constructor (Fun c : I -> tactic) *) -let rec tclANY tac = function -| [] -> Tacticals.New.tclZEROMSG (str "No applicable tactic.") -| arg :: l -> - Tacticals.New.tclORD (tac arg) (fun () -> tclANY tac l) - let any_constructor with_evars tacopt = - let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in - let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in + let one_constr = + let tac i = constructor_tac with_evars None i NoBindings in + match tacopt with + | None -> tac + | Some t -> fun i -> Tacticals.New.tclTHEN (tac i) t in + let rec any_constr n i () = + if Int.equal i n then one_constr i + else Tacticals.New.tclORD (one_constr i) (any_constr n (i + 1)) in Proofview.Goal.enter begin fun gl -> let cl = Tacmach.New.pf_concl gl in let reduce_to_quantified_ind = @@ -2266,7 +2267,7 @@ let any_constructor with_evars tacopt = let nconstr = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in if Int.equal nconstr 0 then error "The type has no constructors."; - tclANY tac (List.interval 1 nconstr) + any_constr nconstr 1 () end let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 @@ -4131,7 +4132,7 @@ let guess_elim isrec dep s hyp0 gl = let env = Tacmach.New.pf_env gl in let sigma = Tacmach.New.project gl in let u = EInstance.kind (Tacmach.New.project gl) u in - if use_dependent_propositions_elimination () && dep + if use_dependent_propositions_elimination () && dep = Some true then let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in let ind = EConstr.of_constr ind in @@ -4165,7 +4166,7 @@ let find_induction_type isrec elim hyp0 gl = | None -> let sort = Tacticals.New.elimination_sort_of_goal gl in let _, (elimc,elimt),_ = - guess_elim isrec (* dummy: *) true sort hyp0 gl in + guess_elim isrec None sort hyp0 gl in let scheme = compute_elim_sig sigma ~elimc elimt in (* We drop the scheme waiting to know if it is dependent *) scheme, ElimOver (isrec,hyp0) @@ -4199,7 +4200,7 @@ let get_eliminator elim dep s gl = | ElimUsing (elim,indsign) -> Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> - let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in + let evd, (elimc,elimt),_ as elims = guess_elim isrec (Some dep) s id gl in let _, (l, s) = compute_elim_signature elims id in let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d))) (List.rev s.branches) |