Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

5 files changed, 86 insertions, 81 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 6ec0fac4..767a7dd6 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -161,21 +161,22 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
-	     (add_hint_list hintl local_db) g'))) ::
+	     (Hint_db.add_list hintl local_db) g'))) ::
     (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
 
 and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
-  let flags = Auto.auto_unif_flags in
   let hintl =
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x))
-	(Hint_db.map_all hdc db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) 
-	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in 
   let tac_of_hint = 
     fun (st, ({pri=b; pat = p; code=t} as _patac)) -> 
@@ -279,7 +280,7 @@ module MySearchProblem = struct
 	     let hintl = 
 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 	     in
-             let ldb = add_hint_list hintl (List.hd s.localdb) in
+             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
 	     { depth = s.depth; tacres = res; 
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb })
@@ -375,7 +376,7 @@ let rec trivial_fail_db db_list local_db gl =
     tclTHEN intro 
       (fun g'->
 	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-	 in trivial_fail_db db_list (add_hint_list hintl local_db) g')
+	 in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
   in
   tclFIRST 
     (assumption::intro_tac::
@@ -383,14 +384,15 @@ let rec trivial_fail_db db_list local_db gl =
 	(trivial_resolve db_list local_db (pf_concl gl)))) gl
 
 and my_find_search db_list local_db hdc concl =
-  let flags = Auto.auto_unif_flags in
   let tacl = 
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) 
-	(Hint_db.map_all hdc db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
-	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in
   List.map 
     (fun (st, {pri=b; pat=p; code=t} as _patac) -> 
@@ -477,7 +479,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   with Failure _ -> [] 
 	 in
          (free_try
-	  (search_gen decomp n db_list (add_hint_list hintl local_db) [d])
+	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
 	  g'))
   in
   let rec_tacs = 
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index dd40c5cc..203bc9e3 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -57,8 +57,7 @@ let explore_tree pfs =
   and explain_prim = function
     | Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
     | Intro identifier -> "Intro"
-    | Intro_replacing identifier -> "Intro_replacing"
-    | Cut (bool, identifier, types) -> "Cut"
+    | Cut (bool, _, identifier, types) -> "Cut"
     | FixRule (identifier, int, l) -> "FixRule"
     | Cofix (identifier, l) -> "Cofix"
     | Convert_concl (types, cast_kind) -> "Convert_concl"
@@ -269,7 +268,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
 	     igtal
 	     acc)
     | TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet"
-    | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
+    | TacMatchGoal (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
     | TacFun tacfa -> depends_of_tac_fun_ast tacfa acc
     | TacArg tacarg -> depends_of_tac_arg tacarg acc
   and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with
@@ -281,7 +280,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacExact          c
     | TacExactNoCheck   c
     | TacVmCastNoCheck  c  -> depends_of_'constr c acc
-    | TacApply (_, _, cb) -> depends_of_'constr_with_bindings cb acc
+    | TacApply (_, _, [cb]) -> depends_of_'constr_with_bindings cb acc
+    | TacApply (_, _, _) -> failwith "TODO"
     | TacElim (_, cwb, cwbo) ->
 	depends_of_'constr_with_bindings cwb
 	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
@@ -302,14 +302,13 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacLetTac (_,c,_,_) -> depends_of_'constr c acc
 
     (* Derived basic tactics *)
-    | TacSimpleInduction _
-    | TacSimpleDestruct  _
+    | TacSimpleInductionDestruct _
     | TacDoubleInduction _ -> acc
-    | TacNewInduction (_, cwbial, cwbo, _, _)
-    | TacNewDestruct (_, cwbial, cwbo, _, _) ->
+    | TacInductionDestruct (_, _, [cwbial, cwbo, _, _]) ->
 	list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings)
 	  cwbial
 	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
+    | TacInductionDestruct (_, _, _) -> failwith "TODO"
     | TacDecomposeAnd c
     | TacDecomposeOr  c -> depends_of_'constr c acc
     | TacDecompose (il, c) -> depends_of_'constr c (list_union_map depends_of_'ind il acc)
@@ -410,8 +409,7 @@ let depends_of_compound_rule cr acc = match cr with
 and depends_of_prim_rule pr acc = match pr with
   | Refine c                     -> depends_of_constr c acc
   | Intro id                     -> acc
-  | Intro_replacing id           -> acc
-  | Cut (_, _, t)                -> depends_of_constr t acc (* TODO: check what 2nd argument contains *)
+  | Cut (_, _, _, t)             -> depends_of_constr t acc (* TODO: check what 3nd argument contains *)
   | FixRule (_, _, l)            -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
   | Cofix (_, l)                 -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
   | Convert_concl (t, _)         -> depends_of_constr t acc
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 06b957d9..65eadf13 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -48,7 +48,7 @@ type pbp_atom =
   | PbpTryClear of identifier list
   | PbpGeneralize of identifier * identifier list
   | PbpLApply of identifier (* = CutAndApply *)
-  | PbpIntros of intro_pattern_expr list
+  | PbpIntros of intro_pattern_expr located list
   | PbpSplit
   (* Existential *)
   | PbpExists of identifier
@@ -93,7 +93,7 @@ type pbp_rule = (identifier list *
                     pbp_sequence option;;
 
 
-let make_named_intro id = PbpIntros [IntroIdentifier id];;
+let make_named_intro id = PbpIntros [zz,IntroIdentifier id];;
 
 let make_clears str_list = PbpThen [PbpTryClear str_list]
 
@@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function
   | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
-  | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings)))
+  | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings]))
   | PbpElim (hyp_name, names) ->
       let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
       TacAtom
@@ -255,9 +255,9 @@ fun avoid c path -> match kind_of_term c, path with
 	or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in
       let patt_list = 
 	if a = 1 then
-	  [cont_patt; IntroIdentifier id2]
+	  [zz,cont_patt; zz,IntroIdentifier id2]
 	else
-	  [IntroIdentifier id2; cont_patt] in
+	  [zz,IntroIdentifier id2; zz,cont_patt] in
       	(IntroOrAndPattern[patt_list], avoid_names, id, c, path, rank, 
 	 total_branches)
   | (App(oper, [|c1; c2|]), 2::3::path)
@@ -268,7 +268,7 @@ fun avoid c path -> match kind_of_term c, path with
 	     let id1 = next_global_ident x avoid in
 	     let cont_patt, avoid_names, id, c, path, rank, total_branches =
 	       or_and_tree_to_intro_pattern (id1::avoid) body path in
-	     (IntroOrAndPattern[[IntroIdentifier id1; cont_patt]],
+	     (IntroOrAndPattern[[zz,IntroIdentifier id1; zz,cont_patt]],
 	      avoid_names, id, c, path, rank, total_branches)
 	 | _ -> assert false)
   | (App(oper, [|c1; c2|]), 2::a::path)
@@ -282,9 +282,9 @@ fun avoid c path -> match kind_of_term c, path with
       let new_rank = if a = 1 then rank else rank+1 in
       let patt_list =
 	if a = 1 then
-	  [[cont_patt];[IntroIdentifier id2]]
+	  [[zz,cont_patt];[zz,IntroIdentifier id2]]
 	else
-	  [[IntroIdentifier id2];[cont_patt]] in
+	  [[zz,IntroIdentifier id2];[zz,cont_patt]] in
 	(IntroOrAndPattern patt_list, 
 	 avoid_names, id, c, path, new_rank, total_branches+1)
   | (_, path) -> let id = next_global_ident hyp_radix avoid in
@@ -305,13 +305,13 @@ let (imply_intro3: pbp_rule) = function
       let intro_patt, avoid_names, id, c, p, rank, total_branches =
 	or_and_tree_to_intro_pattern avoid prem path in
 	if total_branches = 1 then
-	  Some(chain_tactics [PbpIntros [intro_patt]]
+	  Some(chain_tactics [PbpIntros [zz,intro_patt]]
 		 (f avoid_names clear_names clear_flag (Some id)
 		    (kind_of_term c) path))
 	else
 	  Some
 	    (PbpThens
-	       ([PbpIntros [intro_patt]],
+	       ([PbpIntros [zz,intro_patt]],
 	    	auxiliary_goals clear_names clear_flag id
 		  (rank - 1)
 		  ((f avoid_names clear_names clear_flag (Some id)
@@ -667,7 +667,7 @@ let rec cleanup_clears str_list = function
 
 let rec optim3_aux str_list = function
     (PbpGeneralize (h,l1))::
-    (PbpIntros [IntroIdentifier s])::(PbpGeneralize (h',l2))::others
+    (PbpIntros [zz,IntroIdentifier s])::(PbpGeneralize (h',l2))::others
       when s=h' ->
       optim3_aux (s::str_list) (PbpGeneralize (h,l1@l2)::others)
   | (PbpTryClear names)::other ->
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 953fb5e7..4b9c1332 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1197,12 +1197,12 @@ let rec natural_ntree ig ntree =
 	  | TacAssumption -> natural_trivial ig lh g gs ltree
 	  | TacClear _ -> natural_clear ig lh g gs ltree
 (* Besoin de l'argument de la tactique *)
-	  | TacSimpleInduction (NamedHyp id) -> 
+	  | TacSimpleInductionDestruct (true,NamedHyp id) -> 
               natural_induction ig lh g gs ge id ltree false
 	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
               natural_induction ig lh g gs ge id ltree true
-	  | TacApply (_,false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree
+	  | TacApply (_,false,[c,_]) -> natural_apply ig lh g gs (snd c) ltree
 	  | TacExact c -> natural_exact ig lh g gs (snd c) ltree
 	  | TacCut c -> natural_cut ig lh g gs (snd c) ltree
 	  | TacExtend (_,"CutIntro",[a]) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7d1f57fe..da4908e5 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -615,8 +615,7 @@ let get_flag r =
   (* Rem: EVAR flag obsolète *)
   conv_flags, red_ids
 
-let rec xlate_intro_pattern =
- function
+let rec xlate_intro_pattern (loc,pat) = match pat with
   | IntroOrAndPattern [] -> assert false
   | IntroOrAndPattern (fp::ll) ->
       CT_disj_pattern
@@ -684,8 +683,8 @@ let xlate_one_unfold_block = function
 ;;
 
 let xlate_with_names = function
-    IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
-  | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+    None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
+  | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
 
 let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level
 
@@ -829,11 +828,11 @@ and xlate_tactic =
                          | [] -> assert false
                          | fst::others ->
                              CT_match_tac_rules(fst, others))
-   | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
-   | TacMatchContext (false,false,rule1::rules) ->
+   | TacMatchGoal (_,_,[]) | TacMatchGoal (true,_,_) -> failwith ""
+   | TacMatchGoal (false,false,rule1::rules) ->
          CT_match_context(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
-   | TacMatchContext (false,true,rule1::rules) ->
+   | TacMatchGoal (false,true,rule1::rules) ->
          CT_match_context_reverse(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
    | TacLetIn (false, l, t) ->
@@ -926,23 +925,26 @@ and xlate_tac =
     | TacExtend (_,"contradiction",[]) -> CT_contradiction
     | TacDoubleInduction (n1, n2) ->
 	CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2)
-    | TacExtend (_,"discriminate", [idopt]) ->
+    | TacExtend (_,"discriminate", []) ->
+     CT_discriminate_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
+    | TacExtend (_,"discriminate", [id]) ->
      CT_discriminate_eq
          (xlate_quantified_hypothesis_opt
-	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
-    | TacExtend (_,"simplify_eq", [idopt]) ->
-	let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in
-	let idopt2 = match idopt1 with
-	    None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT
-		(CT_coerce_NONE_to_ID_OPT CT_none)
-	  | Some v ->
-	      CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
-	      	(xlate_quantified_hypothesis v) in
-	  CT_simplify_eq idopt2
-    | TacExtend (_,"injection", [idopt]) ->
+	    (Some (out_gen rawwit_quant_hyp id)))
+    | TacExtend (_,"simplify_eq", []) ->
+	  CT_simplify_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT
+		(CT_coerce_NONE_to_ID_OPT CT_none))
+    | TacExtend (_,"simplify_eq", [id]) ->
+	let id1 = out_gen rawwit_quant_hyp id in
+	let id2 = CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
+	      	(xlate_quantified_hypothesis id1) in
+	  CT_simplify_eq id2
+    | TacExtend (_,"injection", []) ->
+     CT_injection_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
+    | TacExtend (_,"injection", [id]) ->
      CT_injection_eq
          (xlate_quantified_hypothesis_opt
-	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
+	    (Some (out_gen rawwit_quant_hyp id)))
     | TacExtend (_,"injection_as", [idopt;ipat]) ->
 	xlate_error "TODO: injection as"
     | TacFix (idopt, n) ->
@@ -967,19 +969,22 @@ and xlate_tac =
 	CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
     | TacIntrosUntil (AnonHyp n) -> 
 	CT_intros_until (CT_coerce_INT_to_ID_OR_INT (CT_int n))
-    | TacIntroMove (Some id1, Some (_,id2)) ->
-     CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_ident id2)
-    | TacIntroMove (None, Some (_,id2)) ->
-	CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_ident id2)
-    | TacMove (true, id1, id2) ->
+    | TacIntroMove (Some id1, MoveAfter id2) ->
+     CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_hyp id2)
+    | TacIntroMove (None, MoveAfter id2) ->
+	CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_hyp id2)
+    | TacMove (true, id1, MoveAfter id2) ->
 	CT_move_after(xlate_hyp id1, xlate_hyp id2)
     | TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal"
+    | TacMove _ -> xlate_error "TODO: move before, at top, at bottom"
     | TacIntroPattern patt_list ->
 	CT_intros
 	  (CT_intro_patt_list (List.map xlate_intro_pattern patt_list))
-    | TacIntroMove (Some id, None) ->
+    | TacIntroMove (Some id, MoveToEnd true) ->
      CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
-    | TacIntroMove (None, None) ->  CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
+    | TacIntroMove (None, MoveToEnd true) ->
+	CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
+    | TacIntroMove _ -> xlate_error "TODO"
     | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl)
     | TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
     | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl)
@@ -1150,11 +1155,12 @@ and xlate_tac =
 	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
-    | TacApply (true,false,(c,bindl)) ->
+    | TacApply (true,false,[c,bindl]) ->
      CT_apply (xlate_formula c, xlate_bindings bindl)
-    | TacApply (true,true,(c,bindl)) ->
+    | TacApply (true,true,[c,bindl]) ->
      CT_eapply (xlate_formula c, xlate_bindings bindl)
-    | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply"
+    | TacApply (_,_,_) ->
+	xlate_error "TODO: simple (e)apply and iterated apply"
     | TacConstructor (false,n_or_meta, bindl) ->
 	let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
 	in CT_constructor (CT_int n, xlate_bindings bindl)
@@ -1178,10 +1184,12 @@ and xlate_tac =
     | TacCase (false,(c1,sl)) ->
      CT_casetac (xlate_formula c1, xlate_bindings sl)
     | TacElim (true,_,_) | TacCase (true,_)
-    | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) ->
+    | TacInductionDestruct (_,true,_) ->
 	xlate_error "TODO: eelim, ecase, edestruct, einduction"
-    | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
-    | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
+    | TacSimpleInductionDestruct (true,h) ->
+	CT_induction (xlate_quantified_hypothesis h)
+    | TacSimpleInductionDestruct (false,h) ->
+	CT_destruct (xlate_quantified_hypothesis h)
     | TacCut c -> CT_cut (xlate_formula c)
     | TacLApply c -> CT_use (xlate_formula c)
     | TacDecompose ([],c) ->
@@ -1222,19 +1230,16 @@ and xlate_tac =
 	CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
     | TacDAuto (a, b, _) ->
 	xlate_error "TODO: dauto using"
-    | TacNewDestruct(false,a,b,c,None) ->
+    | TacInductionDestruct(true,false,[a,b,(None,c),None]) ->
 	CT_new_destruct
 	  (List.map  xlate_int_or_constr a, xlate_using b, 
 	   xlate_with_names c)
-    | TacNewInduction(false,a,b,c,None) ->
+    | TacInductionDestruct(false,false,[a,b,(None,c),None]) ->
 	CT_new_induction
 	  (List.map xlate_int_or_constr a, xlate_using b,
 	   xlate_with_names c)
-    | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in"
-    | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in"
-    (*| TacInstantiate (a, b, cl) -> 
-        CT_instantiate(CT_int a, xlate_formula b,
-		       assert false) *)
+    | TacInductionDestruct(_,false,_) -> 
+	xlate_error "TODO: clause 'in' and full 'as' of destruct/induction"
     | TacLetTac (na, c, cl, true) when cl = nowhere -> 
         CT_pose(xlate_id_opt_aux na, xlate_formula c)
     | TacLetTac (na, c, cl, true) ->
@@ -1243,13 +1248,13 @@ and xlate_tac =
 		     but the structures are different *)
 		  xlate_clause cl)
     | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
-    | TacAssert (None, IntroIdentifier id, c) -> 
+    | TacAssert (None, (_,IntroIdentifier id), c) -> 
         CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (None, IntroAnonymous, c) -> 
+    | TacAssert (None, (_,IntroAnonymous), c) -> 
         CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
-    | TacAssert (Some (TacId []), IntroIdentifier id, c) -> 
+    | TacAssert (Some (TacId []), (_,IntroIdentifier id), c) -> 
         CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (Some (TacId []), IntroAnonymous, c) -> 
+    | TacAssert (Some (TacId []), (_,IntroAnonymous), c) -> 
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"