]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/fwdSimplTactic.ml
Signature of fwdSimpl changed to get rid of a warning.
[helm.git] / helm / ocaml / tactics / fwdSimplTactic.ml
index e7d25daae63ecc24e4457a91b3188d49054105a9..6f64855d1b4d1432ae07d06d600b26ec199c8af6 100644 (file)
@@ -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