string Lazy.t * (NCicReduction.machine * bool) *
(NCicReduction.machine * bool) ;;
-let (===) x y = Pervasives.compare x y = 0 ;;
+let (===) x y = Stdlib.compare x y = 0 ;;
let mk_msg (status:#NCic.status) metasenv subst context t1 t2 =
(lazy (
in
metasenv,subst,t
+let indfy status exc metasenv subst context t =
+ let t = NCicReduction.whd status ~subst context t in
+ let metasenv,subst =
+ match t with
+ | NCic.Const (Ref.Ref (_, Ref.Ind _))
+ | NCic.Appl (NCic.Const (Ref.Ref (_, Ref.Ind _))::_) -> metasenv, subst
+(*
+ | NCic.Meta (n,_) ->
+ let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
+ let kind = NCicUntrusted.kind_of_meta attrs in
+ if kind = `IsSort then
+ metasenv,subst
+ else
+ (match ty with
+ | NCic.Implicit (`Typeof _) ->
+ metasenv_to_subst n (`IsSort,[],ty) metasenv subst
+ | ty ->
+ let metasenv,subst,ty = sortfy status exc metasenv subst context ty in
+ metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
+*)
+ | NCic.Implicit _ -> assert false
+ | _ -> raise exc
+ in
+ metasenv,subst,t
+
let tipify status exc metasenv subst context t ty =
let is_type attrs =
match NCicUntrusted.kind_of_meta attrs with
let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
let metasenv =
NCicUntrusted.replace_in_metasenv n
- (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
+ (fun (attrs,cc,_) -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
metasenv
in
metasenv,subst,false
let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
let subst =
NCicUntrusted.replace_in_subst n
- (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
+ (fun (attrs,cc,bo,_)->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
subst
in
optimize_meta metasenv subst (NCicSubstitution.subst_meta status lc bo))
i
| NCic.Meta (i,_) -> (metasenv, subst), i
| _ ->
- raise (UnificationFailure (lazy "Locked term vs non
- flexible term; probably not saturated enough yet!"))
+ raise (UnificationFailure (lazy "Locked term vs non flexible term; probably not saturated enough yet!"))
in
let t1 = NCicReduction.whd status ~subst context t1 in
let j, lj =