diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 14 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
3 files changed, 14 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index f1326a51a9..b4def7bb51 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1134,6 +1134,7 @@ let make_tuple env sigma (rterm,rty) lind = assert (not (noccurn sigma lind rty)); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in + let a = simpl env sigma a in let na = Context.Rel.Declaration.get_annot (lookup_rel lind env) in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cb2e607012..70cea89ccb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1044,12 +1044,15 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = end end -let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) +let drop_intro_name (_ : Id.t) = Proofview.tclUNIT () + +let intro_gen n m f d = intro_then_gen n m f d drop_intro_name let intro_mustbe_force id = intro_gen (NamingMustBe (CAst.make id)) MoveLast true false -let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false +let intro_using_then id = intro_then_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false +let intro_using id = intro_using_then id drop_intro_name let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false -let intro = intro_gen (NamingAvoid Id.Set.empty) MoveLast false false +let intro = intro_then drop_intro_name let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false @@ -1065,6 +1068,11 @@ let rec intros_using = function | [] -> Proofview.tclUNIT() | str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l) +let rec intros_using_then_helper tac acc = function + | [] -> tac (List.rev acc) + | str::l -> intro_using_then str (fun str' -> intros_using_then_helper tac (str'::acc) l) +let intros_using_then l tac = intros_using_then_helper tac [] l + let intros = Tacticals.New.tclREPEAT intro let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5b397b15d0..00739306a7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -65,9 +65,11 @@ val intro_avoiding : Id.Set.t -> unit Proofview.tactic val intro_replacing : Id.t -> unit Proofview.tactic val intro_using : Id.t -> unit Proofview.tactic +val intro_using_then : Id.t -> (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intro_mustbe_force : Id.t -> unit Proofview.tactic val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intros_using : Id.t list -> unit Proofview.tactic +val intros_using_then : Id.t list -> (Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic val intros_replacing : Id.t list -> unit Proofview.tactic val intros_possibly_replacing : Id.t list -> unit Proofview.tactic |