-val whd :
- also_in_hypotheses:bool ->
- terms:Cic.term list option -> ProofEngineTypes.tactic
-val normalize :
- also_in_hypotheses:bool ->
- terms:Cic.term list option -> ProofEngineTypes.tactic
-val fwd_simpl : hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
-val lapply :
- ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?substs:(Cic.name * Cic.term) list -> Cic.term -> ProofEngineTypes.tactic
+val unfold :
+ ProofEngineTypes.lazy_term option ->
+ pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic