Merge branch '185_let_premise_apply' into 'master'

[transform apply] let is now a premise for applied condition of apply

See merge request why3/why3!23

examples/bts/185_apply_let.mlw

+module Test
+
+  function f int : int = 17
+  predicate p int int
+  axiom A: forall x y. x = f y -> p x y
+  axiom B: forall y. let x = f y in p x y
+
+  goal g : p 17 42
+
+
+end

examples/bts/185_apply_let/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<file name="../185_apply_let.mlw" proved="true">
+<theory name="Test" proved="true">
+ <goal name="g" proved="true">
+ <transf name="apply" proved="true" arg1="B">
+  <goal name="g.0" proved="true">
+  <transf name="compute_in_goal" proved="true" >
+  </transf>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>

src/transform/apply.ml

@@ -35,6 +35,10 @@ let intros f =
     | Tquant (Tforall, fq) ->
         let vsl, _, fs = t_open_quant fq in
         intros_aux lp (lv @ vsl) fs
+    | Tlet (t, tb) ->
+        let vs, t2 = t_open_bound tb in
+        let f = t_equ (t_var vs) t in
+        intros_aux (f :: lp) ([vs] @ lv) t2
     | _ -> (lp, lv, f) in
   intros_aux [] [] f