X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralConversion.ml;h=30a52c32c66c5d760e1c050e4190bdbb9c910332;hb=790eccfa6b94dc82826d919691f8d4bfadb04573;hp=b3a247b02c448ca53aa7070a677d8f4574f97ef6;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index b3a247b02..30a52c32c 100644
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -210,9 +210,9 @@ let get_clears c p xtypes =
 	    else 
 	       hd, names, v
 	 in
-	 let p = C.LetIn (n, v, assert false, p) in
-	 let it = C.LetIn (n, v, assert false, it) in
-	 let et = C.LetIn (n, v, assert false, 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, assert false, p) in
-	 let it = C.LetIn (n, meta, assert false, it) in
-	 let et = C.LetIn (n, meta, assert false, 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