diff options
| author | letouzey | 2012-10-06 10:08:48 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-06 10:08:48 +0000 |
| commit | 30cf9c6711df3eb583dacad3cb98158adbbf1f5f (patch) | |
| tree | dbb893378505ee744b94b4d8ef051018dac9d813 /intf | |
| parent | 3ab6c3a21f569ec684737e45200aa1b32f009214 (diff) | |
remove useless hidden_flag in TacMutual(Co)Fix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15874 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 7da58ca091..18232dce03 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -28,7 +28,6 @@ type evars_flag = bool (* true = pose evars false = fail on evars *) type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) type split_flag = bool (* true = exists false = split *) -type hidden_flag = bool (* true = internal use false = user-level *) type letin_flag = bool (* true = use local def false = use Leibniz *) type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) @@ -106,10 +105,9 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacCase of evars_flag * 'trm with_bindings | TacCaseType of 'trm | TacFix of identifier option * int - | TacMutualFix of - hidden_flag * identifier * int * (identifier * int * 'trm) list + | TacMutualFix of identifier * int * (identifier * int * 'trm) list | TacCofix of identifier option - | TacMutualCofix of hidden_flag * identifier * (identifier * 'trm) list + | TacMutualCofix of identifier * (identifier * 'trm) list | TacCut of 'trm | TacAssert of ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option * |