val whd_tac:
also_in_hypotheses:bool -> terms:(Cic.term list option) ->
ProofEngineTypes.tactic
+val normalize_tac:
+ also_in_hypotheses:bool -> terms:(Cic.term list option) ->
+ ProofEngineTypes.tactic
val fold_tac:
reduction:(Cic.context -> Cic.term -> Cic.term) ->