- let coercion_src = carr type_to_coerce subst ctx in
- match coercion_src with
- | Cic.Sort _ ->
- t,type_to_coerce,subst,metasenv,ugraph
-(*
- | Cic.Meta _ as meta when not in_source ->
- let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
- let subst, metasenv, ugraph =
- fo_unif_subst
- subst ctx metasenv meta coercion_tgt ugraph
- in
- t, Cic.Sort tgt_sort, subst, metasenv, ugraph
-*)
- | Cic.Meta _ as meta ->
- t, meta, subst, metasenv, ugraph
- | Cic.Cast _ as cast ->
- t, cast, subst, metasenv, ugraph
- | term ->
- let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
- let search = CoercGraph.look_for_coercion in
- let boh = search coercion_src coercion_tgt in
- (match boh with
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- raise
- (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
- | CoercGraph.NotMetaClosed ->
- raise
- (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
- | CoercGraph.SomeCoercion c ->
- Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
+ if not !insert_coercions then
+ t,type_to_coerce,subst,metasenv,ugraph
+ else
+ let coercion_src = carr type_to_coerce subst context in
+ match coercion_src with
+ | Cic.Sort _ ->
+ t,type_to_coerce,subst,metasenv,ugraph
+ | Cic.Meta _ as meta ->
+ t, meta, subst, metasenv, ugraph
+ | Cic.Cast _ as cast ->
+ t, cast, subst, metasenv, ugraph
+ | term ->
+ let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
+ let search = CoercGraph.look_for_coercion in
+ let boh = search coercion_src coercion_tgt in
+ (match boh with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst t context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.NotMetaClosed ->
+ enrich localization_tbl t
+ (Uncertain
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst t context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.SomeCoercion c ->
+ let newt, tty, subst, metasenv, ugraph =
+ avoid_double_coercion
+ subst metasenv ugraph
+ (Cic.Appl[c;t]) coercion_tgt
+ in
+ newt, tty, subst, metasenv, ugraph)