diff options
Diffstat (limited to 'pretyping/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 45 |
1 files changed, 24 insertions, 21 deletions
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index aec9da95..03c4cb41 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,14 +11,13 @@ open Term open Environ open Evd open Reductionops -open Closure -open Glob_term -open Termops open Pattern -open Libnames +open Globnames +open Locus +open Univ type reduction_tactic_error = - InvalidAbstraction of env * constr * (env * Type_errors.type_error) + InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) exception ReductionTacticError of reduction_tactic_error @@ -28,13 +27,13 @@ exception ReductionTacticError of reduction_tactic_error val is_evaluable : Environ.env -> evaluable_global_reference -> bool -val error_not_evaluable : Libnames.global_reference -> 'a +val error_not_evaluable : Globnames.global_reference -> 'a val evaluable_of_global_reference : - Environ.env -> Libnames.global_reference -> evaluable_global_reference + Environ.env -> Globnames.global_reference -> evaluable_global_reference val global_of_evaluable_reference : - evaluable_global_reference -> Libnames.global_reference + evaluable_global_reference -> Globnames.global_reference exception Redelimination @@ -44,14 +43,6 @@ val red_product : reduction_function (** Red (raise Redelimination if nothing reducible) *) val try_red_product : reduction_function -(** 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 @@ -70,7 +61,8 @@ val unfoldn : val fold_commands : constr list -> reduction_function (** Pattern *) -val pattern_occs : (occurrences * constr) list -> reduction_function +val pattern_occs : (occurrences * constr) list -> env -> evar_map -> constr -> + evar_map * constr (** Rem: Lazy strategies are defined in Reduction *) @@ -84,12 +76,12 @@ val cbv_norm_flags : Closure.RedFlags.reds -> reduction_function (** [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 +val reduce_to_atomic_ind : env -> evar_map -> types -> pinductive * types (** [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 +val reduce_to_quantified_ind : env -> evar_map -> types -> pinductive * types (** [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 *) @@ -100,7 +92,18 @@ val reduce_to_atomic_ref : env -> evar_map -> global_reference -> types -> types val find_hnf_rectype : - env -> evar_map -> types -> inductive * constr list + env -> evar_map -> types -> pinductive * constr list val contextually : bool -> occurrences * constr_pattern -> (patvar_map -> reduction_function) -> reduction_function + +val e_contextually : bool -> occurrences * constr_pattern -> + (patvar_map -> e_reduction_function) -> e_reduction_function + +(** Returns the same inductive if it is allowed for pattern-matching + raises an error otherwise. **) +val check_privacy : env -> inductive puniverses -> inductive puniverses + +(** Returns the same inductive if it is not a primitive record + raises an error otherwise. **) +val check_not_primitive_record : env -> inductive puniverses -> inductive puniverses |