X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicDischarge.ml;h=65b5cea3393918525b68a721f7713b39955f32a0;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=4ad41eef774913594c15f865c304c74ce07e92a2;hpb=987627a48b2a3c2345d1af2c2a6b1ab78aa90b58;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
index 4ad41eef7..65b5cea33 100644
--- a/helm/software/components/cic_proof_checking/cicDischarge.ml
+++ b/helm/software/components/cic_proof_checking/cicDischarge.ml
@@ -211,12 +211,20 @@ let rec discharge_term st t = match t with
 	    C.Lambda (C.Anonymous, vty, S.lift 1 wb)
 	 else
 (* Fixing needed, some right parametes *)
-	 if frpsno = rpsno then
-            let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
+	 if frpsno = rpsno && named then
+	    let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
       	    if !debug then begin
 	       out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
 	    end;
-	    let vty, wb = S.lift rpsno vty, S.lift (succ rpsno) wb in 
+	    let vty, wb = S.lift rpsno vty, S.lift 1 wb in 
+	    let vty = match vty with
+	       | C.Appl (C.MutInd (fu, fm, _) as hd :: args) 
+	          when UM.eq fu u && fm = m && List.length args = psno ->
+	          let largs, _ = X.split_nth lpsno args in
+		  C.Appl (hd :: largs @ Ut.mk_rels rpsno 0)  
+	       | _                                                     ->
+	          assert false
+	    in
 	    close false wc (C.Lambda (C.Anonymous, vty, wb))
 (* This case should not happen *)
 	 else assert false 
@@ -294,14 +302,14 @@ let rec discharge_object dn du obj =
       if w' == w && vars = [] then obj else
       let w'' = sh w w' in
 (* We do not typecheck because variables are not closed *)
-      C.Variable (dn b, None, w'', [], attrs)
+      C.Variable (dn b, None, w'', vars, attrs)
    | C.Variable (b, Some v, w, vars, attrs)            ->
       let st = init_status dn du ls vars in
       let w', v' = discharge_term st w, discharge_term st v in
       if w' == w && v' == v && vars = [] then obj else
       let w'', v'' = sh w w', sh v v' in
 (* We do not typecheck because variables are not closed *)
-      C.Variable (dn b, Some v'', w'', [], attrs)
+      C.Variable (dn b, Some v'', w'', vars, attrs)
    | C.Constant (b, None, w, vars, attrs)              ->
       let st = init_status dn du ls vars in
       let w' = discharge_term st w in
@@ -338,14 +346,23 @@ and discharge_uri dn du uri =
    obj', obj' == obj
 
 and discharge_vars dn du vars =
-(* We should check that the dependences are ordered telesopically *)   
-   let map u =
-      match discharge_uri dn du u with
-         | C.Variable (b, None, w, _, _), _   -> Some (C.Name b, C.Decl w)
-         | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
-	 | _                                  -> None
-   in
-   List.rev_map map vars
+   let rec aux us c = function
+      | []      -> c
+      | u :: tl ->
+         let e = match discharge_uri dn du u with
+            | C.Variable (b, None, w, vars, _), _   -> 
+	       let map = relocate us (List.rev vars) in 
+	       let w = S.lift_map 1 map w in
+	       Some (C.Name b, C.Decl w)
+            | C.Variable (b, Some v, w, vars, _), _ -> 
+	       let map = relocate us (List.rev vars) in
+	       let v, w = S.lift_map 1 map v, S.lift_map 1 map w in
+	       Some (C.Name b, C.Def (v, w))
+	    | _                                     -> assert false
+         in
+       	 aux (u :: us) (e :: c) tl
+   in 
+   aux [] [] vars
 
 and init_status dn du ls vars =
    let c, rl = discharge_vars dn du vars, List.rev vars in