diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 13:37:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 13:37:10 +0000 |
| commit | 8ed67d4a2dabe40186c8ad0550fb3fbd2d9b8787 (patch) | |
| tree | 08a302bdd28b98df9da11751b831229ffc21cc04 /tactics/tactics.mli | |
| parent | 77259e0b563a10d57b55ac38400ca1843fb938f3 (diff) | |
Les réduction dans les hypothèses s'appliquent maintenant au corps de la définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 07db3b459..6f315f358 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -102,39 +102,39 @@ val dyn_exact_check : tactic_arg list -> tactic type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr -val reduct_in_hyp : 'a tactic_reduction -> identifier -> tactic -val reduct_option : 'a tactic_reduction -> identifier option -> tactic +val reduct_in_hyp : 'a tactic_reduction -> hyp_location -> tactic +val reduct_option : 'a tactic_reduction -> hyp_location option -> tactic val reduct_in_concl : 'a tactic_reduction -> tactic val change_in_concl : constr -> tactic -val change_in_hyp : constr -> identifier -> tactic -val change_option : constr -> identifier option -> tactic +val change_in_hyp : constr -> hyp_location -> tactic +val change_option : constr -> hyp_location option -> tactic val red_in_concl : tactic -val red_in_hyp : identifier -> tactic -val red_option : identifier option -> tactic +val red_in_hyp : hyp_location -> tactic +val red_option : hyp_location option -> tactic val hnf_in_concl : tactic -val hnf_in_hyp : identifier -> tactic -val hnf_option : identifier option -> tactic +val hnf_in_hyp : hyp_location -> tactic +val hnf_option : hyp_location option -> tactic val simpl_in_concl : tactic -val simpl_in_hyp : identifier -> tactic -val simpl_option : identifier option -> tactic +val simpl_in_hyp : hyp_location -> tactic +val simpl_option : hyp_location option -> tactic val normalise_in_concl: tactic -val normalise_in_hyp : identifier -> tactic -val normalise_option : identifier option -> tactic +val normalise_in_hyp : hyp_location -> tactic +val normalise_option : hyp_location option -> tactic val unfold_in_concl : (int list * Closure.evaluable_global_reference) list -> tactic val unfold_in_hyp : - (int list * Closure.evaluable_global_reference) list -> identifier -> tactic + (int list * Closure.evaluable_global_reference) list -> hyp_location -> tactic val unfold_option : - (int list * Closure.evaluable_global_reference) list -> identifier option + (int list * Closure.evaluable_global_reference) list -> hyp_location option -> tactic -val reduce : red_expr -> identifier list -> tactic +val reduce : red_expr -> hyp_location list -> tactic val dyn_reduce : tactic_arg list -> tactic val dyn_change : tactic_arg list -> tactic val unfold_constr : global_reference -> tactic val pattern_option : - (int list * constr * constr) list -> identifier option -> tactic + (int list * constr * constr) list -> hyp_location option -> tactic (*s Modification of the local context. *) |