| C.Prod (name,s,t) ->
let sort1 = type_of_aux context s
and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
- sort_of_prod context (name,s) (sort1,sort2)
+ let res = sort_of_prod context (name,s) (sort1,sort2) in
+ res
| C.Lambda (n,s,t) ->
let sort1 = type_of_aux context s in
(match R.whd context sort1 with
(CicSubstitution.subst s
(type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
| C.Appl (he::tl) when List.length tl > 0 ->
- let hetype = type_of_aux context he
- and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
+ let hetype = type_of_aux context he in
+ let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (AssertFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
| ((uri,t) as subst)::tl ->
let typeofvar =
CicSubstitution.subst_vars substs (type_of_variable uri) in
+(* CSC: this test should not exist
(match CicEnvironment.get_cooked_obj ~trust:false uri with
Cic.Variable (_,Some bo,_,_) ->
raise
("Unknown variable definition:" ^
UriManager.string_of_uri uri))
) ;
+*)
let typeoft = type_of_aux context t in
if CicReduction.are_convertible context typeoft typeofvar then
check_exp_named_subst_aux (substs@[subst]) tl