3 files changed, 24 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c7b6612f6a..77007b0ba5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1319,8 +1319,10 @@ and compile_alias pb (na,orig,(expanded,expanded_typ)) rest =
          mat = List.map (push_alias_eqn alias) pb.mat } in
     let j = compile pb in
     { uj_val =
-        if isRel c or isVar c then subst1 c j.uj_val
-        else mkLetIn (na,c,t,j.uj_val);
+        if isRel c || isVar c || count_occurrences (mkRel 1) j.uj_val <= 1 then
+          subst1 c j.uj_val
+        else
+          mkLetIn (na,c,t,j.uj_val);
       uj_type = subst1 c j.uj_type } in
   if isRel orig or isVar orig then
     (* Try to compile first using non expanded alias *)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index b28f8046fa..2662093487 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -576,6 +576,25 @@ let dependent_main noevar m t =
 let dependent = dependent_main false
 let dependent_no_evar = dependent_main true
 
+let count_occurrences m t =
+  let n = ref 0 in
+  let rec countrec m t =
+    if eq_constr m t then
+      incr n
+    else
+      match kind_of_term m, kind_of_term t with
+	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+	    countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+	    Array.iter (countrec m)
+	      (Array.sub lt
+		(Array.length lm) ((Array.length lt) - (Array.length lm)))
+	| _, Cast (c,_,_) when isMeta c -> ()
+	| _, Evar _ -> ()
+	| _ -> iter_constr_with_binders (lift 1) countrec m t
+  in
+  countrec m t;
+  !n
+
 (* Synonymous *)
 let occur_term = dependent
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index d101d7d4ff..1c3517d564 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -108,6 +108,7 @@ val occur_var_in_decl :
 val free_rels : constr -> Intset.t
 val dependent : constr -> constr -> bool
 val dependent_no_evar : constr -> constr -> bool
+val count_occurrences : constr -> constr -> int
 val collect_metas : constr -> int list
 val collect_vars : constr -> Idset.t (** for visible vars only *)
 val occur_term : constr -> constr -> bool (** Synonymous