diff options
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 8b98408c5e..9b96fbf68a 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -676,9 +676,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") let side_effect_of_mode = function - | Declare.UserAutomaticRequest -> false - | Declare.InternalTacticRequest -> true - | Declare.UserIndividualRequest -> false + | UserAutomaticRequest -> false + | InternalTacticRequest -> true + | UserIndividualRequest -> false let make_bl_scheme mode mind = let mib = Global.lookup_mind mind in |