X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftactics.mli;h=5eb66704f7fe61f2d76cc379709ef49c7e1ecc19;hb=abd9e5cfa8e7b6923e0664a4813a0a842f5c4e76;hp=a91985290838195bfcd4a9813a0d5de8b5c674a9;hpb=aeec9dd128be72caf5a39bac3a0ef34b564ecd8b;p=helm.git diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index a91985290..5eb66704f 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -2,15 +2,17 @@ val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic -val auto : ?num:int option -> dbd:Mysql.dbd -> ProofEngineTypes.tactic -val auto_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic +val auto : ?num:int option -> Mysql.dbd -> ProofEngineTypes.tactic +val auto_new : + ?depth:int -> + ?width:int -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic val compare : term:Cic.term -> ProofEngineTypes.tactic val constructor : n:int -> ProofEngineTypes.tactic val contradiction : ProofEngineTypes.tactic val cut : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - term:Cic.term -> ProofEngineTypes.tactic + Cic.term -> ProofEngineTypes.tactic val decide_equality : ProofEngineTypes.tactic val decompose : ?uris_choice_callback:((UriManager.uri * int * @@ -42,27 +44,31 @@ val intros : val left : ProofEngineTypes.tactic val letin : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - term:Cic.term -> ProofEngineTypes.tactic -val reduce : - also_in_hypotheses:bool -> - terms:Cic.term list option -> ProofEngineTypes.tactic + Cic.term -> ProofEngineTypes.tactic +val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic val replace : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic -val rewrite_back : term:Cic.term -> ProofEngineTypes.tactic -val rewrite_back_simpl : term:Cic.term -> ProofEngineTypes.tactic -val rewrite : term:Cic.term -> ProofEngineTypes.tactic -val rewrite_simpl : term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back : + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic +val rewrite_back_simpl : + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic +val rewrite : + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic +val rewrite_simpl : + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic -val simpl : - also_in_hypotheses:bool -> - terms:Cic.term list option -> ProofEngineTypes.tactic +val simpl : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic -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 whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val normalize : pattern:ProofEngineTypes.pattern -> 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