From 79490653c4a0cf5f8e75665feffbf92082b8a680 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 1 Jul 2005 11:13:10 +0000 Subject: [PATCH] Signature of fwdSimpl changed to get rid of a warning. --- helm/ocaml/tactics/fwdSimplTactic.ml | 6 ++++-- helm/ocaml/tactics/fwdSimplTactic.mli | 2 +- helm/ocaml/tactics/tactics.mli | 2 +- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index e7d25daae..6f64855d1 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -110,8 +110,10 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub (* fwd **********************************************************************) -let fwd_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) - ~hyp ~dbd = +let fwd_simpl_tac + ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + ~dbd hyp + = let find_type metasenv context = let rec aux p = function | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli index f8101b34b..e16bd5719 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.mli +++ b/helm/ocaml/tactics/fwdSimplTactic.mli @@ -29,4 +29,4 @@ val lapply_tac: val fwd_simpl_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - hyp:string -> dbd:Mysql.dbd -> ProofEngineTypes.tactic + dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index c155d67d3..32bbf2c6a 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -38,7 +38,7 @@ val fold : val fourier : ProofEngineTypes.tactic val fwd_simpl : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - hyp:string -> dbd:Mysql.dbd -> ProofEngineTypes.tactic + dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic val generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic -- 2.39.2