- Extracted from the tactic "now" an experimental tactic "easy" for small

  automation.
- Permitted to use evars in the intermediate steps of "apply in" (as expected 
  in the test file apply.v).
- Back on the systematic use of eq_rect (r11697) for implementing
  rewriting (some proofs, especially lemma DistOoVv in
  Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in
  Sophia-Antipolis/Semantics/example2.v are explicitly refering
  to the name of the lemmas used for rewriting).
- Fixed at the same time a bug in get_sort_of (predicativity of Set was not
  taken into account).



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

6 files changed, 55 insertions, 31 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 03afe0a179..123ff43e7b 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -111,7 +111,10 @@ let retype sigma metamap =
     | Cast (c,_, s) when isSort s -> family_of_sort (destSort s)
     | Sort (Prop c) -> InType
     | Sort (Type u) -> InType
-    | Prod (name,t,c2) -> sort_family_of (push_rel (name,None,t) env) c2
+    | Prod (name,t,c2) -> 
+	let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
+	if Environ.engagement env <> Some ImpredicativeSet &&
+	   s2 = InSet & sort_family_of env t = InType then InType else s2
     | App(f,args) -> 
        family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
     | Lambda _ | Fix _ | Construct _ ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1fcfb4e12f..cdc096e84a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -93,15 +93,15 @@ let is_applied_relation t =
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. *)
 
-let find_elim hdcncl lft2rgt gl =
-  let hdcncls = string_of_inductive hdcncl in 
-  let rwr_thm = if lft2rgt then hdcncls^"_rect_r" else hdcncls^"_rect" in
+let find_elim hdcncl lft2rgt cls gl =
+  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+  let hdcncls = string_of_inductive hdcncl ^ suffix in 
+  let rwr_thm = if lft2rgt = (cls = None) then hdcncls^"_r" else hdcncls in
   try pf_global gl (id_of_string rwr_thm)
   with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".")
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt sigma c l with_evars gl hdcncl =
-  let dir = if cls=None then lft2rgt else not lft2rgt in
-  let elim = find_elim hdcncl dir gl in
+  let elim = find_elim hdcncl lft2rgt cls gl in
   general_elim_clause with_evars cls sigma c l (elim,NoBindings) gl
 
 let adjust_rewriting_direction args lft2rgt =
@@ -991,7 +991,7 @@ let swapEquandsInHyp id gls =
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
   (* find substitution scheme *)
-  let eq_elim = find_elim lbeq.eq false gls in
+  let eq_elim = find_elim lbeq.eq false None gls in
   (* build substitution predicate *)
   let p = lambda_create (pf_env gls) (t,body) in
   (* apply substitution scheme *)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 73e7fe16e9..9ea8a459c7 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -320,23 +320,14 @@ let compute_construtor_signatures isrec (_,k as ity) =
   array_map2 analrec lc lrecargs
 
 let elimination_sort_of_goal gl = 
-  match kind_of_term (hnf_type_of gl (pf_concl gl)) with 
-    | Sort s ->
-	(match s with
-	   | Prop Null -> InProp
-	   | Prop Pos -> InSet
-	   | Type _ -> InType)
-    | _        -> anomaly "goal should be a type"
+  pf_apply Retyping.get_sort_family_of gl (pf_concl gl)
 
 let elimination_sort_of_hyp id gl = 
-  match kind_of_term (hnf_type_of gl (pf_get_hyp_typ gl id)) with 
-    | Sort s ->
-	(match s with
-	   | Prop Null -> InProp
-	   | Prop Pos -> InSet
-	   | Type _ -> InType)
-    | _        -> anomaly "goal should be a type"
+  pf_apply Retyping.get_sort_family_of gl (pf_get_hyp_typ gl id)
 
+let elimination_sort_of_clause = function
+  | None -> elimination_sort_of_goal 
+  | Some id -> elimination_sort_of_hyp id
 
 (* Find the right elimination suffix corresponding to the sort of the goal *)
 (* c should be of type A1->.. An->B with B an inductive definition *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 00ce4da8d5..6cd63fa6ad 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -146,6 +146,7 @@ val compute_induction_names :
 
 val elimination_sort_of_goal : goal sigma -> sorts_family
 val elimination_sort_of_hyp  : identifier -> goal sigma -> sorts_family
+val elimination_sort_of_clause : identifier option -> goal sigma -> sorts_family
 
 val general_elim_then_using :
   (inductive -> goal sigma -> constr) -> rec_flag ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5392fc43e3..6f06c25a0b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -883,7 +883,7 @@ let apply_in_once with_delta with_destruct with_evars id ((sigma,d),lbind) gl0 =
       if not with_evars then check_evars (fst res).sigma sigma gl0;
       res
     with exn when with_destruct ->
-      descend_in_conjunctions with_evars aux (fun _ -> raise exn) c gl
+      descend_in_conjunctions true aux (fun _ -> raise exn) c gl
   in
     if sigma = Evd.empty then aux d gl0
     else
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 705fb3bdf5..0e8b4ab1f0 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -115,7 +115,7 @@ lazymatch T with
     evar (a : t); pose proof (H a) as H1; unfold a in H1;
     clear a; clear H; rename H1 into H; find_equiv H
 | ?A <-> ?B => idtac
-| _ => fail "The given statement does not seem to end with an equivalence"
+| _ => fail "The given statement does not seem to end with an equivalence."
 end.
 
 Ltac bapply lemma todo :=
@@ -135,14 +135,43 @@ bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J).
 Tactic Notation "apply" "<-" constr(lemma) "in" ident(J) :=
 bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
 
-(** A tactic simpler than auto that is useful for ending proofs "in one step" *)
-Tactic Notation "now" tactic(t) :=
-t;
-match goal with
-| H : _ |- _ => solve [inversion H]
-| _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split]
-| _ => fail 1 "Cannot solve this goal"
-end.
+(** An experimental tactic simpler than auto that is useful for ending
+    proofs "in one step" *)
+
+Ltac easy :=
+(*
+  let rec use_hyp H :=
+    match type of H with
+    | _ /\ _ => 
+    | _ => solve [inversion H] 
+    end
+  with destruct_hyp H :=
+    match type of H with
+    | _ /\ _ => case H; do_intro; do_intro
+    | _ => idtac
+    end
+*)
+  let rec use_hyp H :=
+    match type of H with
+    | _ /\ _ => exact H || destruct_hyp H
+    | _ => try solve [inversion H]
+    end
+  with do_intro := let H := fresh in intro H; use_hyp H
+  with destruct_hyp H := case H; clear H; do_intro; do_intro in
+  let rec use_hyps :=
+    match goal with
+    | H : _ /\ _ |- _  => exact H || (destruct_hyp H; use_hyps)
+    | H : _ |- _ => solve [inversion H]
+    | _ => idtac
+    end in
+  let rec do_atom :=
+    solve [reflexivity | symmetry; trivial] ||
+    contradiction ||
+    (split; do_atom)
+  with do_ccl := trivial; repeat do_intro; do_atom in
+  (use_hyps; do_ccl) || fail "Cannot solve this goal".
+
+Tactic Notation "now" tactic(t) := t; easy.
 
 (** A tactic to document or check what is proved at some point of a script *)
 Ltac now_show c := change c.