bugs avec Pose et Assert

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

5 files changed, 19 insertions, 16 deletions

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 3d6463d1d9..9de5e3a2d0 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 77d516a136..8fb0ca5171 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 1f9fec6d58..456b00ea99 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 5d7cff4cf5..9f8ece9b23 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 35357d3ab7..7cf169ec7d 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);;