bugs avec Pose et Assert

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

26 files changed, 105 insertions, 93 deletions

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 3d6463d1d..9de5e3a2d 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -208,7 +208,7 @@ let cc_tactic gls=
 		   [|outtype;trivial;pred;identity;concl;injt|]) in
 	  let neweq=
 	    mkApp(constr_of_reference Coqlib.glob_eq,[|intype;tt1;tt2|]) in
-	    tclTHENS (true_cut (Some hid) neweq)
+	    tclTHENS (true_cut (Name hid) neweq)
 	      [proof_tac axioms p;exact_check endt] gls
 
 (* Tactic registration *)
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 77d516a13..8fb0ca517 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -56,7 +56,7 @@ let tuple_n n =
       (fun i -> 
 	 let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in
 	 let id' = make_ident "T" (Some i) in
-	 (false, Vernacexpr.AssumExpr ((dummy_loc,id), mkIdentC id')))
+	 (false, Vernacexpr.AssumExpr ((dummy_loc,Name id), mkIdentC id')))
       l1n 
   in
   let cons = make_ident "Build_tuple_" (Some n) in
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 1f9fec6d5..456b00ea9 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -402,8 +402,8 @@ and ct_PREMISE_PATTERN =
 and ct_PROOF_SCRIPT =
     CT_proof_script of ct_COMMAND list
 and ct_RECCONSTR =
-    CT_coerce_CONSTR_to_RECCONSTR of ct_CONSTR
-  | CT_constr_coercion of ct_ID * ct_FORMULA
+    CT_coerce_CONSTR_to_RECCONSTR of ct_ID_OPT * ct_FORMULA
+  | CT_constr_coercion of ct_ID_OPT * ct_FORMULA
 and ct_RECCONSTR_LIST =
     CT_recconstr_list of ct_RECCONSTR list
 and ct_REC_TACTIC_FUN =
@@ -526,7 +526,7 @@ and ct_TACTIC_COM =
   | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_ID_LIST
   | CT_left of ct_SPEC_LIST
   | CT_let_ltac of ct_LET_CLAUSES * ct_LET_VALUE
-  | CT_lettac of ct_ID * ct_FORMULA * ct_CLAUSE
+  | CT_lettac of ct_ID_OPT * ct_FORMULA * ct_CLAUSE
   | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 5d7cff4cf..9f8ece9b2 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -910,9 +910,12 @@ and fPROOF_SCRIPT = function
    (List.iter fCOMMAND l);
    fNODE "proof_script" (List.length l)
 and fRECCONSTR = function
-| CT_coerce_CONSTR_to_RECCONSTR x -> fCONSTR x
+| CT_coerce_CONSTR_to_RECCONSTR (x1,x2) ->
+   fID_OPT x1;
+   fFORMULA x2;
+   fNODE "CONSTR_to_RECCONSTR" 2
 | CT_constr_coercion(x1, x2) ->
-   fID x1;
+   fID_OPT x1;
    fFORMULA x2;
    fNODE "constr_coercion" 2
 and fRECCONSTR_LIST = function
@@ -1244,7 +1247,7 @@ and fTACTIC_COM = function
    fLET_VALUE x2;
    fNODE "let_ltac" 2
 | CT_lettac(x1, x2, x3) ->
-   fID x1;
+   fID_OPT x1;
    fFORMULA x2;
    fCLAUSE x3;
    fNODE "lettac" 3
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 35357d3ab..7cf169ec7 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1022,8 +1022,8 @@ and xlate_tac =
     | TacInstantiate (a, b, _) -> 
 	xlate_error "TODO: Instantiate ... <clause>"
 
-    | TacLetTac (id, c, cl) ->
-        CT_lettac(xlate_ident id, xlate_formula c, 
+    | TacLetTac (na, c, cl) ->
+        CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
 		     but the structures are different *)
 		  xlate_clause cl)
@@ -1032,8 +1032,8 @@ and xlate_tac =
                CT_pose(xlate_id_opt ((0,0), name), xlate_formula c)
     | TacForward (false, name, c) -> 
                CT_assert(xlate_id_opt ((0,0),name), xlate_formula c)
-    | TacTrueCut (idopt, c) -> 
-                             CT_truecut(xlate_ident_opt idopt, xlate_formula c)
+    | TacTrueCut (na, c) -> 
+        CT_truecut(xlate_id_opt ((0,0),na), xlate_formula c)
     | TacAnyConstructor(Some tac) -> 
 	CT_any_constructor
 	(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
@@ -1250,12 +1250,12 @@ let build_constructors l =
 
 let build_record_field_list l =
  let build_record_field (coe,d) = match d with
-  | AssumExpr ((_,id),c) ->
-      if coe then CT_constr_coercion (xlate_ident id, xlate_formula c)
+  | AssumExpr (id,c) ->
+      if coe then CT_constr_coercion (xlate_id_opt id, xlate_formula c)
       else
 	CT_coerce_CONSTR_to_RECCONSTR
-	  (CT_constr (xlate_ident id, xlate_formula c))
-  | DefExpr ((_,id),c,topt) ->
+	  (xlate_id_opt id, xlate_formula c)
+  | DefExpr (id,c,topt) ->
       xlate_error "TODO: manifest fields in Record" in
  CT_recconstr_list (List.map build_record_field l);;
 
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 031fd8b25..3276b7212 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -420,6 +420,7 @@ $$
   \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}
 \nlsep \TERM{generalize}~\PLUS{\tacconstr}
 \nlsep \TERM{generalize}~\TERM{dependent}~\tacconstr
+\nlsep \TERM{set}~\tacconstr~\OPT{\NT{clause}}
 \nlsep \TERM{set}~
   \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}}
 \nlsep \TERM{instantiate}~
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e05ed48c5..f529bf26c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -291,9 +291,9 @@ GEXTEND Gram
 	  TacMutualCofix (id,fd)
 
       | IDENT "Cut"; c = constr -> TacCut c
-      | IDENT "Assert"; c = constr -> TacTrueCut (None,c)
+      | IDENT "Assert"; c = constr -> TacTrueCut (Names.Anonymous,c)
       | IDENT "Assert"; c = constr; ":"; t = constr ->
-          TacTrueCut (Some (snd(coerce_to_id c)),t)
+          TacTrueCut (Names.Name (snd(coerce_to_id c)),t)
       | IDENT "Assert"; c = constr; ":="; b = constr ->
           TacForward (false,Names.Name (snd (coerce_to_id c)),b)
       | IDENT "Pose"; c = constr; ":="; b = constr ->
@@ -301,8 +301,8 @@ GEXTEND Gram
       | IDENT "Pose"; b = constr -> TacForward (true,Names.Anonymous,b)
       | IDENT "Generalize"; lc = LIST1 constr -> TacGeneralize lc
       | IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c
-      | IDENT "LetTac"; id = base_ident; ":="; c = constr; p = clause_pattern
-        -> TacLetTac (id,c,p)
+      | IDENT "LetTac"; (_,na) = name; ":="; c = constr; p = clause_pattern
+        -> TacLetTac (na,c,p)
       | IDENT "Instantiate"; n = natural; c = constr; cls = clause -> 
 	    TacInstantiate (n,c,cls)
       | IDENT "Specialize"; n = OPT natural; lcb = constr_with_bindings ->
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index ccac2ae73..b108ab4b4 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -55,7 +55,7 @@ let test_lpar_idnum_coloneq =
 
 (* idem for (x:t) *)
 let lpar_id_colon =
-  Gram.Entry.of_parser "test_lpar_id_colon"
+  Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       match Stream.npeek 1 strm with
         | [("","(")] ->
@@ -333,18 +333,20 @@ GEXTEND Gram
 
       | IDENT "cut"; c = constr -> TacCut c
       | IDENT "assert"; id = lpar_id_colon; t = lconstr; ")" ->
-          TacTrueCut (Some id,t)
+          TacTrueCut (Names.Name id,t)
       | IDENT "assert"; id = lpar_id_coloneq; b = lconstr; ")" ->
           TacForward (false,Names.Name id,b)
-      | IDENT "assert"; c = constr -> TacTrueCut (None,c)
+      | IDENT "assert"; c = constr -> TacTrueCut (Names.Anonymous,c)
       | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
 	  TacForward (true,Names.Name id,b)
       | IDENT "pose"; b = constr -> TacForward (true,Names.Anonymous,b)
       | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
       | IDENT "generalize"; IDENT "dependent"; c = constr ->
           TacGeneralizeDep c
-      | IDENT "set"; "("; id = base_ident; ":="; c = lconstr; ")";
-          p = clause -> TacLetTac (id,c,p)
+      | IDENT "set"; id = lpar_id_coloneq; c = lconstr; ")";
+          p = clause -> TacLetTac (Names.Name id,c,p)
+      | IDENT "set"; c = constr; p = clause ->
+          TacLetTac (Names.Anonymous,c,p)
       | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")";
 	  cls = clause ->
             TacInstantiate (n,c,cls)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index fe8b462d8..b1e6cda09 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -271,12 +271,12 @@ GEXTEND Gram
     [ [ l = LIST1 onecorec SEP "with" -> l ] ]
   ;
   record_field:
-    [ [ id = identref; oc = of_type_with_opt_coercion; t = constr ->
+    [ [ id = name; oc = of_type_with_opt_coercion; t = constr ->
           (oc,AssumExpr (id,t))
-      | id = identref; oc = of_type_with_opt_coercion; t = constr;
+      | id = name; oc = of_type_with_opt_coercion; t = constr;
 	":="; b = constr ->
 	  (oc,DefExpr (id,b,Some t))
-      | id = identref; ":="; b = constr ->
+      | id = name; ":="; b = constr ->
 	  (false,DefExpr (id,b,None)) ] ]
   ;
   fields:
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 5599f5880..814230304 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -266,12 +266,12 @@ GEXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
-    [ [ id = identref -> (false,AssumExpr(id,CHole loc))
-      | id = identref; oc = of_type_with_opt_coercion; t = lconstr ->
+    [ [ id = name -> (false,AssumExpr(id,CHole loc))
+      | id = name; oc = of_type_with_opt_coercion; t = lconstr ->
          (oc,AssumExpr (id,t))
-      | id = identref; oc = of_type_with_opt_coercion;
+      | id = name; oc = of_type_with_opt_coercion;
              t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t))
-      | id = identref; ":="; b = lconstr ->
+      | id = name; ":="; b = lconstr ->
          match b with
              CCast(_,b,t) -> (false,DefExpr(id,b,Some t))
            | _ -> (false,DefExpr(id,b,None)) ] ]
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 980bc63c2..3a6cfab0e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -472,9 +472,9 @@ and pr_atom1 = function
           prlist (fun (id,c) -> spc () ++ pr_id id ++ pr_arg pr_constr c)
 	  l))
   | TacCut c -> hov 1 (str "Cut" ++ pr_arg pr_constr c)
-  | TacTrueCut (None,c) -> 
+  | TacTrueCut (Anonymous,c) -> 
       hov 1 (str "Assert" ++ pr_arg pr_constr c)
-  | TacTrueCut (Some id,c) -> 
+  | TacTrueCut (Name id,c) -> 
       hov 1 (str "Assert" ++ spc () ++ pr_id id ++ str ":" ++ pr_constr c)
   | TacForward (false,na,c) ->
       hov 1 (str "Assert" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
@@ -485,11 +485,11 @@ and pr_atom1 = function
   | TacGeneralizeDep c ->
       hov 1 (str "Generalize" ++ spc () ++ str "Dependent" ++ spc () ++
       pr_constr c)
-  | TacLetTac (id,c,cl) ->
+  | TacLetTac (na,c,cl) ->
       let pcl = match cl with
           {onhyps=None;onconcl=true;concl_occs=[]} -> mt()
         | _ -> pr_clauses pr_ident cl in
-      hov 1 (str "LetTac" ++ spc () ++ pr_id id ++ str ":=" ++
+      hov 1 (str "LetTac" ++ spc () ++ pr_name na ++ str ":=" ++
              pr_constr c ++ pcl)
   | TacInstantiate (n,c,cls) ->
       hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++ 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e4f90ffa8..8df84e573 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -374,19 +374,19 @@ let rec mlexpr_of_atomic_tactic = function
 
   | Tacexpr.TacCut c ->
       <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
-  | Tacexpr.TacTrueCut (ido,c) ->
-      let ido = mlexpr_of_ident_option ido in
-      <:expr< Tacexpr.TacTrueCut $ido$ $mlexpr_of_constr c$ >>
+  | Tacexpr.TacTrueCut (na,c) ->
+      let na = mlexpr_of_name na in
+      <:expr< Tacexpr.TacTrueCut $na$ $mlexpr_of_constr c$ >>
   | Tacexpr.TacForward (b,na,c) ->
       <:expr< Tacexpr.TacForward $mlexpr_of_bool b$ $mlexpr_of_name na$ $mlexpr_of_constr c$ >>
   | Tacexpr.TacGeneralize cl ->
       <:expr< Tacexpr.TacGeneralize $mlexpr_of_list mlexpr_of_constr cl$ >>
   | Tacexpr.TacGeneralizeDep c ->
       <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >>
-  | Tacexpr.TacLetTac (id,c,cl) ->
-      let id = mlexpr_of_ident id in
+  | Tacexpr.TacLetTac (na,c,cl) ->
+      let na = mlexpr_of_name na in
       let cl = mlexpr_of_clause_pattern cl in
-      <:expr< Tacexpr.TacLetTac $id$ $mlexpr_of_constr c$ $cl$ >>
+      <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ >>
 
   (* Derived basic tactics *)
   | Tacexpr.TacSimpleInduction (h,_) ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 743f3cd09..cf4741e5e 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -129,11 +129,11 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacCofix of identifier option
   | TacMutualCofix of identifier * (identifier * 'constr) list
   | TacCut of 'constr
-  | TacTrueCut of identifier option * 'constr 
+  | TacTrueCut of name * 'constr 
   | TacForward of bool * name * 'constr
   | TacGeneralize of 'constr list
   | TacGeneralizeDep of 'constr
-  | TacLetTac of identifier * 'constr * 'id gclause
+  | TacLetTac of name * 'constr * 'id gclause
   | TacInstantiate of int * 'constr * 'id gclause
 
   (* Derived basic tactics *)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index ebcddc71c..5b35fcb86 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -40,12 +40,12 @@ let h_mutual_cofix id l =
   abstract_tactic (TacMutualCofix (id,l)) (mutual_cofix id l)
 
 let h_cut c          = abstract_tactic (TacCut c) (cut c)
-let h_true_cut ido c = abstract_tactic (TacTrueCut (ido,c)) (true_cut ido c)
+let h_true_cut na c = abstract_tactic (TacTrueCut (na,c)) (true_cut na c)
 let h_forward b na c = abstract_tactic (TacForward (b,na,c)) (forward b na c)
 let h_generalize cl  = abstract_tactic (TacGeneralize cl) (generalize cl)
 let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c)
-let h_let_tac id c cl =
-  abstract_tactic (TacLetTac (id,c,cl)) (letin_tac true (Names.Name id) c cl)
+let h_let_tac na c cl =
+  abstract_tactic (TacLetTac (na,c,cl)) (letin_tac true na c cl)
 let h_instantiate n c cls = 
   abstract_tactic (TacInstantiate (n,c,cls))
     (Evar_refiner.instantiate n c (simple_clause_of cls))
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 1ea438874..364e21969 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -44,11 +44,11 @@ val h_mutual_cofix    : identifier -> (identifier * constr) list -> tactic
 val h_cofix           : identifier option -> tactic
 
 val h_cut             : constr -> tactic 
-val h_true_cut        : identifier option -> constr -> tactic 
+val h_true_cut        : name -> constr -> tactic 
 val h_generalize      : constr list -> tactic 
 val h_generalize_dep  : constr -> tactic 
 val h_forward         : bool -> name -> constr -> tactic 
-val h_let_tac         : identifier -> constr -> Tacticals.clause -> tactic
+val h_let_tac         : name -> constr -> Tacticals.clause -> tactic
 val h_instantiate     : int -> constr -> Tacticals.clause -> tactic
 
 (* Derived basic tactics *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index fddcf4761..2902f37e0 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -467,7 +467,7 @@ let raw_inversion inv_kind indbinding id status names gl =
       case_nodep_then_using 
   in
   (tclTHENS
-     (true_cut None cut_concl)
+     (true_cut Anonymous cut_concl)
      [case_tac names 
        (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
        (Some elim_predicate) ([],[]) newc;
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index eff274988..2217dbe10 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -608,14 +608,15 @@ let rec intern_atomic lf ist x =
       let f (id,c) = (intern_ident lf ist id,intern_constr ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
   | TacCut c -> TacCut (intern_constr ist c)
-  | TacTrueCut (ido,c) ->
-      TacTrueCut (option_app (intern_ident lf ist) ido, intern_constr ist c)
-  | TacForward (b,na,c) -> TacForward (b,intern_name lf ist na,intern_constr ist c)
+  | TacTrueCut (na,c) ->
+      TacTrueCut (intern_name lf ist na, intern_constr ist c)
+  | TacForward (b,na,c) ->
+      TacForward (b,intern_name lf ist na,intern_constr ist c)
   | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
-  | TacLetTac (id,c,cls) ->
-      let id = intern_ident lf ist id in
-      TacLetTac (id,intern_constr ist c,
+  | TacLetTac (na,c,cls) ->
+      let na = intern_name lf ist na in
+      TacLetTac (na,intern_constr ist c,
                  (clause_app (intern_hyp_location ist) cls))
   | TacInstantiate (n,c,cls) -> 
       TacInstantiate (n,intern_constr ist c,
@@ -1621,15 +1622,15 @@ and interp_atomic ist gl = function
       let f (id,c) = (eval_ident ist id,pf_interp_constr ist gl c) in
       h_mutual_cofix (eval_ident ist id) (List.map f l)
   | TacCut c -> h_cut (pf_interp_constr ist gl c)
-  | TacTrueCut (ido,c) ->
-      h_true_cut (eval_opt_ident ist ido) (pf_interp_constr ist gl c)
+  | TacTrueCut (na,c) ->
+      h_true_cut (eval_name ist na) (pf_interp_constr ist gl c)
   | TacForward (b,na,c) ->
       h_forward b (eval_name ist na) (pf_interp_constr ist gl c)
   | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
-  | TacLetTac (id,c,clp) ->
+  | TacLetTac (na,c,clp) ->
       let clp = interp_clause ist gl clp in
-      h_let_tac (eval_ident ist id) (pf_interp_constr ist gl c) clp
+      h_let_tac (eval_name ist na) (pf_interp_constr ist gl c) clp
   | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c)
       (clause_app (interp_hyp_location ist gl) ido)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2084cac2a..d739cb225 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -505,15 +505,15 @@ let cut_and_apply c gl =
 (*     Cut tactics        *)
 (**************************)
 
-let true_cut idopt c gl =
+let true_cut na c gl =
   match kind_of_term (hnf_type_of gl c) with
     | Sort s -> 
 	let id =
-	  match idopt with
-	  | None -> 
+	  match na with
+	  | Anonymous -> 
               let d = match s with Prop _ -> "H" | Type _ -> "X" in
               fresh_id [] (id_of_string d) gl
-	  | Some id -> id
+	  | Name id -> id
 	in
 	internal_cut id c gl
     | _  -> error "Not a proposition or a type"
@@ -759,9 +759,12 @@ let check_hypotheses_occurrences_list env (_,occl) =
 
 let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
 
-(* Tactic Pose should not perform any replacement (as specified in
-   the doc), but it does in the conclusion! *) 
-let forward b na c = letin_tac b na c onConcl
+(* Tactic Assert (b=false) and Pose (b=true):
+   the behaviour of Pose is corrected by the translator.
+   not that of Assert *)
+let forward b na c =
+  let wh =  if !Options.v7 && b then onConcl else nowhere in
+  letin_tac b na c wh
 
 (********************************************************************)
 (*               Exact tactics                                      *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f5c761994..ee65f1332 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -234,7 +234,7 @@ val cut_intro                   : constr -> tactic
 val cut_replacing               : identifier -> constr -> tactic
 val cut_in_parallel             : constr list -> tactic
 
-val true_cut                    : identifier option -> constr -> tactic
+val true_cut                    : name -> constr -> tactic
 val letin_tac                   : bool -> name -> constr -> clause -> tactic
 val forward                     : bool -> name -> constr -> tactic
 val generalize                  : constr list -> tactic
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index f0b4793eb..50b38c535 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -1901,12 +1901,12 @@ assert (H : adapted_couple f a b (subdivision f) (subdivision_val f));
           [ symmetry  in |- *; apply H1 | rewrite (StepFun_P8 H0 H2); ring ] ] ] ].
 rewrite Ropp_involutive; eapply StepFun_P17;
  [ apply StepFun_P1
- | apply StepFun_P2; assert (H := StepFun_P6 (pre f)); unfold IsStepFun in H;
+ | apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H;
     elim H; intros; unfold is_subdivision in |- *; 
     elim p; intros; apply p0 ].
 apply Ropp_eq_compat; eapply StepFun_P17;
  [ apply StepFun_P1
- | apply StepFun_P2; assert (H := StepFun_P6 (pre f)); unfold IsStepFun in H;
+ | apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H;
     elim H; intros; unfold is_subdivision in |- *; 
     elim p; intros; apply p0 ].
 assert (H : a < b);
diff --git a/theories7/Reals/RiemannInt_SF.v b/theories7/Reals/RiemannInt_SF.v
index f81c57997..f1f2a4737 100644
--- a/theories7/Reals/RiemannInt_SF.v
+++ b/theories7/Reals/RiemannInt_SF.v
@@ -982,8 +982,8 @@ Qed.
 Lemma StepFun_P39 : (a,b:R;f:(StepFun a b)) (RiemannInt_SF f)==(Ropp (RiemannInt_SF (mkStepFun (StepFun_P6 (pre f))))).
 Intros; Unfold RiemannInt_SF; Case (total_order_Rle a b); Case (total_order_Rle b a); Intros.
 Assert H : (adapted_couple f a b (subdivision f) (subdivision_val f)); [Apply StepFun_P1 | Assert H0 : (adapted_couple (mkStepFun (StepFun_P6 (pre f))) b a (subdivision (mkStepFun (StepFun_P6 (pre f)))) (subdivision_val (mkStepFun (StepFun_P6 (pre f))))); [Apply StepFun_P1 | Assert H1 : a==b; [Apply Rle_antisym; Assumption | Rewrite (StepFun_P8 H H1); Assert H2 : b==a; [Symmetry; Apply H1 | Rewrite (StepFun_P8 H0 H2); Ring]]]].
-Rewrite Ropp_Ropp; EApply StepFun_P17; [Apply StepFun_P1 | Apply StepFun_P2; Assert H := (StepFun_P6 (pre f)); Unfold IsStepFun in H; Elim H; Intros; Unfold is_subdivision; Elim p; Intros; Apply p0].
-Apply eq_Ropp; EApply StepFun_P17; [Apply StepFun_P1 | Apply StepFun_P2; Assert H := (StepFun_P6 (pre f)); Unfold IsStepFun in H; Elim H; Intros; Unfold is_subdivision; Elim p; Intros; Apply p0].
+Rewrite Ropp_Ropp; EApply StepFun_P17; [Apply StepFun_P1 | Apply StepFun_P2; Pose H := (StepFun_P6 (pre f)); Unfold IsStepFun in H; Elim H; Intros; Unfold is_subdivision; Elim p; Intros; Apply p0].
+Apply eq_Ropp; EApply StepFun_P17; [Apply StepFun_P1 | Apply StepFun_P2; Pose H := (StepFun_P6 (pre f)); Unfold IsStepFun in H; Elim H; Intros; Unfold is_subdivision; Elim p; Intros; Apply p0].
 Assert H : ``a<b``; [Auto with real | Assert H0 : ``b<a``; [Auto with real | Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H H0))]].
 Qed.
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index a2a679cb1..89cb35b74 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -32,17 +32,15 @@ open Topconstr
 
 (********** definition d'un record (structure) **************)
 
-let name_of id = if id = wildcard then Anonymous else Name id
-
 let interp_decl sigma env = function
-  | Vernacexpr.AssumExpr((_,id),t) -> (name_of id,None,interp_type Evd.empty env t)
+  | Vernacexpr.AssumExpr((_,id),t) -> (id,None,interp_type Evd.empty env t)
   | Vernacexpr.DefExpr((_,id),c,t) ->
       let c = match t with
 	| None -> c
 	| Some t -> mkCastC (c,t)
       in
       let j = judgment_of_rawconstr Evd.empty env c in
-      (Name id,Some j.uj_val, j.uj_type)
+      (id,Some j.uj_val, j.uj_type)
 
 let typecheck_params_and_fields ps fs =
   let env0 = Global.env () in
@@ -210,10 +208,11 @@ let declare_projections indsp coers fields =
 let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let coers,fs = List.split cfs in
   let nparams = local_binders_length ps in
-  let extract_name = function
-      Vernacexpr.AssumExpr((_,id),_) -> id
-    | Vernacexpr.DefExpr ((_,id),_,_) -> id in
-  let allnames =  idstruc::(List.map extract_name fs) in
+  let extract_name acc = function
+      Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
+    | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
+    | _ -> acc in
+  let allnames =  idstruc::(List.fold_left extract_name [] fs) in
   if not (list_distinct allnames) then error "Two objects have the same name";
   (* Now, younger decl in params and fields is on top *)
   let params,fields = typecheck_params_and_fields ps fs in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index fe07a53d5..9fd934d56 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -26,6 +26,7 @@ open Libnames
 open Nametab
 
 type lident = identifier located
+type lname = name located
 type lstring = string
 type lreference = reference
 
@@ -147,8 +148,8 @@ type definition_expr =
       * constr_expr option
 
 type local_decl_expr =
-  | AssumExpr of lident * constr_expr
-  | DefExpr of lident * constr_expr * constr_expr option
+  | AssumExpr of lname * constr_expr
+  | DefExpr of lname * constr_expr * constr_expr option
 
 type module_binder = lident list * module_type_ast
 
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index ed4417797..1da57f920 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -216,9 +216,9 @@ let pr_let_binder pr x a =
          pr_sep_com (fun () -> brk(0,1)) (pr ltop) a)
 
 let rec extract_prod_binders = function
-  | CLetIn (loc,na,b,c) as x ->
+(*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_prod_binders c in
-      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
   | CProdN (loc,[],c) ->
       extract_prod_binders c
   | CProdN (loc,(nal,t)::bl,c) ->
@@ -227,9 +227,9 @@ let rec extract_prod_binders = function
   | c -> [], c
 
 let rec extract_lam_binders = function
-  | CLetIn (loc,na,b,c) as x ->
+(*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_lam_binders c in
-      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
   | CLambdaN (loc,[],c) ->
       extract_lam_binders c
   | CLambdaN (loc,(nal,t)::bl,c) ->
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index a6ff11b0e..5e0cc68ba 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -483,9 +483,9 @@ and pr_atom1 env = function
       hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
              str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l)
   | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
-  | TacTrueCut (None,c) -> 
+  | TacTrueCut (Anonymous,c) -> 
       hov 1 (str "assert" ++ pr_constrarg env c)
-  | TacTrueCut (Some id,c) -> 
+  | TacTrueCut (Name id,c) -> 
       hov 1 (str "assert" ++ spc () ++
              hov 1 (str"(" ++ pr_id id ++ str " :" ++
                     pr_lconstrarg env c ++ str")"))
@@ -495,7 +495,7 @@ and pr_atom1 env = function
                     pr_lconstrarg env c ++ str")"))
   | TacForward (true,Anonymous,c) ->
       if Options.do_translate () then
-        (* Pose was buggy and was wrongly substituting in conclusion in v7 *)
+        (* Pose was buggy and was wrongly substituted in conclusion in v7 *)
         hov 1 (str "set" ++ pr_constrarg env c)
       else
         hov 1 (str "pose" ++ pr_constrarg env c)
@@ -514,7 +514,9 @@ and pr_atom1 env = function
   | TacGeneralizeDep c ->
       hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
              pr_constrarg env c)
-  | TacLetTac (id,c,cl) ->
+  | TacLetTac (Anonymous,c,cl) ->
+      hov 1 (str "set" ++ pr_constrarg env c) ++ pr_clauses pr_ident cl
+  | TacLetTac (Name id,c,cl) ->
       hov 1 (str "set" ++ spc () ++
              hov 1 (str"(" ++ pr_id id ++ str " :=" ++
                     pr_lconstrarg env c ++ str")") ++
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 41f36ccda..6756e3157 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -824,16 +824,16 @@ let rec pr_vernac = function
   | VernacRecord (b,(oc,name),ps,s,c,fs) ->
       let pr_record_field = function
         | (oc,AssumExpr (id,t)) ->
-            hov 1 (pr_lident id ++
+            hov 1 (pr_lname id ++
             (if oc then str" :>" else str" :") ++ spc() ++
             pr_type t)
         | (oc,DefExpr(id,b,opt)) -> (match opt with
 	    | Some t ->
-                hov 1 (pr_lident id ++
+                hov 1 (pr_lname id ++
                 (if oc then str" :>" else str" :") ++ spc() ++
                 pr_type t ++ str" :=" ++ pr_lconstr b)
 	    | None ->
-                hov 1 (pr_lident id ++ str" :=" ++ spc() ++
+                hov 1 (pr_lname id ++ str" :=" ++ spc() ++
                 pr_lconstr b)) in
       hov 2
         (str (if b then "Record" else "Structure") ++