diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:52:54 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:52:54 +0000 |
| commit | c3ca134628ad4d9ef70a13b65c48ff17c737238f (patch) | |
| tree | 136b4efbc3aefe76dcd2fa772141c774343f46df /tactics | |
| parent | 6946bbbf2390024b3ded7654814104e709cce755 (diff) | |
Modulification of name
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/evar_tactics.mli | 2 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 6 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.mli | 12 |
4 files changed, 11 insertions, 11 deletions
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 7813f5326..b6ce3e30c 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -14,4 +14,4 @@ open Locus val instantiate : int -> Tacinterp.interp_sign * Glob_term.glob_constr -> (Id.t * hyp_location_flag, unit) location -> tactic -val let_evar : name -> Term.types -> tactic +val let_evar : Name.t -> Term.types -> tactic diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 47fd9aac2..b4491770e 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -54,11 +54,11 @@ val h_cofix : Id.t option -> tactic val h_cut : constr -> tactic val h_generalize : constr list -> tactic -val h_generalize_gen : (constr Locus.with_occurrences * name) list -> tactic +val h_generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic val h_generalize_dep : ?with_let:bool -> constr -> tactic -val h_let_tac : letin_flag -> name -> constr -> Locus.clause -> +val h_let_tac : letin_flag -> Name.t -> constr -> Locus.clause -> intro_pattern_expr located option -> tactic -val h_let_pat_tac : letin_flag -> name -> evar_map * constr -> +val h_let_pat_tac : letin_flag -> Name.t -> evar_map * constr -> Locus.clause -> intro_pattern_expr located option -> tactic diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 69a4db463..1367bb87a 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -86,7 +86,7 @@ val is_equality_type : testing_function val match_with_nottype : (constr * constr) matching_function val is_nottype : testing_function -val match_with_forall_term : (name * constr * constr) matching_function +val match_with_forall_term : (Name.t * constr * constr) matching_function val is_forall_term : testing_function val match_with_imp_term : (constr * constr) matching_function diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 041edd250..84040722e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -363,16 +363,16 @@ val cut_in_parallel : constr list -> tactic val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic val forward : tactic option -> intro_pattern_expr located option -> constr -> tactic -val letin_tac : (bool * intro_pattern_expr located) option -> name -> +val letin_tac : (bool * intro_pattern_expr located) option -> Name.t -> constr -> types option -> clause -> tactic -val letin_pat_tac : (bool * intro_pattern_expr located) option -> name -> +val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t -> evar_map * constr -> types option -> clause -> tactic -val assert_tac : name -> types -> tactic -val assert_by : name -> types -> tactic -> tactic -val pose_proof : name -> constr -> tactic +val assert_tac : Name.t -> types -> tactic +val assert_by : Name.t -> types -> tactic -> tactic +val pose_proof : Name.t -> constr -> tactic val generalize : constr list -> tactic -val generalize_gen : ((occurrences * constr) * name) list -> tactic +val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic val unify : ?state:Names.transparent_state -> constr -> constr -> tactic |