diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-30 16:44:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-30 16:44:25 +0000 |
| commit | deb036a1712e802a55a6160630387fb52ce3d998 (patch) | |
| tree | b0bdd58eb37fc1254d569ee94a4c8ac6d3948643 /pretyping | |
| parent | 8e6dfb334bd42d58cba5a81704139afdd632df4d (diff) | |
Généralisation de with_occurrence (ex occurrence) et de red_expr pour permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 12 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 12 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 2 |
3 files changed, 15 insertions, 11 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 480ee13b2..9a0e51e10 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -263,22 +263,24 @@ type 'a raw_red_flag = { let all_flags = {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} -type 'a occurrences = int list * 'a +type 'a or_var = ArgArg of 'a | ArgVar of identifier located + +type 'a with_occurrences = int or_var list * 'a type ('a,'b) red_expr_gen = | Red of bool | Hnf - | Simpl of 'a occurrences option + | Simpl of 'a with_occurrences option | Cbv of 'b raw_red_flag | Lazy of 'b raw_red_flag - | Unfold of 'b occurrences list + | Unfold of 'b with_occurrences list | Fold of 'a list - | Pattern of 'a occurrences list + | Pattern of 'a with_occurrences list | ExtraRedExpr of string | CbvVm type ('a,'b) may_eval = | ConstrTerm of 'a - | ConstrEval of ('a, 'b) red_expr_gen * 'a + | ConstrEval of ('a,'b) red_expr_gen * 'a | ConstrContext of (loc * identifier) * 'a | ConstrTypeOf of 'a diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index d64ba03a7..f6541ff31 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -132,22 +132,24 @@ type 'a raw_red_flag = { val all_flags : 'a raw_red_flag -type 'a occurrences = int list * 'a +type 'a or_var = ArgArg of 'a | ArgVar of identifier located + +type 'a with_occurrences = int or_var list * 'a type ('a,'b) red_expr_gen = | Red of bool | Hnf - | Simpl of 'a occurrences option + | Simpl of 'a with_occurrences option | Cbv of 'b raw_red_flag | Lazy of 'b raw_red_flag - | Unfold of 'b occurrences list + | Unfold of 'b with_occurrences list | Fold of 'a list - | Pattern of 'a occurrences list + | Pattern of 'a with_occurrences list | ExtraRedExpr of string | CbvVm type ('a,'b) may_eval = | ConstrTerm of 'a - | ConstrEval of ('a, 'b) red_expr_gen * 'a + | ConstrEval of ('a,'b) red_expr_gen * 'a | ConstrContext of (loc * identifier) * 'a | ConstrTypeOf of 'a diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 9ffa1dfb7..84cc87e7f 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -77,5 +77,5 @@ val reduce_to_quantified_ref : val reduce_to_atomic_ref : env -> evar_map -> Libnames.global_reference -> types -> types -val contextually : bool -> constr occurrences -> reduction_function +val contextually : bool -> int list * constr -> reduction_function -> reduction_function |