Cic.InductiveDefinition (il,_,leftsno,_) ->
let _,_,_,cl =
try
Cic.InductiveDefinition (il,_,leftsno,_) ->
let _,_,_,cl =
try
| CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
let cic_name = CicNotationUtil.cic_name_of_name name in
| CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
let cic_name = CicNotationUtil.cic_name_of_name name in
- let build_term funs (var,_,_,_) t =
+ let build_term funs (var,_,ty,_) t =
- Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+ Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
let uris = CicUtil.params_of_obj o in
Cic.Const (uri, mk_subst uris)
| Cic.Var (uri, []) ->
let uris = CicUtil.params_of_obj o in
Cic.Const (uri, mk_subst uris)
| Cic.Var (uri, []) ->
let uris = CicUtil.params_of_obj o in
Cic.Var (uri, mk_subst uris)
| Cic.MutInd (uri, i, []) ->
(try
let uris = CicUtil.params_of_obj o in
Cic.Var (uri, mk_subst uris)
| Cic.MutInd (uri, i, []) ->
(try
let uris = CicUtil.params_of_obj o in
Cic.MutInd (uri, i, mk_subst uris)
with
let uris = CicUtil.params_of_obj o in
Cic.MutInd (uri, i, mk_subst uris)
with
(*here the explicit_named_substituion is assumed to be of length 0 *)
Cic.MutInd (uri,i,[]))
| Cic.MutConstruct (uri, i, j, []) ->
(*here the explicit_named_substituion is assumed to be of length 0 *)
Cic.MutInd (uri,i,[]))
| Cic.MutConstruct (uri, i, j, []) ->
let uris = CicUtil.params_of_obj o in
Cic.MutConstruct (uri, i, j, mk_subst uris)
| Cic.Meta _ | Cic.Implicit _ as t ->
let uris = CicUtil.params_of_obj o in
Cic.MutConstruct (uri, i, j, mk_subst uris)
| Cic.Meta _ | Cic.Implicit _ as t ->
| CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
| CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)
CicNotationUtil.cic_name_of_name var :: context,
domain_of_term_option ~loc ~context ty @ res)
(add_defs context,[]) params))
CicNotationUtil.cic_name_of_name var :: context,
domain_of_term_option ~loc ~context ty @ res)
(add_defs context,[]) params))
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
let disambiguate_thing ~dbd ~context ~metasenv
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
let disambiguate_thing ~dbd ~context ~metasenv
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
(thing_txt,thing_txt_prefix_len,thing)
=
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
(thing_txt,thing_txt_prefix_len,thing)
=
failwith "Disambiguate: circular dependency"
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
failwith "Disambiguate: circular dependency"
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv