From a502c83b5c9878ef30a8f25f945ff0ef7b70f0f6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 1 Feb 2008 08:55:51 +0000 Subject: 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 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- contrib/setoid_ring/newring.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'contrib/setoid_ring/newring.ml4') diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 2c6e0ebcd..6c3b6337a 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -771,7 +771,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in Tacinterp.eval_tactic (TacLetIn - ([(dummy_loc,id_of_string"f"),None,Tacexp f], + (false,[(dummy_loc,id_of_string"f"),Tacexp f], ltac_lcall "f" [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac;lH;rl])) gl @@ -1112,7 +1112,7 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl = let posttac = Tacexp(TacFun([None],e.field_post_tac)) in Tacinterp.eval_tactic (TacLetIn - ([(dummy_loc,id_of_string"f"),None,Tacexp f], + (false,[(dummy_loc,id_of_string"f"),Tacexp f], ltac_lcall "f" [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl -- cgit v1.2.3