Update CHANGES, add documentation for new commands/tactics and do a bit

of cleanup in tactics/


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

11 files changed, 90 insertions, 156 deletions

diff --git a/CHANGES b/CHANGES
index f06cbb2e1..b36dbb55c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -21,10 +21,13 @@ Tactics
   (i.e. library Classical_Prop or Classical) is loaded.
 - New "Hint Resolve ->" (or "<-") for declaring iff's as oriented
   hints (wish #2104).
+- "Hint Rewrite" now checks that the lemma looks like an equation.
 - New introduction patterns "*" for introducing the next block of dependent 
   variables and "**" for introducing all quantified variables and hypotheses.
 - Pattern Unification for existential variables activated in tactics and 
   new option "Unset Tactic Evars Pattern Unification" to deactivate it.
+- Resolution of Canonical Structures is now part of the tactic's unification
+  algorithm.
 - New tactic "etransitivity".
 - Support of JMeq for "injection" and "discriminate".
 - Tactic "subst" now supports heterogeneous equality and equality
@@ -52,6 +55,16 @@ Tactics
   sequences of "apply in") now leave the side conditions of the lemmas
   uniformly after the main goal (possible source of rare incompatibilities).
 - In "simpl c" and "change c with d", c can be a pattern.
+- Tactic "revert" now preserves let-in's making it the exact inverse of
+  "intro".
+- Renamed "Morphism" into "Proper" and "respect" into "proper_prf"
+  (possible source of incompatibility).
+- "Require Import Setoid" does not export all of "Morphims" and
+  "RelationClasses" anymore (possible source of incompatibility, fixed
+  by importing "Morphisms" too).
+- New tactic variants "rewrite* by" and "autorewrite*" that rewrite
+  respectively the first and all matches whose side-conditions are
+  solved.
 
 Tactic Language
 
@@ -94,6 +107,13 @@ Vernacular commands
 - Include Type is now deprecated since Include now accept both modules and
   module types.
 - Declare ML Module supports Local option.
+- New command "(Global?) Generalizable [All|No] Variable(s)? ident(s)?" to
+  declare which identifiers are generalizable in `{} and `() binders.
+- New command "Print Opaque Dependencies" to display opaque constants in
+  addition to all variables, parameters or axioms a theorem or
+  definition relies on.
+- New option [Set Automatic Introduction] to automatically introduce
+  variables before the colon at the start of interactive proofs.
 - New command "Declare Reduction <id> := <conv_expr>", allowing to write
   later "Eval <id> in ...". This command accepts a Local variant.
 
@@ -116,7 +136,7 @@ Coqdoc
 - The "--lib-name <string>" flag prints "<string> Foo" instead of
   "Library Foo" where library titles are called for.  The
   "--no-lib-name" flag eliminates the extra title.
-- New option "--parse-comments" to allow parsing of regular ("(* *)") 
+- New option "--parse-comments" to allow parsing of regular "(* *)"
   comments.
 - New option "--plain-comments" to disable interpretation inside comments.
 - New option "--interpolate" to try and typeset identifiers in Coq escapings
@@ -153,6 +173,29 @@ Language
   to high-order structures (cf. libraries Numbers and Structures to see examples).
   Interactive proofs are now authorized in module type.
 
+Program
+
+- Streamlined definitions using well-founded recursion and measures so
+  that they can work on any number subset of the arguments directly
+  (uses currying).
+- Try to automatically clear structural fixpoint prototypes in
+  obligations to avoid issues of opacity.
+- Use return type clause inference as in the standard typing algorithm.
+- Support [Local Obligation Tactic] and [Next Obligation with tactic].
+- Use [Show Obligation Tactic] to print the current default tactic.
+- [fst] and [snd] have maximal implicits in Program now (possible source
+  of incompatibility)
+
+Typeclasses
+
+- Use [Existing Class foo] to declare foo as a class a posteriori.
+  [foo] can be an inductive type or a constant definition, no
+  projections are defined.
+- Various bug fixes and improvements: support for defined fields, 
+  anonymous instances, declarations giving terms, better handling of
+  sections, contexts.
+
+
 Changes from V8.1 to V8.2
 =========================
 
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 9d88fa077..defcb4596 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -203,10 +203,14 @@ obligations (e.g. when defining mutually recursive blocks). The optional
 tactic is replaced by the default one if not specified.
 
 \begin{itemize}
-\item {\tt Obligation Tactic := \tacexpr}\comindex{Obligation Tactic}
+\item {\tt [Local|Global] Obligation Tactic := \tacexpr}\comindex{Obligation Tactic}
   Sets the default obligation
   solving tactic applied to all obligations automatically, whether to
   solve them or when starting to prove one, e.g. using {\tt Next}.
+  Local makes the setting last only for the current module. Inside
+  sections, local is the default.
+\item {\tt Show Obligation Tactic}\comindex{Show Obligation Tactic}
+  Displays the current default tactic.
 \item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining
   obligations.
 \item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of
@@ -270,5 +274,5 @@ Program Fixpoint f (x : A | P) { measure size } :=
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
+%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage2 doc/refman/Reference-Manual.pdf"
 %%% End: 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4d5cdbb81..ab8cfd07a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -795,14 +795,22 @@ where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by
   This generalizes {\term} but also {\em all} hypotheses which depend
   on {\term}. It clears the generalized hypotheses.
 
-\item {\tt revert \ident$_1$ \dots\ \ident$_n$}\tacindex{revert}
- 
-  This is equivalent to a {\tt generalize} followed by a {\tt clear}
-  on the given hypotheses. This tactic can be seen as reciprocal to 
-  {\tt intros}. 
-
 \end{Variants}
 
+
+\subsection{\tt revert  \ident$_1$ \dots\ \ident$_n$
+\tacindex{revert}
+\label{revert}}
+
+This applies to any goal with variables \ident$_1$ \dots\ \ident$_n$.
+It moves the hypotheses (possibly defined) to the goal, if this respects
+dependencies. This tactic is the inverse of {\tt intro}. 
+
+\begin{ErrMsgs}
+\item \errindexbis{{\ident} is used in the hypothesis {\ident'}}{is
+    used in the hypothesis} 
+\end{ErrMsgs}
+
 \subsection{\tt change \term
 \tacindex{change}
 \label{change}}
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 45e384a41..d805b3ac7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -848,6 +848,10 @@ let hintmap_of hdc concl =
       if occur_existential concl then Hint_db.map_all hdc
       else Hint_db.map_auto (hdc,concl)
 
+let exists_evaluable_reference env = function
+  | EvalConstRef _ -> true
+  | EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
+
 let rec trivial_fail_db mod_delta db_list local_db gl =
   let intro_tac =
     tclTHEN intro
@@ -908,7 +912,10 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
       tclTHEN
         (unify_resolve_gen flags (term,cl))
         (trivial_fail_db (flags <> None) db_list local_db)
-  | Unfold_nth c -> tclPROGRESS (unfold_in_concl [all_occurrences,c])
+  | Unfold_nth c -> (fun gl ->
+      if exists_evaluable_reference (pf_env gl) c then
+	tclPROGRESS (unfold_in_concl [all_occurrences,c]) gl
+      else tclFAIL 0 (str"Unbound reference") gl)
   | Extern tacast -> conclPattern concl p tacast
 
 and trivial_resolve mod_delta db_list local_db cl =
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 45e688456..5e9bb653c 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -722,7 +722,8 @@ END
 
 let _ = Classes.refine_ref := Refine.refine
 
-(** Take the head of the arity af constr. *)
+(** Take the head of the arity of a constr.
+    Used in the partial application tactic. *)
 
 let rec head_of_constr t =
   let t = strip_outer_cast(collapse_appl t) in
@@ -739,94 +740,6 @@ TACTIC EXTEND head_of_constr
   ]
 END
 
-(** A tactic to help reification based on classes:
-    factorize all variables of a particular type into a varmap. *)
-
-let gen_constant dir s = Coqlib.gen_constant "typeclass_tactics" dir s
-let coq_List_nth = lazy (gen_constant ["Lists"; "List"] "nth")
-let coq_List_cons = lazy (gen_constant ["Lists"; "List"] "cons")
-let coq_List_nil = lazy (gen_constant ["Lists"; "List"] "nil")
-
-let freevars c =
-  let rec frec acc c = match kind_of_term c with
-    | Var id       -> Idset.add id acc
-    | _ -> fold_constr frec acc c
-  in
-  frec Idset.empty c
-
-let coq_zero = lazy (gen_constant ["Init"; "Datatypes"] "O")
-let coq_succ = lazy (gen_constant ["Init"; "Datatypes"] "S")
-let coq_nat = lazy (gen_constant ["Init"; "Datatypes"] "nat")
-
-let rec coq_nat_of_int = function
-  | 0 -> Lazy.force coq_zero
-  | n -> mkApp (Lazy.force coq_succ, [| coq_nat_of_int (pred n) |])
-
-let varify_constr_list ty def varh c =
-  let vars = Idset.elements (freevars c) in
-  let mkaccess i =
-    mkApp (Lazy.force coq_List_nth,
-	  [| ty; coq_nat_of_int i; varh; def |])
-  in
-  let l = List.fold_right (fun id acc ->
-    mkApp (Lazy.force coq_List_cons, [| ty ; mkVar id; acc |]))
-    vars (mkApp (Lazy.force coq_List_nil, [| ty |]))
-  in
-  let subst =
-    list_map_i (fun i id -> (id, mkaccess i)) 0 vars
-  in
-    l, replace_vars subst c
-
-let coq_varmap_empty =  lazy (gen_constant ["quote"; "Quote"] "Empty_vm")
-let coq_varmap_node =  lazy (gen_constant ["quote"; "Quote"] "Node_vm")
-let coq_varmap_lookup =  lazy (gen_constant ["quote"; "Quote"] "varmap_find")
-
-let coq_index_left =  lazy (gen_constant ["quote"; "Quote"] "Left_idx")
-let coq_index_right =  lazy (gen_constant ["quote"; "Quote"] "Right_idx")
-let coq_index_end =  lazy (gen_constant ["quote"; "Quote"] "End_idx")
-
-let rec split_interleaved l r = function
-  | hd :: hd' :: tl' ->
-      split_interleaved (hd :: l) (hd' :: r) tl'
-  | hd :: [] -> (List.rev (hd :: l), List.rev r)
-  | [] -> (List.rev l, List.rev r)
-
-let rec mkidx i p =
-  if i mod 2 = 0 then
-    if i = 0 then mkApp (Lazy.force coq_index_left, [|Lazy.force coq_index_end|])
-    else mkApp (Lazy.force coq_index_left, [|mkidx (i - p) (2 * p)|])
-  else if i = 1 then mkApp (Lazy.force coq_index_right, [|Lazy.force coq_index_end|])
-  else mkApp (Lazy.force coq_index_right, [|mkidx (i - p) (2 * p)|])
-
-let varify_constr_varmap ty def varh c =
-  let vars = Idset.elements (freevars c) in
-  let mkaccess i =
-    mkApp (Lazy.force coq_varmap_lookup,
-	  [| ty; def; i; varh |])
-  in
-  let rec vmap_aux l cont =
-    match l with
-    | [] -> [], mkApp (Lazy.force coq_varmap_empty, [| ty |])
-    | hd :: tl ->
-	let left, right = split_interleaved [] [] tl in
-	let leftvars, leftmap = vmap_aux left (fun x -> cont (mkApp (Lazy.force coq_index_left, [| x |]))) in
-	let rightvars, rightmap = vmap_aux right (fun x -> cont (mkApp (Lazy.force coq_index_right, [| x |]))) in
-	  (hd, cont (Lazy.force coq_index_end)) :: leftvars @ rightvars,
-	mkApp (Lazy.force coq_varmap_node, [| ty; hd; leftmap ; rightmap |])
-  in
-  let subst, vmap = vmap_aux (def :: List.map (fun x -> mkVar x) vars) (fun x -> x) in
-  let subst = List.map (fun (id, x) -> (destVar id, mkaccess x)) (List.tl subst) in
-    vmap, replace_vars subst c
-
-
-TACTIC EXTEND varify
-  [ "varify" ident(varh) ident(h') constr(ty) constr(def) constr(c) ] -> [
-    let vars, c' = varify_constr_varmap ty def (mkVar varh) c in
-      tclTHEN (letin_tac None (Name varh) vars None allHyps)
-	(letin_tac None (Name h') c' None allHyps)
-  ]
-END
-
 TACTIC EXTEND not_evar
   [ "not_evar" constr(ty) ] -> [
     match kind_of_term ty with
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c0043db06..8a68c9f20 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -507,21 +507,8 @@ END
 
 (** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T] 
     where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated
-    during dependent induction. *)
+    during dependent induction. For internal use. *)
 
-TACTIC EXTEND specialize_hyp
-[ "specialize_hypothesis" hyp(id) ] -> [ specialize_hypothesis id ]
-END
-
-TACTIC EXTEND dependent_pattern
-| ["dependent" "pattern" constr(c) ] -> [ dependent_pattern c ]
-END
-
-TACTIC EXTEND dependent_pattern_from
-| ["dependent" "pattern" "from" constr(c) ] ->
-    [ dependent_pattern ~pattern_term:false c ]
-END
-
-TACTIC EXTEND resolve_classes
-| ["resolve_classes" ] -> [ resolve_classes ]
+TACTIC EXTEND specialize_eqs
+[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ]
 END
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 460d7d846..120b3510b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2433,7 +2433,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
 				   tclMAP (fun id -> 
 				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl) gl
 
-let specialize_hypothesis id gl =
+let specialize_eqs id gl =
   let env = pf_env gl in
   let ty = pf_get_hyp_typ gl id in
   let evars = ref (create_evar_defs (project gl)) in
@@ -2481,36 +2481,10 @@ let specialize_hypothesis id gl =
     else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
       
 
-let specialize_hypothesis id gl =
+let specialize_eqs id gl =
   if try ignore(clear [id] gl); false with _ -> true then
     tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl 
-  else specialize_hypothesis id gl
-
-let dependent_pattern ?(pattern_term=true) c gl =
-  let cty = pf_type_of gl c in
-  let deps =
-    match kind_of_term cty with
-    | App (f, args) -> 
-	let f', args' = decompose_indapp f args in 
-	  Array.to_list args'
-    | _ -> []
-  in
-  let varname c = match kind_of_term c with
-    | Var id -> id
-    | _ -> id_of_string (hdchar (pf_env gl) c)
-  in
-  let mklambda ty (c, id, cty) =
-    let conclvar = subst_term_occ all_occurrences c ty in
-      mkNamedLambda id cty conclvar
-  in
-  let subst = 
-    let deps = List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in
-      if pattern_term then (c, varname c, cty) :: deps
-      else deps
-  in
-  let concllda = List.fold_left mklambda (pf_concl gl) subst in
-  let conclapp = applistc concllda (List.rev_map pi1 subst) in
-    convert_concl_no_check conclapp DEFAULTcast gl
+  else specialize_eqs id gl
 
 let occur_rel n c =
   let res = not (noccurn n c) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f556551b0..e8b53c704 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -381,9 +381,7 @@ val tclABSTRACT : identifier option -> tactic -> tactic
 val admit_as_an_axiom : tactic
 
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic
-val specialize_hypothesis : identifier -> tactic
-
-val dependent_pattern : ?pattern_term:bool -> constr -> tactic
+val specialize_eqs : identifier -> tactic
 
 val register_general_multi_rewrite :
   (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index d47092f68..4b827c244 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -346,8 +346,9 @@ Proof. firstorder. Qed.
 Lemma proper_proper_proxy `(Proper A R x) : ProperProxy R x.
 Proof. firstorder. Qed.
 
-Hint Extern 1 (ProperProxy _ _) => class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
-Hint Extern 2 (ProperProxy ?R _) => not_evar R ; class_apply @proper_proper_proxy : typeclass_instances.
+Hint Extern 1 (ProperProxy _ _) => 
+  class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
+Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
@@ -383,7 +384,7 @@ Ltac partial_application_tactic :=
     let v := eval compute in n in clear n ;
     let H := fresh in
       assert(H:Params m' v) by typeclasses eauto ;
-      let v' := eval compute in v in
+      let v' := eval compute in v in subst m';
       do_partial H v' m
  in
   match goal with
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index c9ec29d2b..79c9bec53 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -221,7 +221,7 @@ Ltac simplify_eqs :=
 
 Ltac simplify_IH_hyps := repeat
   match goal with
-    | [ hyp : _ |- _ ] => specialize_hypothesis hyp
+    | [ hyp : _ |- _ ] => specialize_eqs hyp
   end.
 
 (** We split substitution tactics in the two directions depending on which 
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index da30d096c..c3cd4f4a8 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -75,11 +75,10 @@ Hint Resolve Permutation_refl Permutation_sym Permutation_trans.
 (* This provides reflexivity, symmetry and transitivity and rewriting
    on morphims to come *)
 
-Add Parametric Relation A : (list A) (@Permutation A)
-  reflexivity proved by (@Permutation_refl A)
-  symmetry proved by (@Permutation_sym A)
-  transitivity proved by (@Permutation_trans A)
-as Permutation_Equivalence.
+Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := {
+  Equivalence_Reflexive := @Permutation_refl A ;
+  Equivalence_Symmetric := @Permutation_sym A ;
+  Equivalence_Transitive := @Permutation_trans A }.
 
 Add Parametric Morphism A (a:A) : (cons a)
   with signature @Permutation A ==> @Permutation A