- 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

4 files changed, 13 insertions, 21 deletions

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