É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

5 files changed, 14 insertions, 24 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index d7bcde69cb..bd335d3049 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -136,7 +136,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
   fun g -> 
     let prov_id = pf_get_new_id hyp_id g in 
     tclTHENS
-      ((* observe_tac msg *) (forward (Some  (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t))
+      ((* observe_tac msg *) (forward (Some  (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t))
       [tclTHENLIST 
       [	
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		     in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
-		       (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x)
+		       (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x)
 		       [
 			 (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
 (* 			observe_tac "prove rec hyp" *)
@@ -571,7 +571,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
 	fun g -> 
 	  let prov_hid = pf_get_new_id hid g in
 	  tclTHENLIST[
-	    forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+	    forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
 	    thin [hid];
 	    h_rename [prov_hid,hid]
 	  ] g
@@ -1497,7 +1497,7 @@ let prove_principle_for_gen
 	    (tclTHEN
 	       (forward 
 		  (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))
-		  (Genarg.IntroIdentifier wf_thm_id)
+		  (dummy_loc,Genarg.IntroIdentifier wf_thm_id)
 		  (mkApp (delayed_force well_founded,[|input_type;relation|])))
 	       (
 		 (* observe_tac  *)
@@ -1561,7 +1561,7 @@ let prove_principle_for_gen
 	);
       (* observe_tac "" *) (forward
 	 (Some (prove_rec_arg_acc))
-	 (Genarg.IntroIdentifier acc_rec_arg_id)
+	 (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id)
  	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
       );
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index dae76f2dd9..d435f51351 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -90,11 +90,6 @@ END
 TACTIC EXTEND newfunind
    ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> 
      [ 
-       let pat = 
-	 match pat with 
-	   | None -> IntroAnonymous
-	   | Some pat -> pat
-       in
        let c = match cl with 
 	 | [] -> assert false
 	 | [c] -> c 
@@ -106,11 +101,6 @@ END
 TACTIC EXTEND snewfunind
    ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> 
      [ 
-       let pat = 
-	 match pat with 
-	   | None -> IntroAnonymous
-	   | Some pat -> pat
-       in
        let c = match cl with 
 	 | [] -> assert false
 	 | [c] -> c 
@@ -319,7 +309,7 @@ let poseq_unsafe idunsafe cstr gl =
   tclTHEN
     (Tactics.letin_tac None (Name idunsafe) cstr allClauses)
     (tclTHENFIRST 
-      (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) 
+      (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) 
       Tactics.reflexivity)
     gl
   
@@ -396,7 +386,7 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l
 	      fun gl -> 
 		  (functional_induction 
 		    true (applist (info.fname, List.rev !list_constr_largs)) 
-		    None IntroAnonymous) gl)) 
+		    None None) gl)) 
 	  nexttac)) ordered_info_list in
   (* we try each (f t u v) until one does not fail *)
   (* TODO: try also to mix functional schemes *)
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index a6cbb3211b..79ef009729 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -120,7 +120,7 @@ let functional_induction with_clean c princl pat =
 	 princ_infos
 	 args_as_induction_constr
 	 princ'
-	 pat
+	 (None,pat)
          None)
       subst_and_reduce
       g
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 63d44916be..f62d70ab9a 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -280,13 +280,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       List.map
 	(fun (_,_,br_type) ->
 	   List.map
-	     (fun id -> Genarg.IntroIdentifier id)
+	     (fun id -> dummy_loc, Genarg.IntroIdentifier id)
 	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
     in
     (* before building the full intro pattern for the principle *)
-    let pat = Genarg.IntroOrAndPattern intro_pats in
+    let pat = Some (dummy_loc,Genarg.IntroOrAndPattern intro_pats) in
     let eq_ind = Coqlib.build_coq_eq () in
     let eq_construct = mkConstruct((destInd eq_ind),1) in
     (* The next to referencies will be used to find out which constructor to apply in each branch *)
@@ -297,7 +297,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       (* We get the identifiers of this branch *)
       let this_branche_ids =
 	List.fold_right
-	  (fun pat acc ->
+	  (fun (_,pat) acc ->
 	     match pat with
 	       | Genarg.IntroIdentifier id -> Idset.add id acc
 	       | _ -> anomaly "Not an identifier"
@@ -447,7 +447,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       [ observe_tac "intro args_names" (tclMAP h_intro args_names);
 	observe_tac "principle" (forward
 	  (Some (h_exact f_principle))
-	  (Genarg.IntroIdentifier principle_id)
+	  (dummy_loc,Genarg.IntroIdentifier principle_id)
 	  princ_type);
 	tclTHEN_i
 	  (observe_tac "functional_induction" (
@@ -948,7 +948,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	    h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
 	    thin [hid];
 	    h_intro hid;
-	    Inv.inv FullInversion Genarg.IntroAnonymous (Rawterm.NamedHyp hid);
+	    Inv.inv FullInversion None (Rawterm.NamedHyp hid);
 	    (fun g ->
 	       let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in 
 	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 13989f03bc..6227f92d72 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -1157,7 +1157,7 @@ let rec introduce_all_values_eq cont_tac functional termine
       [] ->
        let heq2 = next_global_ident_away true heq_id ids in
 	tclTHENLIST
-	  [forward None (IntroIdentifier heq2)
+	  [forward None (dummy_loc,IntroIdentifier heq2)
              (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
            simpl_iter (onHyp heq2);
            unfold_in_hyp [((true,[1]), evaluable_of_global_reference