From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 11 Jun 2003 17:23:35 +0000 (+0000)
Subject: Multiple Prod branches did not have their inner-sorts computed properly.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=aa414acf306f5cbf0157b467ab6115599c845bce

Multiple Prod branches did not have their inner-sorts computed properly.
---

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 773050c56..c18e7d6a6 100644
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -169,30 +169,33 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
           | C.Prod (n,s,t) ->
               Hashtbl.add ids_to_inner_sorts fresh_id''
                (string_of_sort innertype) ;
-              C.AProd
-               (fresh_id'', n, aux' context idrefs s,
-                aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
+	            let sourcetype = T.type_of_aux' metasenv context s in
+	             Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
+	              (string_of_sort sourcetype) ;
+               C.AProd
+                (fresh_id'', n, aux' context idrefs s,
+                 aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
           | C.Lambda (n,s,t) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
-	     let sourcetype = T.type_of_aux' metasenv context s in
-	      Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
-	       (string_of_sort sourcetype) ;
-             if innersort = "Prop" then
-              begin
-               let father_is_lambda =
-                match father with
-                   None -> false
-                 | Some father' ->
-                    match Hashtbl.find ids_to_terms father' with
-                       C.Lambda _ -> true
-                     | _ -> false
-               in
-                if (not father_is_lambda) || expected_available then
-                 add_inner_type fresh_id''
-              end ;
-             C.ALambda
-              (fresh_id'',n, aux' context idrefs s,
-               aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
+	           let sourcetype = T.type_of_aux' metasenv context s in
+	            Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
+	             (string_of_sort sourcetype) ;
+              if innersort = "Prop" then
+               begin
+                let father_is_lambda =
+                 match father with
+                    None -> false
+                  | Some father' ->
+                     match Hashtbl.find ids_to_terms father' with
+                        C.Lambda _ -> true
+                      | _ -> false
+                in
+                 if (not father_is_lambda) || expected_available then
+                  add_inner_type fresh_id''
+               end ;
+              C.ALambda
+               (fresh_id'',n, aux' context idrefs s,
+                aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
           | C.LetIn (n,s,t) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then