Unification de TacLetRecIn et TacLetIn. En particulier, on peut

maintenant écrire des fonctions récursives qui n'ont pas l'apparence
d'être fonctionnelle. La sémantique reste toutefois différente. Par
exemple, dans

Ltac is := 
  let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
  i.

l'évaluation de i est paresseuse, alors que dans une version non récursive

Ltac is := 
  let i := match goal with |- ?A -> ?B => intro | _ => idtac end in
  i.

l'évaluation de i est forte (et échoue sur le "match" qui n'est pas
autorisé à retourner une tactique).

(note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10495 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 0 deletions

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 880b5da11..9dd7b273d 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -198,3 +198,14 @@ Goal forall x : nat, x = 1 -> x + x + x = 3.
 intros x H.
 test x 2.
 Abort.
+
+(* Utilisation de let rec sans arguments *)
+
+Ltac is := 
+  let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
+  i.
+
+Goal True -> True -> True.
+is.
+exact I.
+Abort.