[ porting from CerCo's Matita ]

[helm.git] / matita / components / ng_tactics / nTacStatus.mli

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index f9eb1917c3c243ba72574b1626bc415a464514f5..30989faba8dcfeb6c96400cbe96bdc3932ae77fa 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.mli
+++ b/matita/components/ng_tactics/nTacStatus.mli
@@ -107,7 +107,7 @@ val mk_meta:
  #pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
    [ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
      'status * cic_term
-val instantiate: #pstatus as 'status -> int -> cic_term -> 'status
+val instantiate: #pstatus as 'status -> ?refine:bool -> int -> cic_term -> 'status
 val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status
 
 val select_term: