helm/gTopLevel/proofEngineHelpers.mli

   1 val identity_relocation_list_for_metavariable :
   2   'a option list -> Cic.term option list
   3 val new_meta : proof:('a * (int * 'b * 'c) list * 'd * 'e) option -> int
   4 val subst_meta_in_proof :
   5   ProofEngineTypes.proof ->
   6   int -> Cic.term -> Cic.metasenv ->
   7   ProofEngineTypes.proof * Cic.metasenv
   8 val subst_meta_and_metasenv_in_proof :
   9   ProofEngineTypes.proof ->
  10   int -> (Cic.term -> Cic.term) -> Cic.metasenv ->
  11   ProofEngineTypes.proof * Cic.metasenv