Bug 2838: ExplApp in mutual inductive parameters

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

3 files changed, 9 insertions, 11 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7396fc44cc..5fec962b8e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -210,7 +210,8 @@ let rec check_same_type ty1 ty2 =
   | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 ->
       check_same_type a1 a2;
       check_same_type b1 b2
-  | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 ->
+  | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when proj1=proj2 ->
+      check_same_ref r1 r2;
       List.iter2 check_same_type al1 al2
   | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) ->
       check_same_type e1 e2;
@@ -254,7 +255,7 @@ and check_same_fix_binder bl1 bl2 =
           check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
       | _ -> failwith "not same binder") bl1 bl2
 
-let same c d = try check_same_type c d; true with _ -> false
+let is_same_type c d = try let () = check_same_type c d in true with Failure _ -> false
 
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
@@ -848,7 +849,7 @@ and factorize_prod scopes vars aty c =
     ([],extern_symbol (Some Notation.type_scope,snd scopes) vars c (uninterp_notations c))
   with No_match -> match c with
   | GProd (loc,(Name id as na),bk,ty,c)
-      when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
+      when is_same_type aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
 	-> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
            ((loc,Name id)::nal,c)
@@ -860,7 +861,7 @@ and factorize_lambda inctx scopes vars aty c =
     ([],extern_symbol (None,snd scopes) vars c (uninterp_notations c))
   with No_match -> match c with
   | GLambda (loc,na,bk,ty,c)
-      when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
+      when is_same_type aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
 	-> let (nal,c) =
 	     factorize_lambda inctx scopes (add_vname vars na) aty c in
@@ -879,7 +880,7 @@ and extern_local_binder scopes vars = function
       let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
       (match extern_local_binder scopes (name_fold Idset.add na vars) l with
           (assums,ids,LocalRawAssum(nal,k,ty')::l)
-            when same ty ty' &
+            when is_same_type ty ty' &
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::assums,na::ids,
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 9f7acbc6d1..d865bc581a 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -22,7 +22,7 @@ open Notation_term
 open Notation
 open Misctypes
 
-val check_same_type : constr_expr -> constr_expr -> unit
+val is_same_type : constr_expr -> constr_expr -> bool
 
 (** Translation of pattern, cases pattern, glob_constr and term into syntax
    trees for printing *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e8e6516187..5c4692e966 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -321,17 +321,14 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
     mind_entry_inds = entries },
     impls
 
-let eq_constr_expr c1 c2 =
-  try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false
-
 (* Very syntactical equality *)
 let eq_local_binder d1 d2 = match d1,d2 with
   | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) ->
       List.length nal1 = List.length nal2 && k1 = k2 &&
       List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 &&
-      eq_constr_expr c1 c2
+      Constrextern.is_same_type c1 c2
   | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) ->
-      id1 = id2 && eq_constr_expr c1 c2
+      id1 = id2 && Constrextern.is_same_type c1 c2
   | _ ->
       false