* 'default "equality"' command changed to consider also

[helm.git] / helm / software / components / tactics / equalityTactics.ml

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index 839d0532a401d44a9e159ae11cacc97a8651948e..f2760c30f33f394daded905bc246cc63446e7321 100644 (file)
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -46,6 +46,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   let proof,goal = status in
   let curi, metasenv, pbo, pty, attrs = proof in
   let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
+  let gsort,_ =
+   CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in
   match hyps_pat with
      he::(_::_ as tl) ->
        PET.apply_tactic
@@ -117,8 +119,16 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
     | C.Appl [C.MutInd (uri, 0, []); ty; t1; t2]
       when LibraryObjects.is_eq_URI uri ->
         let ind_uri =
-         if_right_to_left dir2
-          LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI
+         match gsort with
+            C.Sort C.Prop ->
+             if_right_to_left dir2
+              LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI
+          | C.Sort C.Set ->
+             if_right_to_left dir2
+              LibraryObjects.eq_rec_URI LibraryObjects.eq_rec_r_URI
+          | _ ->
+             if_right_to_left dir2
+              LibraryObjects.eq_rect_URI LibraryObjects.eq_rect_r_URI
         in
         let eq_ind = C.Const (ind_uri uri,[]) in
          if dir2 then