diff options
Diffstat (limited to 'pretyping/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 57 |
1 files changed, 33 insertions, 24 deletions
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 55c305cc..f2a4c303 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -1,33 +1,30 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacred.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Environ open Evd open Reductionops open Closure -open Rawterm +open Glob_term open Termops open Pattern -(*i*) +open Libnames type reduction_tactic_error = InvalidAbstraction of env * constr * (env * Type_errors.type_error) exception ReductionTacticError of reduction_tactic_error -(*s Reduction functions associated to tactics. \label{tacred} *) +(** {6 Reduction functions associated to tactics. {% \label{%}tacred{% }%} } *) -(* Evaluable global reference *) +(** Evaluable global reference *) val is_evaluable : Environ.env -> evaluable_global_reference -> bool @@ -41,57 +38,69 @@ val global_of_evaluable_reference : exception Redelimination -(* Red (raise user error if nothing reducible) *) +(** Red (raise user error if nothing reducible) *) val red_product : reduction_function -(* Red (raise Redelimination if nothing reducible) *) +(** Red (raise Redelimination if nothing reducible) *) val try_red_product : reduction_function -(* Simpl *) +(** Tune the behaviour of simpl for the given constant name *) +type simpl_flag = [ `SimplDontExposeCase | `SimplNeverUnfold ] + +val set_simpl_behaviour : + bool -> global_reference -> (int list * int * simpl_flag list) -> unit +val get_simpl_behaviour : + global_reference -> (int list * int * simpl_flag list) option + +(** Simpl *) val simpl : reduction_function -(* Simpl only at the head *) +(** Simpl only at the head *) val whd_simpl : reduction_function -(* Hnf: like whd_simpl but force delta-reduction of constants that do +(** Hnf: like whd_simpl but force delta-reduction of constants that do not immediately hide a non reducible fix or cofix *) val hnf_constr : reduction_function -(* Unfold *) +(** Unfold *) val unfoldn : (occurrences * evaluable_global_reference) list -> reduction_function -(* Fold *) +(** Fold *) val fold_commands : constr list -> reduction_function -(* Pattern *) +(** Pattern *) val pattern_occs : (occurrences * constr) list -> reduction_function -(* Rem: Lazy strategies are defined in Reduction *) -(* Call by value strategy (uses Closures) *) +(** Rem: Lazy strategies are defined in Reduction *) + +(** Call by value strategy (uses Closures) *) val cbv_norm_flags : Closure.RedFlags.reds -> reduction_function val cbv_beta : local_reduction_function val cbv_betaiota : local_reduction_function val cbv_betadeltaiota : reduction_function - val compute : reduction_function (* = [cbv_betadeltaiota] *) + val compute : reduction_function (** = [cbv_betadeltaiota] *) -(* [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)] +(** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)] with [I] an inductive definition; returns [I] and [t'] or fails with a user error *) val reduce_to_atomic_ind : env -> evar_map -> types -> inductive * types -(* [reduce_to_quantified_ind env sigma t] puts [t] in the form +(** [reduce_to_quantified_ind env sigma t] puts [t] in the form [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition; returns [I] and [t'] or fails with a user error *) val reduce_to_quantified_ind : env -> evar_map -> types -> inductive * types -(* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form +(** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *) val reduce_to_quantified_ref : - env -> evar_map -> Libnames.global_reference -> types -> types + env -> evar_map -> global_reference -> types -> types val reduce_to_atomic_ref : - env -> evar_map -> Libnames.global_reference -> types -> types + env -> evar_map -> global_reference -> types -> types + +val find_hnf_rectype : + env -> evar_map -> types -> inductive * constr list val contextually : bool -> occurrences * constr_pattern -> (patvar_map -> reduction_function) -> reduction_function |