X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=c004fd346b4e2a9ff30714fa3cf84af50a5acf00;hb=bc698deb9b8416c2b903b78a6053d59f6cc2a8ec;hp=18b4f064f71bfaccfadddb83acf4f62d57e3166b;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 18b4f064f..c004fd346 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -282,7 +282,7 @@ let rec proc_lambda st name v t =
    let intro = get_intro name in
    proc_proof (add st entry intro) t
 
-and proc_letin st what name v t =
+and proc_letin st what name v w t =
    let intro = get_intro name in
    let proceed, dtext = test_depth st in
    let script = if proceed then 
@@ -300,8 +300,7 @@ and proc_letin st what name v t =
 	    in
 	    st, C.Decl (H.cic ity), rqv
 	 | None          ->
-            (*CSC: here we need the type of v *)
-	    st, C.Def (H.cic v, assert false), [T.LetIn (intro, v, dtext)]
+	    st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)]
       in
       let entry = Some (name, hyp) in
       let qt = proc_proof (next (add st entry intro)) t in
@@ -322,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
@@ -385,12 +389,13 @@ and proc_proof st t =
       {st with context = context; clears = clears; clears_note = note; }
    in
    match t with
-      | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
-      | C.ALetIn (_, name, v, ty, t) as what -> assert false (*proc_letin (f st) what name v t*)
-      | C.ARel _ as what                 -> proc_rel (f st) what
-      | C.AMutConstruct _ as what        -> proc_mutconstruct (f st) what
-      | C.AAppl (_, hd :: tl) as what    -> proc_appl (f st) what hd tl
-      | what                             -> proc_other (f st) what
+      | C.ALambda (_, name, w, t)           -> proc_lambda st name w 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
 
 and proc_bkd_proofs st synth names classes ts =
 try 
@@ -419,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