blob: b5e4a7acbfdb3da2630bda5631990d84e3fc3441 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Genredexpr
let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
let make_red_flag l =
let rec add_flag red = function
| [] -> red
| FBeta :: lf -> add_flag { red with rBeta = true } lf
| FMatch :: lf -> add_flag { red with rMatch = true } lf
| FFix :: lf -> add_flag { red with rFix = true } lf
| FCofix :: lf -> add_flag { red with rCofix = true } lf
| FZeta :: lf -> add_flag { red with rZeta = true } lf
| FConst l :: lf ->
if red.rDelta then
CErrors.user_err Pp.(str
"Cannot set both constants to unfold and constants not to unfold");
add_flag { red with rConst = union_consts red.rConst l } lf
| FDeltaBut l :: lf ->
if red.rConst <> [] && not red.rDelta then
CErrors.user_err Pp.(str
"Cannot set both constants to unfold and constants not to unfold");
add_flag
{ red with rConst = union_consts red.rConst l; rDelta = true }
lf
in
add_flag
{rBeta = false; rMatch = false; rFix = false; rCofix = false;
rZeta = false; rDelta = false; rConst = []}
l
let all_flags =
{rBeta = true; rMatch = true; rFix = true; rCofix = true;
rZeta = true; rDelta = true; rConst = []}
|
