More optimizations of [Clenv.clenv_fchain].

Everywhere we know that the universes of the left argument are an
extension of the right argument, we do not have to merge universes.

3 files changed, 4 insertions, 4 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 674c85af79..fe0ca61c66 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -914,7 +914,7 @@ let apply_on_clause (f,t) clause =
     (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
-  clenv_fchain argmv f_clause clause
+  clenv_fchain ~with_univs:false argmv f_clause clause
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
   let e = next_ident_away eq_baseid (ids_of_context env) in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bc82e9ef46..4cce891a2a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -620,7 +620,7 @@ module New = struct
 	  errorlabstrm "Tacticals.general_elim_then_using"
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
-    let elimclause' = clenv_fchain indmv elimclause indclause in
+    let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
     let branchsigns = compute_construtor_signatures isrec ind in
     let brnames = compute_induction_names (Array.length branchsigns) allnames in
     let flags = Unification.elim_flags () in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0551787e3a..8daa7c4b86 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1605,7 +1605,7 @@ let progress_with_clause flags innerclause clause =
   let ordered_metas = List.rev (clenv_independent clause) in
   if List.is_empty ordered_metas then error "Statement without assumptions.";
   let f mv =
-    try Some (find_matching_clause (clenv_fchain mv ~flags clause) innerclause)
+    try Some (find_matching_clause (clenv_fchain ~with_univs:false mv ~flags clause) innerclause)
     with Failure _ -> None
   in
   try List.find_map f ordered_metas
@@ -3756,7 +3756,7 @@ let recolle_clenv i params args elimclause gl =
          trying to unify (which would lead to trying to apply it to
          evars if y is a product). *)
       let indclause  = mk_clenv_from_n gl (Some 0) (x,y) in
-      let elimclause' = clenv_fchain i acc indclause in
+      let elimclause' = clenv_fchain ~with_univs:false i acc indclause in
       elimclause')
     (List.rev clauses)
     elimclause