From b5df1925bbc14f441247349b200aa3f5828e8427 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 18 Feb 2004 18:32:33 +0000
Subject: - 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
---
 pretyping/rawterm.ml  | 3 +++
 pretyping/rawterm.mli | 2 ++
 2 files changed, 5 insertions(+)

(limited to 'pretyping')

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 =
-- 
cgit v1.2.3