Reports improved.

[helm.git] / helm / software / components / acic_procedural / acic2Procedural.ml

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 483378ce6c47f6f6df337687d71e133624bf9bd3..c004fd346b4e2a9ff30714fa3cf84af50a5acf00 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -321,6 +321,11 @@ and proc_mutconstruct st what =
    let script = [T.Apply (what, dtext)] in 
    mk_intros st what script
 
+and proc_const st what = 
+   let _, dtext = test_depth st in
+   let script = [T.Apply (what, dtext)] in 
+   mk_intros st what script
+
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
    let script = if proceed then
@@ -388,6 +393,7 @@ and proc_proof st t =
       | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
       | C.ARel _ as what                    -> proc_rel (f st) what
       | C.AMutConstruct _ as what           -> proc_mutconstruct (f st) what
+      | C.AConst _ as what                  -> proc_const (f st) what
       | C.AAppl (_, hd :: tl) as what       -> proc_appl (f st) what hd tl
       | what                                -> proc_other (f st) what
 
@@ -418,7 +424,8 @@ with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
 (* object costruction *******************************************************)
 
-let is_theorem pars =   
+let is_theorem pars =
+   pars = [] ||
    List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || 
    List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars