nouvelle syntaxe de ltac

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

2 files changed, 33 insertions, 65 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 460d0bc380..da5ab1772d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -689,17 +689,14 @@ and intern_tactic_seq ist = function
   | TacLetIn (l,u) ->
       let l = List.map
         (fun (n,c,b) ->
-          (n,option_app (intern_constr_may_eval ist) c, intern_tacarg !strict_check ist b)) l in
+          (n,option_app (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
       let (l1,l2) = ist.ltacvars in
       let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
       ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
-  | TacLetCut l ->
-      let f (n,c,t) = (n,intern_constr_may_eval ist c,intern_tacarg !strict_check ist t) in
-      ist.ltacvars, TacLetCut (List.map f l)
   | TacMatchContext (lr,lmr) ->
       ist.ltacvars, TacMatchContext(lr, intern_match_rule ist lmr)
   | TacMatch (c,lmr) ->
-      ist.ltacvars, TacMatch (intern_constr_may_eval ist c,intern_match_rule ist lmr)
+      ist.ltacvars, TacMatch (intern_tactic ist c,intern_match_rule ist lmr)
   | TacId -> ist.ltacvars, TacId
   | TacFail _ as x -> ist.ltacvars, x
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
@@ -1230,7 +1227,6 @@ and eval_tactic ist = function
   | TacFun (it,body) -> assert false
   | TacLetRecIn (lrc,u) -> assert false
   | TacLetIn (l,u) -> assert false
-  | TacLetCut l -> letcut_interp ist l
   | TacMatchContext _ -> assert false
   | TacMatch (c,lmr) -> assert false
   | TacId -> tclIDTAC
@@ -1347,15 +1343,16 @@ and interp_letin ist gl = function
       check_is_value v;
       (id,v):: (interp_letin ist gl tl)
   | ((loc,id),Some com,tce)::tl ->
-    let typ = interp_may_eval pf_interp_constr ist gl com
+    let env = pf_env gl in
+    let typ = constr_of_value env (val_interp ist gl com)
     and v = interp_tacarg ist gl tce in
     let csr = 
       try
-	constr_of_value (pf_env gl) v
+	constr_of_value env v
       with Not_found ->
       try
 	let t = tactic_of_value v in
-	let ndc = Environ.named_context (pf_env gl) in
+	let ndc = Environ.named_context env in
 	start_proof id IsLocal ndc typ (fun _ _ -> ());
 	by t;
 	let (_,({const_entry_body = pft},_,_)) = cook_proof () in
@@ -1367,32 +1364,6 @@ and interp_letin ist gl = function
           (str "Term or fully applied tactic expected in Let")
     in (id,VConstr (mkCast (csr,typ)))::(interp_letin ist gl tl)
 
-(* Interprets the clauses of a LetCut *)
-and letcut_interp ist = function 
-  | [] -> tclIDTAC
-  | (id,c,tce)::tl -> fun gl ->
-    let typ = interp_constr_may_eval ist gl c
-    and v = interp_tacarg ist gl tce in
-    let csr = 
-      try
-	constr_of_value (pf_env gl) v
-      with Not_found ->
-      try
-	let t = tactic_of_value v in
-	start_proof id IsLocal (pf_hyps gl) typ (fun _ _ -> ());
-	by t;
-	let (_,({const_entry_body = pft},_,_)) = cook_proof () in
-	delete_proof (dummy_loc,id);
-        pft
-      with | NotTactic ->
-	delete_proof (dummy_loc,id);
-	errorlabstrm "Tacinterp.interp_letin"
-          (str "Term or fully applied tactic expected in Let")
-    in
-    let cutt = h_cut typ
-    and exat = h_exact csr in
-    tclTHENSV cutt [|tclTHEN (introduction id) (letcut_interp ist tl);exat|] gl
-
 (* Interprets the Match Context expressions *)
 and match_context_interp ist g lr lmr =
   let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps =
@@ -1561,8 +1532,8 @@ and match_interp ist g constr lmr =
     | _ ->
       errorlabstrm "Tacinterp.apply_match" (str
         "No matching clauses for Match") in
-  let csr = interp_constr_may_eval ist g constr in
   let env = pf_env g in
+  let csr = constr_of_value env (val_interp ist g constr) in
   let ilr = read_match_rule (project g) env (fst (constr_list ist env)) lmr in
   apply_match ist csr ilr
 
@@ -1927,15 +1898,12 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in
       TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr))
   | TacLetIn (l,u) ->
-      let l = List.map (fun (n,c,b) -> (n,option_app (subst_raw_may_eval subst) c,subst_tacarg subst b)) l in
+      let l = List.map (fun (n,c,b) -> (n,option_app (subst_tactic subst) c,subst_tacarg subst b)) l in
       TacLetIn (l,subst_tactic subst u)
-  | TacLetCut l ->
-      let f (n,c,t) = (n,subst_raw_may_eval subst c,subst_tacarg subst t) in
-      TacLetCut (List.map f l)
   | TacMatchContext (lr,lmr) ->
       TacMatchContext(lr, subst_match_rule subst lmr)
   | TacMatch (c,lmr) ->
-      TacMatch (subst_raw_may_eval subst c,subst_match_rule subst lmr)
+      TacMatch (subst_tactic subst c,subst_match_rule subst lmr)
   | TacId | TacFail _ as x -> x
   | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
   | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index ec05d2b400..c9a5c2cc01 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -55,13 +55,13 @@ let is_disj ist =
 let not_dep_intros ist =
   <:tactic<
   repeat match context with
-  | [|- (?X1 -> ?X2) ] => intro
-  | [|- (Coq.Init.Logic.iff _ _)] => unfold Coq.Init.Logic.iff
-  | [|- (Coq.Init.Logic.not _)]   => unfold Coq.Init.Logic.not
-  | [ H:(Coq.Init.Logic.iff _ _)|- _] => unfold Coq.Init.Logic.iff in H
-  | [ H:(Coq.Init.Logic.not _)|-_]    => unfold Coq.Init.Logic.not in H
-  | [ H:(Coq.Init.Logic.iff _ _)->_|- _] => unfold Coq.Init.Logic.iff in H
-  | [ H:(Coq.Init.Logic.not _)->_|-_]    => unfold Coq.Init.Logic.not in H
+  | |- (?X1 -> ?X2) => intro
+  | |- (Coq.Init.Logic.iff _ _) => unfold Coq.Init.Logic.iff
+  | |- (Coq.Init.Logic.not _)   => unfold Coq.Init.Logic.not
+  | H:(Coq.Init.Logic.iff _ _)|- _ => unfold Coq.Init.Logic.iff in H
+  | H:(Coq.Init.Logic.not _)|-_    => unfold Coq.Init.Logic.not in H
+  | H:(Coq.Init.Logic.iff _ _)->_|- _ => unfold Coq.Init.Logic.iff in H
+  | H:(Coq.Init.Logic.not _)->_|-_    => unfold Coq.Init.Logic.not in H
   end >>
 				      
 let axioms ist =
@@ -69,9 +69,9 @@ let axioms ist =
   and t_is_empty = tacticIn is_empty in
     <:tactic<
     match reverse context with
-      |[|- ?X1] => $t_is_unit; constructor 1
-      |[_:?X1 |- _] => $t_is_empty; elimtype X1; assumption
-      |[_:?X1 |- ?X1] => assumption
+      | |- ?X1 => $t_is_unit; constructor 1
+      | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
+      | _:?X1 |- ?X1 => assumption
     end >>
 
 
@@ -84,27 +84,27 @@ let simplif ist =
     $t_not_dep_intros;
     repeat
        (match reverse context with
-        | [id: (?X1 _ _) |- _] =>
+        | id: (?X1 _ _) |- _ =>
             $t_is_conj; elim id; do 2 intro; clear id
-        | [id: (?X1 _ _) |- _] => $t_is_disj; elim id; intro; clear id
-        | [id0: ?X1-> ?X2, id1: ?X1|- _] =>
+        | id: (?X1 _ _) |- _ => $t_is_disj; elim id; intro; clear id
+        | id0: ?X1-> ?X2, id1: ?X1|- _ =>
 	    (* generalize (id0 id1); intro; clear id0 does not work
 	       (see Marco Maggiesi's bug PR#301)
 	    so we instead use Assert and exact. *)
 	    assert X2; [exact (id0 id1) | clear id0]
-        | [id: ?X1 -> ?X2|- _] =>
+        | id: ?X1 -> ?X2|- _ =>
           $t_is_unit; cut X2;
 	    [ intro; clear id
 	    | (* id : ?X1 -> ?X2 |- ?X2 *)
 	      cut X1; [exact id| constructor 1; fail]
 	    ]
-        | [id: (?X1 ?X2 ?X3) -> ?X4|- _] =>
+        | id: (?X1 ?X2 ?X3) -> ?X4|- _ =>
           $t_is_conj; cut (X2-> X3-> X4);
 	    [ intro; clear id
 	    | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X3 -> ?X4 *)
 	      intro; intro; cut (X1 X2 X3); [exact id| split; assumption]
 	    ]
-        | [id: (?X1 ?X2 ?X3) -> ?X4|- _] =>
+        | id: (?X1 ?X2 ?X3) -> ?X4|- _ =>
           $t_is_disj;
 	    cut (X3-> X4);
 	      [cut (X2-> X4);
@@ -115,7 +115,7 @@ let simplif ist =
 	      | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X3 -> ?X4 *)
 		intro; cut (X1 X2 X3); [exact id| right; assumption]
 	      ]
-        | [|- (?X1 _ _)] => $t_is_conj; split
+        | |- (?X1 _ _) => $t_is_conj; split
         end;
         $t_not_dep_intros) >>
 
@@ -128,20 +128,20 @@ let rec tauto_intuit t_reduce solver ist =
   <:tactic<
    ($t_simplif;$t_axioms
    || match reverse context with
-      | [id:(?X1-> ?X2)-> ?X3|- _] =>
+      | id:(?X1-> ?X2)-> ?X3|- _ =>
 	  cut X3;
 	    [ intro; clear id; $t_tauto_intuit 
 	    | cut (X1 -> X2);
 		[ exact id
 		| generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
 		  solve [ $t_tauto_intuit ]]]
-      | [|- (?X1 _ _)] =>
+      | |- (?X1 _ _) =>
           $t_is_disj; solve [left;$t_tauto_intuit | right;$t_tauto_intuit]
       end
     ||
     (* NB: [|- _ -> _] matches any product *)
-    match context with |[ |- _ -> _ ] => intro; $t_tauto_intuit
-    |[ |- _ ] => $t_reduce;$t_solver
+    match context with | |- _ -> _ => intro; $t_tauto_intuit
+    |  |- _  => $t_reduce;$t_solver
     end
     ||
     $t_solver
@@ -150,8 +150,8 @@ let rec tauto_intuit t_reduce solver ist =
 let reduction_not_iff=interp
  <:tactic<repeat 
   match context with 
-  | [ |- _ ] => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff 
-  | [ H:_ |- _ ] => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H
+  | |- _     => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff 
+  | H:_ |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H
   end >>
 
 
@@ -174,7 +174,7 @@ let default_intuition_tac = interp <:tactic< auto with * >>
 let q_elim tac=
   <:tactic<
   match context with 
-  [ x : ?X1, H : ?X1 -> _ |- _ ] => generalize (H x); clear H; $tac
+    x : ?X1, H : ?X1 -> _ |- _ => generalize (H x); clear H; $tac
   end >>
 
 let rec lfo n gl=