diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:37 +0000 |
| commit | 32170384190168856efeac5bcf90edf1170b54d6 (patch) | |
| tree | 0ea86b672df93d997fa1cab70b678ea7abdcf171 /pretyping/tacred.mli | |
| parent | 1e5182e9d5c29ae9adeed20dae32969785758809 (diff) | |
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 4100a31ae..c03c67c09 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -40,7 +40,7 @@ val unfoldn : val fold_commands : constr list -> reduction_function (* Pattern *) -val pattern_occs : (int list * constr * constr) list -> reduction_function +val pattern_occs : (int list * constr) list -> reduction_function (* Rem: Lazy strategies are defined in Reduction *) (* Call by value strategy (uses Closures) *) @@ -60,6 +60,8 @@ val reduce_to_atomic_ind : env -> evar_map -> types -> inductive * types returns [I] and [t'] or fails with a user error *) val reduce_to_quantified_ind : env -> evar_map -> types -> inductive * types +open Rawterm +(* type red_expr = | Red of bool (* raise Redelimination if true otherwise UserError *) | Hnf @@ -69,8 +71,14 @@ type red_expr = | Unfold of (int list * evaluable_global_reference) list | Fold of constr list | Pattern of (int list * constr * constr) list +*) +type red_expr = (constr, evaluable_global_reference) red_expr_gen -val reduction_of_redexp : red_expr -> reduction_function +val reduction_of_redexp : red_expr -> reduction_function + +type generic_reduction_function = constr list -> reduction_function + +val declare_red_expr : string -> generic_reduction_function -> unit (* Opaque and Transparent commands. *) val set_opaque_const : section_path -> unit |