diff options
| author | barras | 2004-02-18 18:32:33 +0000 |
|---|---|---|
| committer | barras | 2004-02-18 18:32:33 +0000 |
| commit | b5df1925bbc14f441247349b200aa3f5828e8427 (patch) | |
| tree | c158ac5d3d3133f2fce8188f3d0b4a75bd0c5415 /pretyping | |
| parent | 06900e469cd593c272f57c2af7d2e4f206a2f944 (diff) | |
- fixed the Assert_failure error in kernel/modops
- fixed the problem with passing atomic tactics to ltacs
- restructured the distrib Makefile (can build a package from
the CVS working dir)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 3 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 2 |
2 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 78425e107a..6442ca9693 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -324,6 +324,9 @@ type 'a raw_red_flag = { rConst : 'a list } +let all_flags = + {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} + type 'a occurrences = int list * 'a type ('a,'b) red_expr_gen = diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 651530c94c..869861ccd7 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -117,6 +117,8 @@ type 'a raw_red_flag = { rConst : 'a list } +val all_flags : 'a raw_red_flag + type 'a occurrences = int list * 'a type ('a,'b) red_expr_gen = |