X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralConversion.ml;h=30a52c32c66c5d760e1c050e4190bdbb9c910332;hb=a3ff8f4f61a45e8c269322275956fad0805da8bc;hp=376313ac8f9de4577fbeae6780e57b33b6b77801;hpb=797f61edb93f41eb2c5e281bc9457f6bff633063;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 376313ac8..30a52c32c 100644
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -72,7 +72,7 @@ let lift k n =
       | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
       | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
       | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
-      | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t)
+      | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term k ty, lift_term (succ k) t)
       | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
       | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
    in
@@ -87,9 +87,9 @@ let lift k n =
             | Invalid_argument _ -> assert false
       in
       let mk_decl n v = Some (n, C.Decl v) in
-      let mk_def n v = Some (n, C.Def (v, None)) in
-      let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in
-      let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in
+      let mk_def n v ty = Some (n, C.Def (v, ty)) in
+      let mk_fix (name, _, ty, bo) = mk_def (C.Name name) bo ty in
+      let mk_cofix (name, ty, bo) = mk_def (C.Name name) bo ty in
       let rec ann_xns c (uri, t) = uri, ann_term c t
       and ann_ms c = function
          | None -> None
@@ -112,7 +112,7 @@ let lift k n =
          | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)
          | C.Prod (n, s, t) -> C.AProd (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
          | C.Lambda (n, s, t) -> C.ALambda (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
-         | C.LetIn (n, s, t) -> C.ALetIn (id, n, ann_term c s, ann_term (mk_def n s :: c) t)
+         | C.LetIn (n, s, ty, t) -> C.ALetIn (id, n, ann_term c s, ann_term c ty, ann_term (mk_def n s ty :: c) t)
          | C.Fix (i, fl) -> C.AFix (id, i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
          | C.CoFix (i, fl) -> C.ACoFix (id, i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
       in
@@ -175,9 +175,9 @@ let generalize n =
       | C.ALambda (id, _, s, t) ->
          let s, t = gen_term k s, gen_term (succ k) t in
          if is_meta [s; t] then meta id else C.ALambda (id, anon, s, t)
-      | C.ALetIn (id, _, s, t) -> 
-         let s, t = gen_term k s, gen_term (succ k) t in
-         if is_meta [s; t] then meta id else C.ALetIn (id, anon, s, t)
+      | C.ALetIn (id, _, s, ty, t) -> 
+         let s, ty, t = gen_term k s, gen_term k ty, gen_term (succ k) t in
+         if is_meta [s; t] then meta id else C.ALetIn (id, anon, s, ty, t)
       | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (gen_fix (List.length fl) k) fl)
       | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (gen_cofix (List.length fl) k) fl)
    in
@@ -210,9 +210,9 @@ let get_clears c p xtypes =
 	    else 
 	       hd, names, v
 	 in
-	 let p = C.LetIn (n, v, p) in
-	 let it = C.LetIn (n, v, it) in
-	 let et = C.LetIn (n, v, et) in
+	 let p = C.LetIn (n, v, x, p) in
+	 let it = C.LetIn (n, v, x, it) in
+	 let et = C.LetIn (n, v, x, et) in
 	 aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Decl v) as hd :: tl     ->
 	 let p = C.Lambda (n, meta, p) in
@@ -220,9 +220,9 @@ let get_clears c p xtypes =
 	 let et = C.Lambda (n, meta, et) in
 	 aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
-	 let p = C.LetIn (n, meta, p) in
-	 let it = C.LetIn (n, meta, it) in
-	 let et = C.LetIn (n, meta, et) in
+	 let p = C.LetIn (n, meta, meta, p) in
+	 let it = C.LetIn (n, meta, meta, it) in
+	 let et = C.LetIn (n, meta, meta, et) in
 	 aux (hd :: c) names p it et tl
       | None :: tl                                        -> assert false
    in
@@ -240,7 +240,7 @@ let clear c hyp =
    aux [] c
 
 let elim_inferred_type context goal arg using cpattern =
-   let metasenv, ugraph = [], Un.empty_ugraph in 
+   let metasenv, ugraph = [], Un.oblivion_ugraph in 
    let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
    let _splits, args_no = PEH.split_with_whd (context, ety) in
    let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim