* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf
exception RefineFailure of string Lazy.t;;
and avoid_double_coercion subst metasenv ugraph t ty =
match t with
- | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when
+ | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when
CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
let source_carr = CoercGraph.source_of c2 in
let tgt_carr = CicMetaSubst.apply_subst subst ty in
and eat_prods
allow_coercions subst metasenv context hetype tlbody_and_type ugraph
=
- let rec mk_prod metasenv context =
+ let rec mk_prod metasenv context' =
function
[] ->
let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context
+ CicMkImplicit.mk_implicit_type metasenv subst context'
in
let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
+ CicMkImplicit.identity_relocation_list_for_metavariable context'
in
metasenv,Cic.Meta (idx, irl)
| (_,argty)::tl ->
let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context
+ CicMkImplicit.mk_implicit_type metasenv subst context'
in
let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
+ CicMkImplicit.identity_relocation_list_for_metavariable context'
in
let meta = Cic.Meta (idx,irl) in
let name =
(* Nevertheless, argty is well-typed only in context. *)
(* Thus I generate a name (name_hint) in context and *)
(* then I generate a name --- using the hint name_hint *)
- (* --- that is fresh in (context'@context). *)
+ (* --- that is fresh in context'. *)
let name_hint =
(* Cic.Name "pippo" *)
FreshNamesGenerator.mk_fresh_name ~subst metasenv
in
(* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
FreshNamesGenerator.mk_fresh_name ~subst
- [] context name_hint ~typ:(Cic.Sort Cic.Prop)
+ [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
in
let metasenv,target =
- mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+ mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
in
metasenv,Cic.Prod (name,meta,target)
in
let metasenv,ugraph,cl' =
List.fold_right
(fun (name,ty) (metasenv,ugraph,res) ->
- let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
+ let ty =
+ CicTypeChecker.debrujin_constructor
+ ~cb:(relocalize localization_tbl) uri typesno ty in
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
let ty' = undebrujin uri typesno tys ty' in