Évolutions diverses et variées.

- Correction divers messages d'erreur
  - lorsque rien à réécrire dans une hyp,
  - lorsqu'une variable ltac n'est pas liée,
  - correction anomalie en présence de ?id dans le "as" de induction,
  - correction mauvais env dans message d'erreur de unify_0.

- Diverses extensions et améliorations
  - "specialize" :
    - extension au cas (fun x1 ... xn => H u1 ... un),
    - renommage au même endroit.
  - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
  - "induction"
    - intro des IH toujours au sommet même si induction sur var quantifiée,
    - ajout d'un hack pour la reconnaissance de schémas inductifs comme
      N_ind_double mais il reste du boulot pour reconnaître (et/ou
      réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
      dans l'ordre standard,
    - vérification de longueur et éventuelle complétion des
      intropatterns dans le cas de sous-patterns destructifs dans induction
      (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
       le n dans le contexte),
    - localisation des erreurs d'intropattern,
    - ajout d'un pattern optionnel après "as" pour forcer une égalité et la
      nommer (*).
  - "apply" accepte plusieurs arguments séparés par des virgules (*).
  - Plus de robustesse pour clear en présence d'evars.
  - Amélioration affichage TacFun dans Print Ltac.
  - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
    (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
  - Fusion VTactic/VFun dans l'espoir.
  - Mise en place d'un système de trace de la pile des appels Ltac (tout en
    préservant certains aspects de la récursivité terminale - cf bug #468).

- Tactiques primitives

  - ajout de "move before" dans les tactiques primitives et ajout des
    syntaxes move before et move dependent au niveau utilisateur (*),
  - internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
  - suppression de Intro_replacing et du code sous-traitant

- Nettoyage
  - Suppression cible et fichiers minicoq non portés depuis longtemps.

(*) Extensions de syntaxe qu'il pourrait être opportun de discuter



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

4 files changed, 51 insertions, 51 deletions

diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index dd40c5cc36..bf1cf5e7b2 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"
@@ -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 06b957d9c2..65eadf13db 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 953fb5e790..4b9c1332a4 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 2e4ff80bb0..716f6da3b7 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
@@ -625,7 +624,7 @@ let rec xlate_intro_pattern =
 	   (fun l ->
 	      CT_intro_patt_list(List.map xlate_intro_pattern l))
 	   ll)
-  | IntroWildcard _ -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
+  | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
   | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
   | IntroFresh _ -> xlate_error "TODO: IntroFresh"
@@ -686,8 +685,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
 
@@ -972,19 +971,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)
@@ -1155,11 +1157,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)
@@ -1183,10 +1186,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) ->
@@ -1227,19 +1232,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) ->
@@ -1248,13 +1250,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'"