diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-12 09:15:49 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-12 09:15:49 +0000 |
| commit | 445dd89b113475bef680f013abdc99377791751f (patch) | |
| tree | d235ed4cbd8af055e0678373df4e6287eb29eaba /toplevel/command.ml | |
| parent | eabacd04872bda164e222cdc9b48a1ee95631c8a (diff) | |
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
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index e8e651618..5c4692e96 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 |