type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
-let pp_status status =
- pp (lazy (NCicPp.ppobj status#obj))
+let pp_tac_status status =
+ prerr_endline (NCicPp.ppobj status#obj);
+ prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack)
;;
type cic_term = NCic.context * NCic.term
status#set_obj (name,height,metasenv,subst,obj)
;;
-let instantiate status i t =
+let instantiate status ?refine:(dorefine=true) i t =
let _,_,metasenv,_,_ = status#obj in
let gname, context, gty = List.assoc i metasenv in
- let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
- to_subst status i (gname,context,t,ty)
+ if dorefine then
+ let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
+ to_subst status i (gname,context,t,ty)
+ else
+ let status,(_,ty) = typeof status context t in
+ to_subst status i (gname,context,snd t,ty)
;;
let instantiate_with_ast status i t =
| _,NCic.Const ref -> ref, []
| _,NCic.Appl (NCic.Const (NRef.Ref (_,(NRef.Ind _)) as ref) :: args) ->
ref, args
- | _,_ -> fail (lazy ("not an inductive type")) in
+ | _,_ -> fail (lazy ("not an inductive type: " ^ ppterm status ty)) in
let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in
let _,_,_,cl = List.nth tl i in
let consno = List.length cl in
status, (ctx, NCicUntrusted.apply_subst subst ctx t)
;;
+let apply_subst_context status ~fix_projections ctx =
+ let _,_,_,subst,_ = status#obj in
+ NCicUntrusted.apply_subst_context ~fix_projections subst ctx
+;;
+
let metas_of_term status (context,t) =
let _,_,_,subst,_ = status#obj in
NCicUntrusted.metas_of_term subst context t