res
;;
+let source_id_of_id id = "#source#" ^ id;;
+
exception NotEnoughElements;;
exception NameExpected;;
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 =