- in
- (match cic with
- | Cic.Const (uri, []) ->
- let uris =
- match CicEnvironment.get_obj uri with
- | Cic.Constant (_, _, _, uris) -> uris
- | _ -> assert false
- in
- Cic.Const (uri, mk_subst uris)
- | Cic.Var (uri, []) ->
- let uris =
- match CicEnvironment.get_obj uri with
- | Cic.Variable (_, _, _, uris) -> uris
- | _ -> assert false
- in
- Cic.Var (uri, mk_subst uris)
- | Cic.MutInd (uri, i, []) ->
- let uris =
- match CicEnvironment.get_obj uri with
- | Cic.InductiveDefinition (_, uris, _) -> uris
- | _ -> assert false
- in
- Cic.MutInd (uri, i, mk_subst uris)
- | Cic.MutConstruct (uri, i, j, []) ->
- let uris =
- match CicEnvironment.get_obj uri with
- | Cic.InductiveDefinition (_, uris, _) -> uris
- | _ -> assert false
- in
- Cic.MutConstruct (uri, i, j, mk_subst uris)
- | Cic.Meta _ | Cic.Implicit _ as t ->
+ in
+ (* the try is for CicTypeChecker.typecheck *)
+ (try
+ match cic with
+ | Cic.Const (uri, []) ->
+ let uris =
+ match CicEnvironment.get_obj uri with
+ (*match CicTypeChecker.typecheck uri with*)
+ | Cic.Constant (_, _, _, uris) -> uris
+ | _ -> assert false
+ in
+ Cic.Const (uri, mk_subst uris)
+ | Cic.Var (uri, []) ->
+ let uris =
+ match CicEnvironment.get_obj uri with
+ (*match CicTypeChecker.typecheck uri with*)
+ | Cic.Variable (_, _, _, uris) -> uris
+ | _ -> assert false
+ in
+ Cic.Var (uri, mk_subst uris)
+ | Cic.MutInd (uri, i, []) ->
+ let uris =
+ match CicEnvironment.get_obj uri with
+ (*match CicTypeChecker.typecheck uri with*)
+ | Cic.InductiveDefinition (_, uris, _) -> uris
+ | _ -> assert false
+ in
+ Cic.MutInd (uri, i, mk_subst uris)
+ | Cic.MutConstruct (uri, i, j, []) ->
+ let uris =
+ match CicEnvironment.get_obj uri with
+ (*match CicTypeChecker.typecheck uri with*)
+ | Cic.InductiveDefinition (_, uris, _) -> uris
+ | _ -> assert false
+ in
+ Cic.MutConstruct (uri, i, j, mk_subst uris)
+ | Cic.Meta _ | Cic.Implicit _ as t ->