+ let paste_as_pattern_sequent term unsh_sequent =
+ match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with
+ | [context, _] ->
+ (let context_len = List.length context in
+ let _, unsh_context, conclusion = unsh_sequent in
+ try
+ (match
+ List.nth unsh_context (List.length unsh_context - context_len - 1)
+ with
+ | None -> assert false (* can't select a restricted hyp *)
+ | Some (name, Cic.Decl ty) ->
+ let pattern =
+ ProofEngineHelpers.pattern_of ~term:ty [term]
+ in
+ HLog.debug (CicPp.ppname name ^ ":" ^ CicPp.ppterm pattern);
+ ~-1, [], pattern
+ | Some (name, Cic.Def (bo, _)) ->
+ let pattern =
+ ProofEngineHelpers.pattern_of ~term:bo [term]
+ in
+ HLog.debug (CicPp.ppname name ^ ":=" ^ CicPp.ppterm pattern);
+ ~-1, [], pattern)
+ with Failure _ | Invalid_argument _ ->
+ let pattern =
+ ProofEngineHelpers.pattern_of ~term:conclusion [term]
+ in
+ HLog.debug ("\\vdash " ^ CicPp.ppterm pattern);
+ ~-1, [], pattern)
+ | _ -> assert false (* since it uses physical equality *)
+ in
+ let paste_as_term_sequent term unsh_sequent =
+ let context' =
+ match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with
+ | [context,_] -> context
+ | _ -> assert false (* since it uses physical equality *)
+ in
+ ~-1, context', term
+ in