É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

6 files changed, 66 insertions, 48 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f0c020908d..63a56f0d13 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -374,42 +374,41 @@ let restrict_upon_filter evd evi evk p args =
   else
     evd,evk,args
 
-exception Dependency_error of identifier
+let collect_vars c =
+  let rec collrec acc c =
+    match kind_of_term c with
+    | Var id -> list_add_set id acc
+    | _      -> fold_constr collrec acc c
+  in
+  collrec [] c
 
-module EvkOrd = 
-struct
-  type t = Term.existential_key
-  let compare = Pervasives.compare
-end
+type clear_dependency_error =
+| OccurHypInSimpleClause of identifier option
+| EvarTypingBreak of existential
 
-module EvkSet = Set.Make(EvkOrd)
+exception ClearDependencyError of identifier * clear_dependency_error
 
-let rec check_and_clear_in_constr evdref c ids hist =
+let rec check_and_clear_in_constr evdref err ids c =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
-     evars *)
+     evars) *)
   let check id' = 
     if List.mem id' ids then
-      raise (Dependency_error id')
+      raise (ClearDependencyError (id',err))
   in 
     match kind_of_term c with
-      | ( Rel _ | Meta _ | Sort _ ) -> c
-
-      | ( Const _ | Ind _ | Construct _ ) -> 
-	  let vars = Environ.vars_of_global (Global.env()) c in
-	    List.iter check vars; c
+      | Var id' ->
+	  check id'; c
 
-      | Var id' ->  
-	  check id'; mkVar id'
+      | ( Const _ | Ind _ | Construct _ ) ->
+          let vars = Environ.vars_of_global (Global.env()) c in
+            List.iter check vars; c
 
       | Evar (evk,l as ev) -> 
 	  if Evd.is_defined_evar !evdref ev then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = nf_evar (evars_of !evdref) c in 
-	      (check_and_clear_in_constr evdref nc ids hist)
-	  else if EvkSet.mem evk hist then
-	    (* Loop detection => do nothing *)
-	    c
+	    let nc = whd_evar (evars_of !evdref) c in 
+	      (check_and_clear_in_constr evdref err ids nc)
 	  else 
 	    (* We check for dependencies to elements of ids in the
 	       evar_info corresponding to e and in the instance of
@@ -418,16 +417,32 @@ let rec check_and_clear_in_constr evdref c ids hist =
 	       removed *)
 	    let evi = Evd.find (evars_of !evdref) evk in
 	    let ctxt = Evd.evar_filtered_context evi in
-	    let (nhyps,nargs,rids) = 
+	    let (nhyps,nargs,rids) =
 	      List.fold_right2 
 		(fun (rid,ob,c as h) a (hy,ar,ri) ->
-		  match kind_of_term a with
-		    | Var id -> if List.mem id ids then (hy,ar,id::ri) else (h::hy,a::ar,ri)
-		    | _ -> (h::hy,a::ar,ri)
-		) 	      
+		  (* Check if some id to clear occurs in the instance
+		     a of rid in ev and remember the dependency *)
+		  match 
+		    List.filter (fun id -> List.mem id ids) (collect_vars a)
+		  with
+		  | id :: _ -> (hy,ar,(rid,id)::ri)
+		  | _ ->
+		  (* Check if some rid to clear in the context of ev
+		     has dependencies in another hyp of the context of ev
+		     and transitively remember the dependency *)
+		  match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
+		  | rid' :: _ -> (hy,ar,(rid,List.assoc rid ri)::ri)
+		  | _ ->
+		  (* No dependency at all, we can keep this ev's context hyp *)
+		      (h::hy,a::ar,ri))
 		ctxt (Array.to_list l) ([],[],[]) in
-	    (* nconcl must be computed ids (non instanciated hyps) *)
-	    let nconcl = check_and_clear_in_constr evdref (evar_concl evi) rids (EvkSet.add evk hist) in
+	    (* Check if some rid to clear in the context of ev has dependencies
+	       in the type of ev and adjust the source of the dependency *)
+	    let nconcl =
+	      try check_and_clear_in_constr evdref (EvarTypingBreak ev)
+		    (List.map fst rids) (evar_concl evi) 
+	      with ClearDependencyError (rid,err) -> 
+		raise (ClearDependencyError (List.assoc rid rids,err)) in
 
 	    let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
 	    let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
@@ -435,25 +450,19 @@ let rec check_and_clear_in_constr evdref c ids hist =
 	      let (evk',_) = destEvar ev' in
 		mkEvar(evk', Array.of_list nargs)
 
-      | _ -> map_constr (fun c -> check_and_clear_in_constr evdref c ids hist) c
-
-exception OccurHypInSimpleClause of identifier * identifier option
+      | _ -> map_constr (check_and_clear_in_constr evdref err ids) c
 
 let clear_hyps_in_evi evdref hyps concl ids =
-  (* clear_evar_hyps erases hypotheses ids in hyps, checking if some
+  (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occuring in evi *)
-  let nconcl = try check_and_clear_in_constr evdref concl ids EvkSet.empty
-    with Dependency_error id' -> raise (OccurHypInSimpleClause (id',None)) in
-  let (nhyps,_) = 
-    let check_context (id,ob,c) = 
-      try
-	(id,
-	(match ob with 
-	    None -> None
-	  | Some b -> Some (check_and_clear_in_constr evdref b ids EvkSet.empty)),
-	check_and_clear_in_constr evdref c ids EvkSet.empty)
-      with Dependency_error id' -> raise (OccurHypInSimpleClause (id',Some id))
+  let nconcl =
+    check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
+  let nhyps = 
+    let check_context (id,ob,c) =
+      let err = OccurHypInSimpleClause (Some id) in
+      (id, Option.map (check_and_clear_in_constr evdref err ids) ob,
+	check_and_clear_in_constr evdref err ids c)
     in
     let check_value vk =
       match !vk with
@@ -470,6 +479,7 @@ let clear_hyps_in_evi evdref hyps concl ids =
   in
   (nhyps,nconcl)
 
+
 (* Expand rels and vars that are bound to other rels or vars so that 
    dependencies in variables are canonically associated to the most ancient
    variable in its family of aliased variables *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index c48c979109..d11e1fa2a5 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -176,7 +176,11 @@ val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
 (* Removing hyps in evars'context;                                   *)
 (* raise OccurHypInSimpleClause if the removal breaks dependencies   *)
 
-exception OccurHypInSimpleClause of identifier * identifier option
+type clear_dependency_error =
+| OccurHypInSimpleClause of identifier option
+| EvarTypingBreak of existential
+
+exception ClearDependencyError of identifier * clear_dependency_error
 
 val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types ->
   identifier list -> named_context_val * types
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ecc63ce940..270dac01a9 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -523,6 +523,8 @@ let pr_sort_constraints (_,sm) = pr_sort_cstrs sm
 
 let meta_list evd = metamap_to_list evd.metas
 
+let find_meta evd mv = Metamap.find mv evd.metas
+
 let undefined_metas evd =
   List.sort Pervasives.compare (map_succeed (function
     | (n,Clval(_,_,typ)) -> failwith ""
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 6aa26aa432..cb74290022 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -100,6 +100,8 @@ val sig_sig : 'a sigma -> evar_map
 (*********************************************************************)
 (* Meta map *)
 
+module Metamap : Map.S with type key = metavariable
+
 module Metaset : Set.S with type elt = metavariable
 
 val meta_exists : (metavariable -> bool) -> Metaset.t -> bool
@@ -197,6 +199,7 @@ val extract_all_conv_pbs : evar_defs -> evar_defs * evar_constraint list
 
 
 (* Metas *)
+val find_meta : evar_defs -> metavariable -> clbinding
 val meta_list : evar_defs -> (metavariable * clbinding) list
 val meta_defined : evar_defs -> metavariable -> bool
 (* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 6c029a161f..422ee57d47 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -111,7 +111,6 @@ val whd_betadeltaiota_nolet_stack :  contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
 val whd_betalet_stack : local_stack_reduction_function
 
-val whd_state : local_state_reduction_function
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
 val whd_betaiotazeta_state : local_state_reduction_function
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a29dca57c9..dbf7d6469e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -239,9 +239,9 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
       | Some c ->
 	  unirec_rec curenv pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
       | None ->
-      error_cannot_unify env sigma (cM,cN)
+      error_cannot_unify curenv sigma (cM,cN)
     else
-      error_cannot_unify env sigma (cM,cN)
+      error_cannot_unify curenv sigma (cM,cN)
 
   in
     if (not(occur_meta m)) &&