let metasenv,s = aux metasenv n s in
let metasenv,t = aux metasenv (n+1) t in
metasenv,Cic.Prod(name,s,t)
- | Cic.LetIn(name,s,t) ->
+ | Cic.LetIn(name,s,ty,t) ->
let metasenv,s = aux metasenv n s in
+ let metasenv,ty = aux metasenv n ty in
let metasenv,t = aux metasenv (n+1) t in
- metasenv,Cic.LetIn(name,s,t)
+ metasenv,Cic.LetIn(name,s,ty,t)
| Cic.Const(uri,ens) ->
let metasenv,ens =
List.fold_right
prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
raise exn
in
+ let old_insert_coercions = !CicRefine.insert_coercions in
let goal_proof,goal_ty,real_menv,_ =
(* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
try
debug_print (lazy (CicPp.ppterm goal_proof));
- CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
+ CicRefine.insert_coercions := false;
+ let res =
+ CicRefine.type_of_aux'
+ real_menv context goal_proof CicUniv.empty_ugraph
+ in
+ CicRefine.insert_coercions := old_insert_coercions;
+ res
with
| CicRefine.RefineFailure s
| CicRefine.Uncertain s
| CicRefine.AssertFailure s as exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
pp_error goal_proof names (Lazy.force s) exn
| CicUtil.Meta_not_found i as exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
| Invalid_argument "list_fold_left2" as exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
pp_error goal_proof names "Invalid_argument: list_fold_left2" exn
+ | exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
+ raise exn
in
let subst_side_effects,real_menv,_ =
try