summaryrefslogtreecommitdiff
path: root/toplevel/indschemes.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
commit3e96002677226c0cdaa8f355938a76cfb37a722a (patch)
tree3ca96e142fdb68e464d2f5f403f315282b94f922 /toplevel/indschemes.ml
parentf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff)
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'toplevel/indschemes.ml')
-rw-r--r--toplevel/indschemes.ml34
1 files changed, 14 insertions, 20 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 29d7a12c..9031d8a3 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indschemes.ml 13333 2010-07-27 10:18:30Z vsiles $ *)
+(* $Id: indschemes.ml 13396 2010-09-02 16:52:15Z vsiles $ *)
(* Created by Hugo Herbelin from contents related to inductive schemes
initially developed by Christine Paulin (induction schemes), Vincent
@@ -123,8 +123,8 @@ let declare_beq_scheme_gen internal names kn =
let alarm what internal msg =
let debug = false in
- (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
match internal with
+ | KernelVerbose
| KernelSilent ->
(if debug then
Flags.if_verbose Pp.msg_warning
@@ -172,17 +172,15 @@ let beq_scheme_msg mind =
let declare_beq_scheme_with l kn =
try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
-(* TODO : maybe switch to KernelVerbose to have the right behaviour *)
let try_declare_beq_scheme kn =
(* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle
proof-irrelevance; improve decidability by depending on decidability
for the parameters rather than on the bl and lb properties *)
- try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelSilent [] kn
+ try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn
let declare_beq_scheme = declare_beq_scheme_with []
(* Case analysis schemes *)
-(* TODO: maybe switch to KernelVerbose *)
let declare_one_case_analysis_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
@@ -192,7 +190,7 @@ let declare_one_case_analysis_scheme ind =
induction scheme, the other ones share the same code with the
apropriate type *)
if List.mem InType kelim then
- ignore (define_individual_scheme dep KernelSilent None ind)
+ ignore (define_individual_scheme dep KernelVerbose None ind)
(* Induction/recursion schemes *)
@@ -206,7 +204,6 @@ let kinds_from_type =
InProp,ind_dep_scheme_kind_from_type;
InSet,rec_dep_scheme_kind_from_type]
- (* TODO: maybe switch to kernel verbose *)
let declare_one_induction_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
@@ -216,7 +213,7 @@ let declare_one_induction_scheme ind =
list_map_filter (fun (sort,kind) ->
if List.mem sort kelim then Some kind else None)
(if from_prop then kinds_from_prop else kinds_from_type) in
- List.iter (fun kind -> ignore (define_individual_scheme kind KernelSilent None ind))
+ List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind))
elims
let declare_induction_schemes kn =
@@ -241,10 +238,9 @@ let declare_eq_decidability_scheme_with l kn =
try_declare_scheme (eq_dec_scheme_msg (kn,0))
declare_eq_decidability_gen UserVerbose l kn
-(* TODO: maybe switch to kernel verbose *)
let try_declare_eq_decidability kn =
try_declare_scheme (eq_dec_scheme_msg (kn,0))
- declare_eq_decidability_gen KernelSilent [] kn
+ declare_eq_decidability_gen KernelVerbose [] kn
let declare_eq_decidability = declare_eq_decidability_scheme_with []
@@ -252,36 +248,34 @@ let ignore_error f x = try ignore (f x) with _ -> ()
let declare_rewriting_schemes ind =
if Hipattern.is_inductive_equality ind then begin
- ignore (define_individual_scheme rew_r2l_scheme_kind KernelSilent None ind);
- ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelSilent None ind);
+ ignore (define_individual_scheme rew_r2l_scheme_kind KernelVerbose None ind);
+ ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelVerbose None ind);
ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
- KernelSilent None ind);
+ KernelVerbose None ind);
(* These ones expect the equality to be symmetric; the first one also *)
(* needs eq *)
- ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelSilent None) ind;
+ ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelVerbose None) ind;
ignore_error
- (define_individual_scheme rew_l2r_dep_scheme_kind KernelSilent None) ind;
+ (define_individual_scheme rew_l2r_dep_scheme_kind KernelVerbose None) ind;
ignore_error
- (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelSilent None) ind
+ (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelVerbose None) ind
end
-(* TODO: maybe switch to kernel verbose *)
let declare_congr_scheme ind =
if Hipattern.is_equality_type (mkInd ind) then begin
if
try Coqlib.check_required_library Coqlib.logic_module_name; true
with _ -> false
then
- ignore (define_individual_scheme congr_scheme_kind KernelSilent None ind)
+ ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
else
warning "Cannot build congruence scheme because eq is not found"
end
-(* TODO: maybe switch to kernel verbose *)
let declare_sym_scheme ind =
if Hipattern.is_inductive_equality ind then
(* Expect the equality to be symmetric *)
- ignore_error (define_individual_scheme sym_scheme_kind KernelSilent None) ind
+ ignore_error (define_individual_scheme sym_scheme_kind KernelVerbose None) ind
(* Scheme command *)