From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 1 Jul 2005 11:13:10 +0000 (+0000)
Subject: Signature of fwdSimpl changed to get rid of a warning.
X-Git-Tag: PRE_GETTER_STORAGE~74
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=79490653c4a0cf5f8e75665feffbf92082b8a680;p=helm.git

Signature of fwdSimpl changed to get rid of a warning.
---

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